From c250e58dfd5d89b14bde8692de42bc388ad54de2 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 21 Aug 2026 21:42:39 +0000 Subject: [PATCH] chore: bump toolchain to v4.34.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 75def609..b814d987 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.34.0-rc1 +leanprover/lean4:v4.34.0-rc2 diff --git a/test/Mathlib/lake-manifest.json b/test/Mathlib/lake-manifest.json index 649b190b..6d8f4828 100644 --- a/test/Mathlib/lake-manifest.json +++ b/test/Mathlib/lake-manifest.json @@ -5,17 +5,17 @@ "type": "git", "subDir": null, "scope": "", - "rev": "de5ce8a9a66a4aa68a9bdbb35b63a06d34d9ca11", + "rev": "85e3a25e006c35636f0e53b0e9296caca2685bc0", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.34.0-rc1", + "inputRev": "v4.34.0-rc2", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "38e9c3ce15cbb63c92e90bb9a92e4eb82131f669", + "rev": "d9598f07b1bc701f1e3aae163d2681c1fd978793", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2bc7cf064315b26bc38dac2e9612fb581be9b75f", + "rev": "ba67e212be1197b84c1f1f6299488a10a3002713", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "978b7ec9fbbf9a535114f1de8fe5b3778b358870", + "rev": "d8823026ac7ef130c253089d95685f9877b95323", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "99e8adeea3c3cd86b6b79ba01a1383bf2d31d055", + "rev": "a8acbfd87375ff4abe14ce09db5b7664d383bc7f", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c1c4362a130f12e632d252180a6c2a31d8fd4726", + "rev": "18889deb9e83ea7420ef51c160d6f88552e744e3", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3b55e9d00c6b0018e5d984eb011b6f93c09bd163", + "rev": "507746ab8f4b643ccdacb2ec4cdb5853fa9f8ab3", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "01bc479e7432594821ba3fb0ca465211941de86d", + "rev": "d54dddc581e08be364c278052863524bff7a99a9", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,10 +85,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "af8bc067a4cc6c6df472a68909a3f40b1c76c43e", + "rev": "ab3a82db9fea14cf0fd7f5a2de650f4b534640af", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.34.0-rc1", + "inputRev": "v4.34.0-rc2", "inherited": true, "configFile": "lakefile.toml"}], "name": "«repl-mathlib-tests»", diff --git a/test/Mathlib/lakefile.toml b/test/Mathlib/lakefile.toml index 495648cb..5f4ebc2b 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.34.0-rc1" +rev = "v4.34.0-rc2" [[lean_lib]] name = "ReplMathlibTests" diff --git a/test/Mathlib/lean-toolchain b/test/Mathlib/lean-toolchain index 75def609..b814d987 100644 --- a/test/Mathlib/lean-toolchain +++ b/test/Mathlib/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.34.0-rc1 +leanprover/lean4:v4.34.0-rc2