From 5598641c69f14f3222aec71690ac648ee51ece49 Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Fri, 1 Nov 2024 17:54:21 +0900 Subject: [PATCH 1/5] Update to v4.13.0-rc3 --- lake-manifest.json | 52 +++++++++++++++++++++++++++------------------- lakefile.lean | 4 ++-- lean-toolchain | 2 +- 3 files changed, 34 insertions(+), 24 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 75c21fb..b1a3699 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "937cd3219c0beffa7b623d2905707d1304da259e", + "rev": "422d1a5f608fccafeddab9748e8038ef346b59bf", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6", + "rev": "fa3d73a2cf077f4b14c7840352ac7b08aeb6eb41", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "622d52c803db99ff4ea4fb442c1db9e91aed944c", + "rev": "b20a88676fd00affb90cbc9f1ff004ae588103b3", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -35,47 +35,57 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d1b33202c3a29a079f292de65ea438648123b635", + "rev": "cd20dae87c48495f0220663014dff11671597fcf", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.39", + "inputRev": "v0.0.43-pre", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, - "scope": "", - "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29", + "scope": "leanprover", + "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/import-graph", "type": "git", "subDir": null, "scope": "", - "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7", + "rev": "984d7ee170b75d6b03c0903e0b750ee2c6d1e3fb", "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7", + "inputRev": "main", "inherited": false, "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "7bedaed1ef024add1e171cc17706b012a9a37802", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, - "scope": "", - "rev": "ab9dec5b351bc7e92f30b47031edf13458bc7a1d", + "scope": "leanprover-community", + "rev": "a54be302d6fd476755ef0d77c2e4b3a7768e9c9c", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "ab9dec5b351bc7e92f30b47031edf13458bc7a1d", + "inputRev": "master", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/FormalizedFormalLogic/Foundation", "type": "git", "subDir": null, "scope": "", - "rev": "33e08c2b47f966f772df9af60cbdbc5688295bbf", + "rev": "86061a79f3936f3c5d58ae1c75ab7f7755de7530", "name": "foundation", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -85,7 +95,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "85e327734277b7f5b91d272d34a060ed21cbfdfa", + "rev": "bb64ed6d177ed0ad96f4b409a5b85c3975ce4209", "name": "arithmetization", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -95,7 +105,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "a8ad9e0408c932c95aca6dc136cb081f789aeab9", + "rev": "ebafa2a385533589fab7f40b042ad6e41ed9c6eb", "name": "incompleteness", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -105,7 +115,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "9148a0a7506099963925cf239c491fcda5ed0044", + "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005", "name": "MD4Lean", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -115,7 +125,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "f93115d0209de6db335725dee900d379f40c0317", + "rev": "107e98b3e7603628d9bfd817b4704488d8a25e96", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -125,7 +135,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "bd8747df9ee72fca365efa5bd3bd0d8dcd083b9f", + "rev": "bdc2fc30b1e834b294759a5d391d83020a90058e", "name": "BibtexQuery", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -135,10 +145,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "b941c425f6f0f1dc45fe13b850ffa7db1bb20d04", + "rev": "c2156beadb1a4d049ff3b19fe396c5403025aac5", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", - "inputRev": "b941c425f6f0f1dc45fe13b850ffa7db1bb20d04", + "inputRev": "main", "inherited": false, "configFile": "lakefile.lean"}], "name": "Summary", diff --git a/lakefile.lean b/lakefile.lean index 4ca5ab7..b99f56e 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -5,8 +5,8 @@ require foundation from git "https://github.com/FormalizedFormalLogic/Foundation require arithmetization from git "https://github.com/FormalizedFormalLogic/Arithmetization" @ "master" require incompleteness from git "https://github.com/FormalizedFormalLogic/Incompleteness" @ "master" -require importGraph from git "https://github.com/leanprover-community/import-graph" @ "68b518c9b352fbee16e6d632adcb7a6d0760e2b7" -require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "b941c425f6f0f1dc45fe13b850ffa7db1bb20d04" +require importGraph from git "https://github.com/leanprover-community/import-graph" @ "main" +require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main" package "Summary" where diff --git a/lean-toolchain b/lean-toolchain index 6a4259f..eff86fd 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.10.0-rc2 +leanprover/lean4:v4.13.0-rc3 From 54c5a9f69704cef6a2396b0fc82a43775a86b480 Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Fri, 1 Nov 2024 17:55:40 +0900 Subject: [PATCH 2/5] fx ci --- .github/workflows/build.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 3ded8fd..d9fa00e 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -2,6 +2,8 @@ name: CI on: push: + branches: + - "master" pull_request: workflow_dispatch: From a008e23a06367eb87b6768450df49369ad58d7e1 Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Fri, 1 Nov 2024 17:56:39 +0900 Subject: [PATCH 3/5] concurrency --- .github/workflows/build.yml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index d9fa00e..eefd9af 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -12,6 +12,10 @@ permissions: pages: write id-token: write +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + jobs: build: runs-on: ubuntu-latest From 2276b3fcdf2946fb38bc80325f6058114e6dfc4c Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Fri, 8 Nov 2024 04:28:20 +0900 Subject: [PATCH 4/5] upd --- lake-manifest.json | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index b1a3699..e4057b8 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "984d7ee170b75d6b03c0903e0b750ee2c6d1e3fb", + "rev": "ac7b989cbf99169509433124ae484318e953d201", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "86061a79f3936f3c5d58ae1c75ab7f7755de7530", + "rev": "cf6358e190e3cdf58aa26db6e4221ba55c092414", "name": "foundation", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -125,7 +125,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "107e98b3e7603628d9bfd817b4704488d8a25e96", + "rev": "b41bc9cec7f433d6e1d74ff3b59edaaf58ad2915", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -145,7 +145,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "c2156beadb1a4d049ff3b19fe396c5403025aac5", + "rev": "b6ae1cf11e83d972ffa363f9cdc8a2f89aaa24dc", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", "inputRev": "main", From 7e9f5c25d293040f36d4b855882d60535c175cf2 Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Sun, 10 Nov 2024 09:35:24 +0900 Subject: [PATCH 5/5] upd --- lake-manifest.json | 14 +++++++------- lakefile.lean | 1 - 2 files changed, 7 insertions(+), 8 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index e4057b8..9b05b9a 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -54,12 +54,12 @@ {"url": "https://github.com/leanprover-community/import-graph", "type": "git", "subDir": null, - "scope": "", - "rev": "ac7b989cbf99169509433124ae484318e953d201", + "scope": "leanprover-community", + "rev": "9b4088ccf0f44ddd7b1132bb1348aef8cf481e12", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", - "inherited": false, + "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/LeanSearchClient", "type": "git", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "cf6358e190e3cdf58aa26db6e4221ba55c092414", + "rev": "e6caa4b3db976f31c803623a3545493f41f33f5d", "name": "foundation", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -95,7 +95,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "bb64ed6d177ed0ad96f4b409a5b85c3975ce4209", + "rev": "c452703ba2b6fd57a7eb511590b2ff9d7ba70a05", "name": "arithmetization", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -105,7 +105,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "ebafa2a385533589fab7f40b042ad6e41ed9c6eb", + "rev": "6e4c2d997e5a84008963467a618274370fbe6a6c", "name": "incompleteness", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -145,7 +145,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "b6ae1cf11e83d972ffa363f9cdc8a2f89aaa24dc", + "rev": "e18c6c23dd7cb1f12d79d6304262351df943aa37", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.lean b/lakefile.lean index b99f56e..1c3b524 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -5,7 +5,6 @@ require foundation from git "https://github.com/FormalizedFormalLogic/Foundation require arithmetization from git "https://github.com/FormalizedFormalLogic/Arithmetization" @ "master" require incompleteness from git "https://github.com/FormalizedFormalLogic/Incompleteness" @ "master" -require importGraph from git "https://github.com/leanprover-community/import-graph" @ "main" require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main" package "Summary" where