From aee8bb1676aaf50adce168a2148dfb87c67bcb6b Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Wed, 29 Oct 2025 23:04:44 +0100 Subject: [PATCH] Update to lean 4.24 --- docbuild/lake-manifest.json | 60 ++++++++++++++++++------------------- docbuild/lakefile.toml | 2 +- docbuild/lean-toolchain | 2 +- lake-manifest.json | 30 +++++++++---------- lakefile.toml | 2 +- lean-toolchain | 2 +- 6 files changed, 49 insertions(+), 49 deletions(-) diff --git a/docbuild/lake-manifest.json b/docbuild/lake-manifest.json index ede2da6a..1ac60bb2 100644 --- a/docbuild/lake-manifest.json +++ b/docbuild/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "58b48e75bd19f785927e06912dea610e5e48f1fa", + "rev": "1cd7a1113090e216703e323e8fdcdf099f0a9c8a", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0", + "inputRev": "v4.24.0", "inherited": false, "configFile": "lakefile.lean"}, {"type": "path", @@ -18,21 +18,11 @@ "inherited": false, "dir": "../", "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/ProofWidgets4", - "type": "git", - "subDir": null, - "scope": "", - "rev": "0c1d7d3d202757dc00e5ac4e6dac32a8e70d173a", - "name": "proofwidgets", - "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.69", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/mhuisi/lean4-cli", + {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "", - "rev": "6667b921594697980586296511fab6a359e802d1", + "rev": "91c18fa62838ad0ab7384c03c9684d99d306e1da", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -42,7 +32,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "d3195374a885cf2b0bfa66063deb493686029f95", + "rev": "e5aaa4949aad9a866aead1da5d5619e8decc8da7", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -52,17 +42,17 @@ "type": "git", "subDir": null, "scope": "", - "rev": "dbfe2b7630c5f7c5c1cf71e7747ffc0a30337f69", + "rev": "1b05159ad44f220cec7489e65e6bc4b1e178b67f", "name": "BibtexQuery", "manifestFile": "lake-manifest.json", - "inputRev": "dbfe2b7630c5f7c5c1cf71e7747ffc0a30337f69", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/acmepjz/md4lean", "type": "git", "subDir": null, "scope": "", - "rev": "feac4e0c356b0928657bf3b54fa83ae952f53257", + "rev": "66aefec2852d3e229517694e642659f316576591", "name": "MD4Lean", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -72,20 +62,20 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "79e94a093aff4a60fb1b1f92d9681e407124c2ca", + "rev": "f897ebcf72cd16f89ab4577d0c826cd14afaafc7", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0", + "inputRev": "v4.24.0", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b100ad4c5d74a464f497aaa8e7c74d86bf39a56f", + "rev": "dfd06ebfe8d0e8fa7faba9cb5e5a2e74e7bd2805", "name": "plausible", "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/LeanSearchClient", @@ -102,40 +92,50 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "eb164a46de87078f27640ee71e6c3841defc2484", + "rev": "d768126816be17600904726ca7976b185786e6b9", "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "556caed0eadb7901e068131d1be208dd907d07a2", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.74", + "inherited": true, + "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1256a18522728c2eeed6109b02dd2b8f207a2a3c", + "rev": "725ac8cd67acd70a7beaf47c3725e23484c1ef50", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "917bfa5064b812b7fbd7112d018ea0b4def25ab3", + "rev": "dea6a3361fa36d5a13f87333dc506ada582e025c", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e96b5eca4fcfe2e0e96a1511a6cd5747515aba82", + "rev": "8da40b72fece29b7d3fe3d768bac4c8910ce9bee", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0-rc4", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}], "name": "docbuild", diff --git a/docbuild/lakefile.toml b/docbuild/lakefile.toml index 42328d32..db7c4e8e 100644 --- a/docbuild/lakefile.toml +++ b/docbuild/lakefile.toml @@ -10,4 +10,4 @@ path = "../" [[require]] scope = "leanprover" name = "doc-gen4" -rev = "v4.22.0" +rev = "v4.24.0" diff --git a/docbuild/lean-toolchain b/docbuild/lean-toolchain index 6ac6d4c4..c00a5350 100644 --- a/docbuild/lean-toolchain +++ b/docbuild/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.22.0 +leanprover/lean4:v4.24.0 diff --git a/lake-manifest.json b/lake-manifest.json index 5abb587b..0ffbb0e6 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,20 +5,20 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "79e94a093aff4a60fb1b1f92d9681e407124c2ca", + "rev": "f897ebcf72cd16f89ab4577d0c826cd14afaafc7", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0", + "inputRev": "v4.24.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b100ad4c5d74a464f497aaa8e7c74d86bf39a56f", + "rev": "dfd06ebfe8d0e8fa7faba9cb5e5a2e74e7bd2805", "name": "plausible", "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/LeanSearchClient", @@ -35,57 +35,57 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "eb164a46de87078f27640ee71e6c3841defc2484", + "rev": "d768126816be17600904726ca7976b185786e6b9", "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1253a071e6939b0faf5c09d2b30b0bfc79dae407", + "rev": "556caed0eadb7901e068131d1be208dd907d07a2", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.68", + "inputRev": "v0.0.74", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1256a18522728c2eeed6109b02dd2b8f207a2a3c", + "rev": "725ac8cd67acd70a7beaf47c3725e23484c1ef50", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "917bfa5064b812b7fbd7112d018ea0b4def25ab3", + "rev": "dea6a3361fa36d5a13f87333dc506ada582e025c", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "240676e9568c254a69be94801889d4b13f3b249f", + "rev": "8da40b72fece29b7d3fe3d768bac4c8910ce9bee", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "leanprover", - "rev": "c682c91d2d4dd59a7187e2ab977ac25bd1f87329", + "rev": "91c18fa62838ad0ab7384c03c9684d99d306e1da", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.toml b/lakefile.toml index 56150100..6b6cb212 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -5,7 +5,7 @@ defaultTargets = ["Prelude", "Anoma", "AVM", "Applib", "Apps", "Goose", "Tests"] [[require]] name = "mathlib" scope = "leanprover-community" -rev = "v4.22.0" +rev = "v4.24.0" [leanOptions] relaxedAutoImplicit = false diff --git a/lean-toolchain b/lean-toolchain index 6ac6d4c4..c00a5350 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.22.0 +leanprover/lean4:v4.24.0