From ea4bd9e303dbbaf78f1c4701e71cd8a0ac0ed10e Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Tue, 2 Sep 2025 13:20:56 +0000 Subject: [PATCH 1/4] Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/10204 --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 921714f9f93677..dd3616a802772d 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,10 +65,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d7745b2c3a73f65714f18b0d1691274a044f42f0", + "rev": "f0fa8674e63ac767001560e33a240d1bca168b41", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", + "inputRev": "lean-pr-testing-10204", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.lean b/lakefile.lean index 5c59b63676891c..c38371b73c6b45 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,7 +6,7 @@ open Lake DSL ## Mathlib dependencies on upstream projects -/ -require "leanprover-community" / "batteries" @ git "nightly-testing" +require "leanprover-community" / "batteries" @ git "lean-pr-testing-10204" require "leanprover-community" / "Qq" @ git "master" require "leanprover-community" / "aesop" @ git "nightly-testing" require "leanprover-community" / "proofwidgets" @ git "v0.0.71" -- ProofWidgets should always be pinned to a specific version diff --git a/lean-toolchain b/lean-toolchain index 623fd555865cc8..6917fade612d16 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2025-08-31 +leanprover/lean4-pr-releases:pr-release-10204-328dfb0 From ec929dfb13b1a9e2aad2647ceffbfecab8469b3a Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 2 Sep 2025 17:23:27 +0100 Subject: [PATCH 2/4] Update revision for batteries dependency --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index dd3616a802772d..734d2b4b3a6937 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f0fa8674e63ac767001560e33a240d1bca168b41", + "rev": "5ffe9a04ca578fa628215e4ebb0f458d214d9bcf", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "lean-pr-testing-10204", From 3e42fc9b09ceb02c3bea0da02ac1497b5099b6cc Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 3 Sep 2025 00:13:21 +0100 Subject: [PATCH 3/4] Update revision for aesop dependency --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index 734d2b4b3a6937..a99a0ec33a3fd9 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "fc97e592e3e150370f17a12e3613e96252c4d3d0", + "rev": "66a992130e481dc52984fc8160c03846a5f4ee59", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", From a344401ee355d05ba1dcd11194f7a1d345eaa44e Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 3 Sep 2025 00:47:46 +0100 Subject: [PATCH 4/4] Update revision for aesop dependency --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index a99a0ec33a3fd9..4448934614f3b2 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "66a992130e481dc52984fc8160c03846a5f4ee59", + "rev": "5cb8276380ebdb5a5045d2cccf6466319578fa23", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing",