chore: bump toolchain to v4.35.0-rc3

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

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
 

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`. -/

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

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. -/

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)`. -/

lake-manifest.json

@@ -1,51 +1,41 @@
-{"version": "1.2.0",
+{"version": "1.3.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover/lean-eval-generator.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2de74049bd91d2c592e7009df8f5e5968599a272",
+   "rev": "a61cd80bc45b16c4f8f900a15f5c80f32e75aad6",
    "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": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204",
-   "name": "Cli",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204",
+   "inputRev": "a61cd80bc45b16c4f8f900a15f5c80f32e75aad6",
    "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 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ddf04cf3949fa556442341e87d47f9f6e6074707",
+   "rev": "29ff470276c725ae01505d55b17148c18fc7dfd3",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e928b72544873815af278d38681b31c0293588e3",
+   "rev": "7e81a29bda33a6b257bd37557a6aa6aebe175d96",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5",
+   "rev": "c643bbb3c24f8a25f9c14e3a6b1ceb13d01f3de1",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "355695d523e41d0554926416cba2a2b3544fbbc9",
+   "rev": "a90fbf7b02ff06a0deebf74088dff9e5fe02c9ea",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -95,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259",
+   "rev": "37b0ba0b26109cf9f9c541f0f9557e50cfa1a3b9",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -105,11 +95,21 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2",
+   "rev": "33131f4fb10067cb3009bf4db615d9680c1ccd6b",
    "name": "batteries",
    "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",

lakefile.toml

@@ -13,22 +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"
-
-[[require]]
-name = "Cli"
-git = "https://github.com/leanprover/lean4-cli"
-rev = "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204"
+rev = "5e0c4e5239cb0a2d86d68a884bf52cfd963fce22"
 
 [[require]]
 name = "lean-eval-generator"
 git = "https://github.com/leanprover/lean-eval-generator.git"
-rev = "2de74049bd91d2c592e7009df8f5e5968599a272"
+rev = "a61cd80bc45b16c4f8f900a15f5c80f32e75aad6"
 
 [[lean_lib]]
 name = "LeanEval"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.34.0
+leanprover/lean4:v4.35.0-rc3