From f330a0f6e1700cb77354c9a966ff35461a8bb82f Mon Sep 17 00:00:00 2001 From: Joscha Date: Mon, 10 Aug 2026 12:52:16 +0200 Subject: [PATCH] chore: bump toolchain to v4.33.0 --- lean-toolchain | 2 +- test/Mathlib/lake-manifest.json | 22 +++++++++++----------- test/Mathlib/lakefile.toml | 2 +- test/Mathlib/lean-toolchain | 2 +- 4 files changed, 14 insertions(+), 14 deletions(-) diff --git a/lean-toolchain b/lean-toolchain index c084c7fb..025e5954 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.33.0-rc2 +leanprover/lean4:v4.33.0 diff --git a/test/Mathlib/lake-manifest.json b/test/Mathlib/lake-manifest.json index 12170170..2b8b5ff4 100644 --- a/test/Mathlib/lake-manifest.json +++ b/test/Mathlib/lake-manifest.json @@ -5,17 +5,17 @@ "type": "git", "subDir": null, "scope": "", - "rev": "51e6992efd06126df61a496bebf8f49482a4e129", + "rev": "db584cd6d46c92f209a44c0f1c829460d327499d", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.33.0-rc2", + "inputRev": "v4.33.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "123d15766ba49356c02ebad2a4462dfe12d79899", + "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f5c090429dff3cf66cb65562526c9ea6e8edfbcb", + "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "bb3469a87774349fe01898d8bf2fc6a1ce6411ca", + "rev": "16f02aa7642864af59f1ff0e384a015994db9118", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "222c58dad7706a6e7cae46c0edd65ea881d3ee27", + "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7db8190085343afde2f5d2cdcc9bac719b6ec02c", + "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ef42f8944eaf5b6cbfbe75d1917d824c7dd6cf33", + "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "76e1c118b0700b4ceafe99532e887d6431625e1a", + "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,10 +85,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "1319485273bf87833fa472afbcefdedecb16b45f", + "rev": "6130a47896ce867c6a4a55373441e59e565bad0f", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.33.0-rc2", + "inputRev": "v4.33.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "«repl-mathlib-tests»", diff --git a/test/Mathlib/lakefile.toml b/test/Mathlib/lakefile.toml index 2deb31fa..9c3f5c0a 100644 --- a/test/Mathlib/lakefile.toml +++ b/test/Mathlib/lakefile.toml @@ -4,7 +4,7 @@ defaultTargets = ["ReplMathlibTests"] [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4" -rev = "v4.33.0-rc2" +rev = "v4.33.0" [[lean_lib]] name = "ReplMathlibTests" diff --git a/test/Mathlib/lean-toolchain b/test/Mathlib/lean-toolchain index c084c7fb..025e5954 100644 --- a/test/Mathlib/lean-toolchain +++ b/test/Mathlib/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.33.0-rc2 +leanprover/lean4:v4.33.0