From e308794d747f3eb711084133c9c17d385e5ec30b Mon Sep 17 00:00:00 2001 From: "mathlib-nightly-testing[bot]" Date: Wed, 22 Jul 2026 15:08:19 +0000 Subject: [PATCH 1/3] Update Batteries branch for testing https://github.com/leanprover-community/batteries/pull/1921 --- lake-manifest.json | 6 +++--- lakefile.lean | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index da3bfd52ff5d8e..c2f6be36594aa4 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -61,14 +61,14 @@ "inputRev": "master", "inherited": false, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/batteries", + {"url": "https://github.com/Rob23oba/lean4-batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2ccad61f0f1bb8000458a72fc7ec5df8a7a821b2", + "rev": "dfaa50c3987753635144823e712a54e10dba0671", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "float-deprecated-modules", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.lean b/lakefile.lean index bcdf13405f04bf..1a082154e8c827 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,7 +6,7 @@ open Lake DSL ## Mathlib dependencies on upstream projects -/ -require "leanprover-community" / "batteries" @ git "main" +require "leanprover-community" / "batteries" from git "https://github.com/Rob23oba/lean4-batteries" @ "float-deprecated-modules" require "leanprover-community" / "Qq" @ git "master" require "leanprover-community" / "aesop" @ git "master" From a37805536f74ae4d767a6463e000acbd759fd340 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Wed, 22 Jul 2026 13:14:20 -0400 Subject: [PATCH 2/3] chore: fix imports --- Mathlib/Analysis/Real/Pi/Chudnovsky.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/Real/Pi/Chudnovsky.lean b/Mathlib/Analysis/Real/Pi/Chudnovsky.lean index a1ff2d4c48d30d..8aa136c188f0ac 100644 --- a/Mathlib/Analysis/Real/Pi/Chudnovsky.lean +++ b/Mathlib/Analysis/Real/Pi/Chudnovsky.lean @@ -5,7 +5,7 @@ Authors: Kim Morrison -/ module -meta import Batteries.Data.Rat.Float -- shake: keep (for `#eval` sanity check) +meta import Batteries.Data.Float.Rat -- shake: keep (for `#eval` sanity check) public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan public import Mathlib.MeasureTheory.Integral.Bochner.Basic public import Mathlib.Tactic.Positivity From a3ea17239def63c4c7e6f7721c3cf560df27b15a Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Wed, 22 Jul 2026 13:16:42 -0400 Subject: [PATCH 3/3] chore: update batteries to main --- lake-manifest.json | 6 +++--- lakefile.lean | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index c2f6be36594aa4..d4b1f3146e6c82 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -61,14 +61,14 @@ "inputRev": "master", "inherited": false, "configFile": "lakefile.toml"}, - {"url": "https://github.com/Rob23oba/lean4-batteries", + {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "dfaa50c3987753635144823e712a54e10dba0671", + "rev": "975a7ed3e5ed7838da79d5abddc50df73d0c84af", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "float-deprecated-modules", + "inputRev": "main", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.lean b/lakefile.lean index 1a082154e8c827..bcdf13405f04bf 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,7 +6,7 @@ open Lake DSL ## Mathlib dependencies on upstream projects -/ -require "leanprover-community" / "batteries" from git "https://github.com/Rob23oba/lean4-batteries" @ "float-deprecated-modules" +require "leanprover-community" / "batteries" @ git "main" require "leanprover-community" / "Qq" @ git "master" require "leanprover-community" / "aesop" @ git "master"