chore: bump toolchain to v4.35.0-rc1

Algorithm/Data/UnionFind.lean

@@ -103,7 +103,7 @@ lemma findAux_snd_getElem (parent : P) (wf : WellFounded fun j k : ι ↦ j ≠
   unfold findAux rootCore; dsimp
   split_ifs with hi
   · exact .inl rfl
-  · obtain (hj | rfl) := decEq i j
+  · obtain (hj | rfl) := Decidable.ne_or_eq i j
     · simp? [hj, - rootCore_parent] says
         simp only [findAux_fst, ne_eq, hj, not_false_eq_true, all_valid,
           getElem_setElem_of_ne]
@@ -223,7 +223,8 @@ lemma setParent_root (parent : P) (size : S) (wf : WellFounded fun i j : ι ↦
     (setParent parent size wf i j hi hj s).root k =
       if rootCore parent wf k = i then j else rootCore parent wf k := by
   unfold root rootCore; dsimp
-  obtain (hk | hk) := decEq parent[k] k <;> simp only [rootCore_parent, hk, ↓reduceIte]
+  obtain (hk | hk) := Decidable.ne_or_eq parent[k] k <;>
+    simp only [rootCore_parent, hk, ↓reduceIte]
   · have hik : i ≠ k := by aesop
     have : (setParent parent size wf i j hi hj s).parent[k] ≠ k := by
       simp [hik, hk]
@@ -259,7 +260,7 @@ lemma link_root (self : UnionFind ι P S) (i j : ι) (hi : self.parent[i] = i)
       else
         self.root k := by
   ext k; unfold link; dsimp
-  obtain (hij | rfl) := decEq i j
+  obtain (hij | rfl) := Decidable.ne_or_eq i j
   · rw [ite_eq_right hij]
     split_ifs with hk hs <;> aesop
   · aesop

lake-manifest.json

@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5ed2965256430c3649e86755f9576b54eca72435",
+   "rev": "c32e1ec0d1eb5237ba344eee50162f45d5b0fc76",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.34.0",
+   "inputRev": "v4.35.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "118aa17ee84656b8bd727fef7c458ee8c833385c",
+   "rev": "16fe28ca7c2e01b71856f7a0a801ea844580f2d5",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ddf04cf3949fa556442341e87d47f9f6e6074707",
+   "rev": "b43172c7f62b95ecd6daa0951602b83eb35182a1",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e928b72544873815af278d38681b31c0293588e3",
+   "rev": "0b9118a4a6d4c752e51f4f731edc09f4cc135f4c",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5",
+   "rev": "af0c1665a9cdb1c90409b52a183113efbb5a4480",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "355695d523e41d0554926416cba2a2b3544fbbc9",
+   "rev": "7938bfd115516f80b260d43faf630c8520471a00",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259",
+   "rev": "21558817bf8b77bab8f4c3081e0062201fd974d2",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2",
+   "rev": "2a71587431553220d08be069a144b8215350e1d6",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204",
+   "rev": "3c7ccd7060887fa478a55e555fae61bbf466c3ba",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.34.0",
+   "inputRev": "v4.35.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "algorithm",

lakefile.lean

@@ -2,7 +2,7 @@ import Lake
 
 open Lake DSL
 
-require "leanprover-community" / "mathlib" @ git "v4.34.0"
+require "leanprover-community" / "mathlib" @ git "v4.35.0-rc1"
 
 abbrev algorithmOnlyLinters : Array LeanOption := #[
   ⟨`linter.mathlibStandardSet, true⟩,
@@ -17,13 +17,17 @@ abbrev algorithmLeanOptions := #[
     algorithmOnlyLinters.map fun s ↦ { s with name := `weak ++ s.name }
 
 package algorithm where
-  fixedToolchain := true
-  platformIndependent := true
-  restoreAllArtifacts := true
   testDriver := "AlgorithmTest"
   lintDriver := "batteries/runLinter"
   lintDriverArgs := #["Algorithm"]
+  -- Run the builtin linting steps in addition to the `lintDriver` set above.
   builtinLint := true
+  -- A version of Algorithm only supports the toolchain it is built with.
+  fixedToolchain := true
+  -- Allow oleans built on Linux CI to be used across platforms.
+  platformIndependent := true
+  -- Algorithm currently expects artifacts to be in the build directory.
+  restoreAllArtifacts := true
 
 @[default_target]
 lean_lib Algorithm where

lean-toolchain

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