From 2088d15abffe3f96dec98fb5e455c81136bcf561 Mon Sep 17 00:00:00 2001 From: Joscha Date: Wed, 16 Sep 2026 23:58:33 +0200 Subject: [PATCH] chore: bump toolchain to v4.35.0-rc2 --- 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 3d1dc1d0..acc704ff 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.35.0-rc1 +leanprover/lean4:v4.35.0-rc2 diff --git a/test/Mathlib/lake-manifest.json b/test/Mathlib/lake-manifest.json index 25ea1397..151bd1b5 100644 --- a/test/Mathlib/lake-manifest.json +++ b/test/Mathlib/lake-manifest.json @@ -5,17 +5,17 @@ "type": "git", "subDir": null, "scope": "", - "rev": "c32e1ec0d1eb5237ba344eee50162f45d5b0fc76", + "rev": "065356127b1dc0016f66b7283ce0ce2c4055aa55", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.35.0-rc1", + "inputRev": "v4.35.0-rc2", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "16fe28ca7c2e01b71856f7a0a801ea844580f2d5", + "rev": "e50948299c4dc4a4c21b1c34b6a6a4fddc19f912", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b43172c7f62b95ecd6daa0951602b83eb35182a1", + "rev": "95e037bfdc31d3916ac615446847fb01960e2719", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "0b9118a4a6d4c752e51f4f731edc09f4cc135f4c", + "rev": "10930f8138f0462dbd744a91fc03a16fae0e046f", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "af0c1665a9cdb1c90409b52a183113efbb5a4480", + "rev": "4c70ac059693669e5756e32a7a94b57ee1e99dc5", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7938bfd115516f80b260d43faf630c8520471a00", + "rev": "75d936c7af167cc93fac0d31237682fc2204591d", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "21558817bf8b77bab8f4c3081e0062201fd974d2", + "rev": "786b7acdca7eb4e9c76c5d1d5bd810e7e5c56334", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2a71587431553220d08be069a144b8215350e1d6", + "rev": "ed9b316aabe389fec1ef43c3326ab48c7e59be42", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,10 +85,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "3c7ccd7060887fa478a55e555fae61bbf466c3ba", + "rev": "2842b9871b04862f944c032e34052cb9448ccb71", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.35.0-rc1", + "inputRev": "v4.35.0-rc2", "inherited": true, "configFile": "lakefile.toml"}], "name": "«repl-mathlib-tests»", diff --git a/test/Mathlib/lakefile.toml b/test/Mathlib/lakefile.toml index 8458c544..098b0e00 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.35.0-rc1" +rev = "v4.35.0-rc2" [[lean_lib]] name = "ReplMathlibTests" diff --git a/test/Mathlib/lean-toolchain b/test/Mathlib/lean-toolchain index 3d1dc1d0..acc704ff 100644 --- a/test/Mathlib/lean-toolchain +++ b/test/Mathlib/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.35.0-rc1 +leanprover/lean4:v4.35.0-rc2