From cf9dadacc3d7d116ac52c1eafd97eb3d932f9d75 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 28 Sep 2026 11:20:55 +1000 Subject: [PATCH 1/4] chore: bump toolchain to v4.35.0-rc3 Follow TauCeti to v4.35.0-rc3. lean-eval downloads TauCeti's published build outputs rather than compiling TauCeti, and Lake only reuses them when this project pins the same toolchain and Mathlib revision as the pinned TauCeti commit, so all three move together: TauCeti to 522706e, Mathlib to the 5e0c4e5 that commit uses, and the toolchain to v4.35.0-rc3. Cli moves to 843844f for the same reason it was pinned at Mathlib's revision before: a project pinning a different Cli than Mathlib makes `lake exe cache get` compute wrong hashes, and it failed to fetch until this was realigned. `generated/` is untouched. The generator reads the root `lean-toolchain` and `regenerate-main.yml` runs on merge to main when that file changes, so the project toolchains follow from the trusted regenerator. `scripts/fetch_dependency_caches.sh --restore .` passes, so TauCeti's outputs are genuinely being reused rather than silently recompiled, and `lake build LeanEval EvalTools` is clean. Co-Authored-By: Claude Opus 5 --- lake-manifest.json | 28 ++++++++++++++-------------- lakefile.toml | 6 +++--- lean-toolchain | 2 +- 3 files changed, 18 insertions(+), 18 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 6e78c9e9..3d85feff 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,4 +1,4 @@ -{"version": "1.2.0", +{"version": "1.3.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover/lean-eval-generator.git", @@ -15,37 +15,37 @@ "type": "git", "subDir": null, "scope": "", - "rev": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204", + "rev": "843844fa601dd56767b1eb22b7ada5b64d5e567a", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204", + "inputRev": "843844fa601dd56767b1eb22b7ada5b64d5e567a", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, "scope": "", - "rev": "db1c5741da0acf96c97584de6ccf0e3bfbc0ae99", + "rev": "5e0c4e5239cb0a2d86d68a884bf52cfd963fce22", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "db1c5741da0acf96c97584de6ccf0e3bfbc0ae99", + "inputRev": "5e0c4e5239cb0a2d86d68a884bf52cfd963fce22", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/TauCetiProject/TauCeti", "type": "git", "subDir": null, "scope": "", - "rev": "23bfe9bc742f8713b58ce40b155f994848ae8a5e", + "rev": "522706e83ca349c3d6bde045e56778d17354ae8d", "name": "TauCeti", "manifestFile": "lake-manifest.json", - "inputRev": "23bfe9bc742f8713b58ce40b155f994848ae8a5e", + "inputRev": "522706e83ca349c3d6bde045e56778d17354ae8d", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "118aa17ee84656b8bd727fef7c458ee8c833385c", + "rev": "fb13df72ecefd8ddbf9291021d7f33a8673eb57b", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ddf04cf3949fa556442341e87d47f9f6e6074707", + "rev": "29ff470276c725ae01505d55b17148c18fc7dfd3", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e928b72544873815af278d38681b31c0293588e3", + "rev": "7e81a29bda33a6b257bd37557a6aa6aebe175d96", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5", + "rev": "c643bbb3c24f8a25f9c14e3a6b1ceb13d01f3de1", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "355695d523e41d0554926416cba2a2b3544fbbc9", + "rev": "a90fbf7b02ff06a0deebf74088dff9e5fe02c9ea", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -95,7 +95,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259", + "rev": "37b0ba0b26109cf9f9c541f0f9557e50cfa1a3b9", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -105,7 +105,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2", + "rev": "33131f4fb10067cb3009bf4db615d9680c1ccd6b", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.toml b/lakefile.toml index 3f7f8af5..56274a44 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -13,17 +13,17 @@ autoImplicit = false [[require]] name = "TauCeti" git = "https://github.com/TauCetiProject/TauCeti" -rev = "23bfe9bc742f8713b58ce40b155f994848ae8a5e" +rev = "522706e83ca349c3d6bde045e56778d17354ae8d" [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4.git" -rev = "db1c5741da0acf96c97584de6ccf0e3bfbc0ae99" +rev = "5e0c4e5239cb0a2d86d68a884bf52cfd963fce22" [[require]] name = "Cli" git = "https://github.com/leanprover/lean4-cli" -rev = "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204" +rev = "843844fa601dd56767b1eb22b7ada5b64d5e567a" [[require]] name = "lean-eval-generator" diff --git a/lean-toolchain b/lean-toolchain index 12359f92..f0e00b33 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.34.0 +leanprover/lean4:v4.35.0-rc3 From bfc79d7c556468db9687285d3fca8a140be63b98 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 28 Sep 2026 11:46:56 +1000 Subject: [PATCH 2/4] chore: drop the explicit Cli require and repin the generator Take Cli transitively from Mathlib rather than pinning it here. It resolves to the same commit, but via Mathlib's own tag, so the two can no longer drift -- which is what broke `lake exe cache get` when Mathlib's Cli moved. Repin lean-eval-generator at the fix for the String API that v4.35.0-rc3 removes. `String.trim` and `String.dropRight` are gone, and because a Lake dependency builds with the root project's toolchain, the `lean-eval` executable would not build at this toolchain without it. `lake build lean-eval` is clean and the three `lake exe lean-eval` validators CI runs all pass. Co-Authored-By: Claude Opus 5 --- lake-manifest.json | 24 ++++++++++++------------ lakefile.toml | 7 +------ 2 files changed, 13 insertions(+), 18 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 3d85feff..2bf4a650 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,20 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "2de74049bd91d2c592e7009df8f5e5968599a272", + "rev": "f06007733e74a859b4d20665404e49eaa80454a6", "name": "«lean-eval-generator»", "manifestFile": "lake-manifest.json", - "inputRev": "2de74049bd91d2c592e7009df8f5e5968599a272", - "inherited": false, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "scope": "", - "rev": "843844fa601dd56767b1eb22b7ada5b64d5e567a", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "843844fa601dd56767b1eb22b7ada5b64d5e567a", + "inputRev": "f06007733e74a859b4d20665404e49eaa80454a6", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4.git", @@ -110,6 +100,16 @@ "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "843844fa601dd56767b1eb22b7ada5b64d5e567a", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.35.0-rc3", + "inherited": true, "configFile": "lakefile.toml"}], "name": "«lean-eval»", "lakeDir": ".lake", diff --git a/lakefile.toml b/lakefile.toml index 56274a44..c76f5737 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -20,15 +20,10 @@ name = "mathlib" git = "https://github.com/leanprover-community/mathlib4.git" rev = "5e0c4e5239cb0a2d86d68a884bf52cfd963fce22" -[[require]] -name = "Cli" -git = "https://github.com/leanprover/lean4-cli" -rev = "843844fa601dd56767b1eb22b7ada5b64d5e567a" - [[require]] name = "lean-eval-generator" git = "https://github.com/leanprover/lean-eval-generator.git" -rev = "2de74049bd91d2c592e7009df8f5e5968599a272" +rev = "f06007733e74a859b4d20665404e49eaa80454a6" [[lean_lib]] name = "LeanEval" From e7690ad37220b3718ddc36f8ebd2a5331d295243 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 28 Sep 2026 14:01:02 +1000 Subject: [PATCH 3/4] chore: repin lean-eval-generator at its merged commit The previous commit pinned the branch commit of the v4.35.0-rc3 String API fix; point at the commit that landed on the generator's main instead. Co-Authored-By: Claude Opus 5 --- lake-manifest.json | 4 ++-- lakefile.toml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 2bf4a650..af237b8d 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "f06007733e74a859b4d20665404e49eaa80454a6", + "rev": "a61cd80bc45b16c4f8f900a15f5c80f32e75aad6", "name": "«lean-eval-generator»", "manifestFile": "lake-manifest.json", - "inputRev": "f06007733e74a859b4d20665404e49eaa80454a6", + "inputRev": "a61cd80bc45b16c4f8f900a15f5c80f32e75aad6", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4.git", diff --git a/lakefile.toml b/lakefile.toml index c76f5737..cfb065b7 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -23,7 +23,7 @@ rev = "5e0c4e5239cb0a2d86d68a884bf52cfd963fce22" [[require]] name = "lean-eval-generator" git = "https://github.com/leanprover/lean-eval-generator.git" -rev = "f06007733e74a859b4d20665404e49eaa80454a6" +rev = "a61cd80bc45b16c4f8f900a15f5c80f32e75aad6" [[lean_lib]] name = "LeanEval" From 4de5879fd5e671d95c08bed8e191ac1e959e363a Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 28 Sep 2026 14:01:10 +1000 Subject: [PATCH 4/4] fix: adapt six catalog modules to v4.35.0-rc3 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Five modules pass a coefficient category to `singularHomologyFunctor` or `singularChainComplexFunctor` and leave its universe to be inferred from the coefficient object. At v4.35.0-rc3, instance search for `∀ J, HasColimitsOfShape (Discrete J) C` runs while that universe is still a metavariable, and searching with one exhausts the 20000 `synthInstance` heartbeats. Writing the universe the coefficient object already forces -- `ModuleCat.{0} ℝ`, `ModuleCat.{0} ℤ`, `AddCommGrpCat.{0}` -- lets search succeed immediately. `HoneycombConnectiveConstant.walkCount_six` reduces a `Decidable` instance over all `3 ^ 6` direction words. Elaborator reduction now needs 556236 heartbeats, well over the default 200000, so evaluate in the kernel instead: `decide +kernel` costs 37538 heartbeats and half the wall time, and no longer needs the `maxRecDepth` bump. These modules sit outside the `LeanEval` library target, so only `lake exe lean-eval check-problem-build` builds them; it now reports the whole catalog clean. Co-Authored-By: Claude Opus 5 --- LeanEval/Combinatorics/HoneycombConnectiveConstant.lean | 8 +++++--- LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean | 4 ++-- LeanEval/Geometry/MorseInequalities.lean | 2 +- LeanEval/Geometry/WeakMorseInequality.lean | 2 +- LeanEval/Topology/AsphericalHomologySphere.lean | 2 +- LeanEval/Topology/Hurewicz.lean | 2 +- 6 files changed, 11 insertions(+), 9 deletions(-) diff --git a/LeanEval/Combinatorics/HoneycombConnectiveConstant.lean b/LeanEval/Combinatorics/HoneycombConnectiveConstant.lean index 9863fc8a..6484168b 100644 --- a/LeanEval/Combinatorics/HoneycombConnectiveConstant.lean +++ b/LeanEval/Combinatorics/HoneycombConnectiveConstant.lean @@ -93,10 +93,12 @@ three-step self-avoiding walks from a fixed honeycomb vertex. -/ theorem walkCount_three : walkCount 3 = 12 := by decide -set_option maxRecDepth 10000 in -/-- At six steps the first hexagonal cycle appears; the standard count is `90`. -/ +/-- At six steps the first hexagonal cycle appears; the standard count is `90`. +The `+kernel` evaluation keeps the enumeration of all `3 ^ 6` direction words in +the kernel; reducing it in the elaborator costs several times the default +heartbeat budget. -/ theorem walkCount_six : walkCount 6 = 90 := by - decide + decide +kernel /-- **Duminil-Copin-Smirnov honeycomb connective-constant theorem.** The exponential growth rate of the number of self-avoiding walks is diff --git a/LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean b/LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean index d6facad1..b850fac3 100644 --- a/LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean +++ b/LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean @@ -369,14 +369,14 @@ abbrev freeLightCondAbOfTopFunctor : TopCat ⥤ LightCondAb := abelian group. -/ abbrev singularHomologyLightCondAb (X : TopCat) (n : ℕ) : LightCondAb := (LightCondensed.discrete (ModuleCat ℤ)).obj - (((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) n).obj (ModuleCat.of ℤ ℤ)).obj X) + (((AlgebraicTopology.singularHomologyFunctor (ModuleCat.{0} ℤ) n).obj (ModuleCat.of ℤ ℤ)).obj X) /-- The integral singular chain complex of a topological space, viewed as a cochain complex of light condensed abelian groups by applying the discrete functor degreewise and placing homological chain degree `n` in cohomological degree `-n`. -/ abbrev singularChainsLightCondAbComplexFunctor : TopCat ⥤ CochainComplex LightCondAb ℤ := - ((AlgebraicTopology.singularChainComplexFunctor (ModuleCat ℤ)).obj (ModuleCat.of ℤ ℤ)) ⋙ + ((AlgebraicTopology.singularChainComplexFunctor (ModuleCat.{0} ℤ)).obj (ModuleCat.of ℤ ℤ)) ⋙ (LightCondensed.discrete (ModuleCat ℤ)).mapHomologicalComplex (ComplexShape.down ℕ) ⋙ ComplexShape.embeddingDownNat.extendFunctor LightCondAb diff --git a/LeanEval/Geometry/MorseInequalities.lean b/LeanEval/Geometry/MorseInequalities.lean index 0c7606c1..c043b60c 100644 --- a/LeanEval/Geometry/MorseInequalities.lean +++ b/LeanEval/Geometry/MorseInequalities.lean @@ -90,7 +90,7 @@ noncomputable def morseCount coefficients. -/ noncomputable def bettiNumber (M : Type) [TopologicalSpace M] (k : ℕ) : ℕ := Module.finrank ℝ - (((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℝ) k).obj + (((AlgebraicTopology.singularHomologyFunctor (ModuleCat.{0} ℝ) k).obj (ModuleCat.of ℝ ℝ)).obj (TopCat.of M)) /-- The alternating partial sum `∑_{j=0}^{k} (−1)^{k−j} a_j`. -/ diff --git a/LeanEval/Geometry/WeakMorseInequality.lean b/LeanEval/Geometry/WeakMorseInequality.lean index 5aea130c..5a70bcff 100644 --- a/LeanEval/Geometry/WeakMorseInequality.lean +++ b/LeanEval/Geometry/WeakMorseInequality.lean @@ -87,7 +87,7 @@ noncomputable def morseCount /-- `b_k(M) := dim_ℝ H_k(M; ℝ)`. -/ noncomputable def bettiNumber (M : Type) [TopologicalSpace M] (k : ℕ) : ℕ := Module.finrank ℝ - (((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℝ) k).obj + (((AlgebraicTopology.singularHomologyFunctor (ModuleCat.{0} ℝ) k).obj (ModuleCat.of ℝ ℝ)).obj (TopCat.of M)) /-- **Weak Morse inequalities.** For a Morse function `f` on a closed diff --git a/LeanEval/Topology/AsphericalHomologySphere.lean b/LeanEval/Topology/AsphericalHomologySphere.lean index fbe2972c..a4875d74 100644 --- a/LeanEval/Topology/AsphericalHomologySphere.lean +++ b/LeanEval/Topology/AsphericalHomologySphere.lean @@ -59,7 +59,7 @@ attribute [instance] Closed4Manifold.topology Closed4Manifold.t2 /-- `Hₖ(X; ℤ)`, the `k`-th singular homology with integer coefficients, as an object of `ModuleCat ℤ`. -/ noncomputable def intHomology (k : ℕ) (X : TopCat) : ModuleCat ℤ := - ((singularHomologyFunctor (ModuleCat ℤ) k).obj (ModuleCat.of ℤ ℤ)).obj X + ((singularHomologyFunctor (ModuleCat.{0} ℤ) k).obj (ModuleCat.of ℤ ℤ)).obj X /-- `M` is **aspherical**: every higher homotopy group vanishes at every basepoint. -/ diff --git a/LeanEval/Topology/Hurewicz.lean b/LeanEval/Topology/Hurewicz.lean index fa7860f7..42eded5d 100644 --- a/LeanEval/Topology/Hurewicz.lean +++ b/LeanEval/Topology/Hurewicz.lean @@ -18,7 +18,7 @@ open CategoryTheory AlgebraicTopology /-- Integral singular homology in degree `n`, as an additive group. -/ noncomputable abbrev IntegralHomology (n : ℕ) (X : Type) [TopologicalSpace X] : AddCommGrpCat := - ((singularHomologyFunctor AddCommGrpCat n).obj (AddCommGrpCat.of ℤ)).obj (TopCat.of X) + ((singularHomologyFunctor AddCommGrpCat.{0} n).obj (AddCommGrpCat.of ℤ)).obj (TopCat.of X) /-- **Hurewicz (n = 1).** For a path-connected space `X`, `H₁(X;ℤ)` is the abelianization of `π₁(X, x)`. -/