From 28260d38be738952f0ec5b7a13f962f74f97b691 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 6 Jan 2025 17:46:29 +1100 Subject: [PATCH 1/3] bump toolchain/Mathlib to v4.15.0 --- lake-manifest.json | 86 +++++++++++++--------------------------------- lakefile.lean | 2 +- lean-toolchain | 2 +- 3 files changed, 25 insertions(+), 65 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 7080c006..9279c3fc 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,17 +1,7 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/doc-gen4", - "type": "git", - "subDir": null, - "scope": "", - "rev": "e498801db5f148f633237b7cf9f4284f0fd197f8", - "name": "«doc-gen4»", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/PatrickMassot/checkdecls.git", + [{"url": "https://github.com/PatrickMassot/checkdecls.git", "type": "git", "subDir": null, "scope": "", @@ -25,60 +15,20 @@ "type": "git", "subDir": null, "scope": "", - "rev": "e4220ebf1cdae020e7e79ba5a35d26e163bac828", + "rev": "9837ca9d65d9de6fad1ef4381750ca688774e608", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": null, + "inputRev": "v4.15.0", "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/mhuisi/lean4-cli", - "type": "git", - "subDir": null, - "scope": "", - "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/fgdorais/lean4-unicode-basic", - "type": "git", - "subDir": null, - "scope": "", - "rev": "d55279d2ff01759fa75752fcf1a93d1db8db18ff", - "name": "UnicodeBasic", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/dupuisf/BibtexQuery", - "type": "git", - "subDir": null, - "scope": "", - "rev": "982700bcf78b93166e5b1af0b4b756b8acfdb54b", - "name": "BibtexQuery", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/acmepjz/md4lean", - "type": "git", - "subDir": null, - "scope": "", - "rev": "fe8e6e649ac8251f43c6f6f934f095ebebce7e7c", - "name": "MD4Lean", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8e5cb8d424df462f84997dd68af6f40e347c3e35", + "rev": "2c57364ef83406ea86d0f78ce3e342079a2fece5", "name": "plausible", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0-rc1", + "inputRev": "v4.15.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/LeanSearchClient", @@ -95,10 +45,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ed3b856bd8893ade75cafe13e8544d4c2660f377", + "rev": "9a0b533c2fbd6195df067630be18e11e4349051c", "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0-rc1", + "inputRev": "v4.15.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", @@ -115,29 +65,39 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a4a08d92be3de00def5298059bf707c72dfd3c66", + "rev": "2689851f387bb2cef351e6825fe94a56a304ca13", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.15.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ad942fdf0b15c38bface6acbb01d63855a2519ac", + "rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "v4.14.0", + "inputRev": "v4.15.0", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f007bfe46ea8fb801ec907df9ab540054abcc5fd", + "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b", "name": "batteries", "manifestFile": "lake-manifest.json", + "inputRev": "v4.15.0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", + "name": "Cli", + "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}], diff --git a/lakefile.lean b/lakefile.lean index 14c264f8..a5576dee 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -8,7 +8,7 @@ package FLT where ⟨`relaxedAutoImplicit, false⟩ -- switch off relaxed auto-implicit ] -require mathlib from git "https://github.com/leanprover-community/mathlib4.git" +require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "v4.15.0" require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git" diff --git a/lean-toolchain b/lean-toolchain index cf25a981..d0eb99ff 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.15.0-rc1 +leanprover/lean4:v4.15.0 From 2b9242af633025e230cd469ad2012733ef180db5 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 6 Jan 2025 17:49:17 +1100 Subject: [PATCH 2/3] chore: bump toolchain/Mathlib to v4.16.0-rc1 --- lake-manifest.json | 24 ++++++++++++------------ lakefile.lean | 2 +- lean-toolchain | 2 +- 3 files changed, 14 insertions(+), 14 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 9279c3fc..cc5562ef 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,20 +15,20 @@ "type": "git", "subDir": null, "scope": "", - "rev": "9837ca9d65d9de6fad1ef4381750ca688774e608", + "rev": "a57f31753dde989bc415cb64277a1688866e443c", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0", + "inputRev": "v4.16.0-rc1", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2c57364ef83406ea86d0f78ce3e342079a2fece5", + "rev": "1622a8693b31523c8f82db48e01b14c74bc1f155", "name": "plausible", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0", + "inputRev": "v4.16.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/LeanSearchClient", @@ -45,30 +45,30 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9a0b533c2fbd6195df067630be18e11e4349051c", + "rev": "9cb79405471ae931ac718231d6299bfaffef9087", "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0", + "inputRev": "v4.16.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2b000e02d50394af68cfb4770a291113d94801b5", + "rev": "07f60e90998dfd6592688a14cd67bd4e384b77b2", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.48", + "inputRev": "v0.0.50", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2689851f387bb2cef351e6825fe94a56a304ca13", + "rev": "79402ad9ab4be9a2286701a9880697e2351e4955", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0", + "inputRev": "v4.16.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", @@ -85,10 +85,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b", + "rev": "b2e8b6868397fcd93c00aca7278b933c16c0ffb3", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0", + "inputRev": "v4.16.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.lean b/lakefile.lean index a5576dee..aaeb66bc 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -8,7 +8,7 @@ package FLT where ⟨`relaxedAutoImplicit, false⟩ -- switch off relaxed auto-implicit ] -require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "v4.15.0" +require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "v4.16.0-rc1" require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git" diff --git a/lean-toolchain b/lean-toolchain index d0eb99ff..62ccd717 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.15.0 +leanprover/lean4:v4.16.0-rc1 From 6608605e111e475ca4e85ad2981a73926cc6b9d8 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 6 Jan 2025 17:57:28 +1100 Subject: [PATCH 3/3] doc-gen4 --- lake-manifest.json | 62 ++++++++++++++++++++++++++++++++++++++-------- lakefile.lean | 2 +- 2 files changed, 52 insertions(+), 12 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index cc5562ef..acfdab79 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,7 +1,17 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/PatrickMassot/checkdecls.git", + [{"url": "https://github.com/leanprover/doc-gen4", + "type": "git", + "subDir": null, + "scope": "", + "rev": "5a111ebbb151dc6719734f39b1d3aea8d5affb76", + "name": "«doc-gen4»", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.16.0-rc1", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/PatrickMassot/checkdecls.git", "type": "git", "subDir": null, "scope": "", @@ -21,6 +31,46 @@ "inputRev": "v4.16.0-rc1", "inherited": false, "configFile": "lakefile.lean"}, + {"url": "https://github.com/mhuisi/lean4-cli", + "type": "git", + "subDir": null, + "scope": "", + "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/fgdorais/lean4-unicode-basic", + "type": "git", + "subDir": null, + "scope": "", + "rev": "51b0cd28a0ca79ccfa91b8c7d5eb94ba075dfdb4", + "name": "UnicodeBasic", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/dupuisf/BibtexQuery", + "type": "git", + "subDir": null, + "scope": "", + "rev": "46376bc3c8f46ac1a1fd7712856b0f7bd6166098", + "name": "BibtexQuery", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/kim-em/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "17e3f60bca8b6fdc19a55e2a7c9840a9f7afd1dc", + "name": "MD4Lean", + "manifestFile": "lake-manifest.json", + "inputRev": "bump_to_v4.16.0-rc1", + "inherited": true, + "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, @@ -90,16 +140,6 @@ "manifestFile": "lake-manifest.json", "inputRev": "v4.16.0-rc1", "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "scope": "leanprover", - "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, "configFile": "lakefile.toml"}], "name": "FLT", "lakeDir": ".lake"} diff --git a/lakefile.lean b/lakefile.lean index aaeb66bc..cf368443 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -15,7 +15,7 @@ require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git" -- This is run only if we're in `dev` mode. This is so not everyone has to build doc-gen meta if get_config? env = some "dev" then require «doc-gen4» from git - "https://github.com/leanprover/doc-gen4" @ "main" + "https://github.com/leanprover/doc-gen4" @ "v4.16.0-rc1" @[default_target] lean_lib FLT where