Update lean-toolchain for leanprover/lean4#10524

Author: leanprover-community-mathlib4-bot

.github/build.in.yml

@@ -625,6 +625,12 @@ jobs:
         run: |
           lake build Batteries Qq Aesop ProofWidgets Plausible
 
+      - name: build AesopTest (nightly-testing only)
+        # Only run on the mathlib4-nightly-testing repository
+        if: github.repository == 'leanprover-community/mathlib4-nightly-testing'
+        run: |
+          lake build AesopTest
+
       # We no longer run `lean4checker` in regular CI, as it is quite expensive for little benefit.
       # Instead we run it in a cron job on master: see `lean4checker.yml`.
       # Output is posted to the zulip topic

.github/workflows/bors.yml

@@ -635,6 +635,12 @@ jobs:
         run: |
           lake build Batteries Qq Aesop ProofWidgets Plausible
 
+      - name: build AesopTest (nightly-testing only)
+        # Only run on the mathlib4-nightly-testing repository
+        if: github.repository == 'leanprover-community/mathlib4-nightly-testing'
+        run: |
+          lake build AesopTest
+
       # We no longer run `lean4checker` in regular CI, as it is quite expensive for little benefit.
       # Instead we run it in a cron job on master: see `lean4checker.yml`.
       # Output is posted to the zulip topic

.github/workflows/build.yml

@@ -642,6 +642,12 @@ jobs:
         run: |
           lake build Batteries Qq Aesop ProofWidgets Plausible
 
+      - name: build AesopTest (nightly-testing only)
+        # Only run on the mathlib4-nightly-testing repository
+        if: github.repository == 'leanprover-community/mathlib4-nightly-testing'
+        run: |
+          lake build AesopTest
+
       # We no longer run `lean4checker` in regular CI, as it is quite expensive for little benefit.
       # Instead we run it in a cron job on master: see `lean4checker.yml`.
       # Output is posted to the zulip topic

.github/workflows/build_fork.yml

@@ -639,6 +639,12 @@ jobs:
         run: |
           lake build Batteries Qq Aesop ProofWidgets Plausible
 
+      - name: build AesopTest (nightly-testing only)
+        # Only run on the mathlib4-nightly-testing repository
+        if: github.repository == 'leanprover-community/mathlib4-nightly-testing'
+        run: |
+          lake build AesopTest
+
       # We no longer run `lean4checker` in regular CI, as it is quite expensive for little benefit.
       # Instead we run it in a cron job on master: see `lean4checker.yml`.
       # Output is posted to the zulip topic

Archive/Imo/Imo1962Q4.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Lacker, Heather Macbeth
 -/
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
-import Mathlib.Tactic.Polyrith
 
 /-!
 # IMO 1962 Q4

Archive/Imo/Imo2006Q3.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Tian Chen
 -/
 import Mathlib.Analysis.SpecialFunctions.Sqrt
-import Mathlib.Tactic.Polyrith
 
 /-!
 # IMO 2006 Q3

Archive/Imo/Imo2024Q5.lean

@@ -73,7 +73,7 @@ structure Path (N : ℕ) where
   nonempty : cells ≠ []
   head_first_row : (cells.head nonempty).1 = 0
   last_last_row : (cells.getLast nonempty).1 = Fin.last (N + 1)
-  valid_move_seq : cells.Chain' Adjacent
+  valid_move_seq : cells.IsChain Adjacent
 
 /-- The first monster on a path, or `none`. -/
 noncomputable def Path.firstMonster (p : Path N) (m : MonsterData N) : Option (Cell N) :=
@@ -197,7 +197,7 @@ lemma Path.exists_mem_fst_eq (p : Path N) (r : Fin (N + 2)) : ∃ c ∈ p.cells,
       have hi' : i - 1 < i := by omega
       exact of_decide_eq_false (List.not_of_lt_findIdx hi') this
     have ha : Adjacent p.cells[i - 1] p.cells[i] := by
-      convert List.chain'_iff_get.1 p.valid_move_seq (i - 1) ?_
+      convert List.isChain_iff_get.1 p.valid_move_seq (i - 1) ?_
       · simp [Nat.sub_add_cancel hi]
       · omega
     exact ha.le_of_lt h
@@ -223,7 +223,7 @@ lemma Path.findFstEq_fst (p : Path N) (r : Fin (N + 2)) : (p.findFstEq r).1 = r
   simpa using h
 
 lemma find?_eq_eq_find?_le {l : List (Cell N)} {r : Fin (N + 2)} (hne : l ≠ [])
-    (hf : (l.head hne).1 ≤ r) (ha : l.Chain' Adjacent) :
+    (hf : (l.head hne).1 ≤ r) (ha : l.IsChain Adjacent) :
     l.find? (fun c ↦ c.1 = r) = l.find? (fun c ↦ r ≤ c.1) := by
   induction l
   case nil => simp at hne
@@ -234,7 +234,7 @@ lemma find?_eq_eq_find?_le {l : List (Cell N)} {r : Fin (N + 2)} (hne : l ≠ []
       simp only [h, decide_false, Bool.false_eq_true, not_false_eq_true, List.find?_cons_of_neg, h']
       rcases tail with ⟨⟩ | ⟨htail, ttail⟩
       · simp
-      · simp only [List.chain'_cons_cons] at ha
+      · simp only [List.isChain_cons_cons] at ha
         rcases ha with ⟨ha1, ha2⟩
         simp only [List.head_cons] at hf
         simp only [ne_eq, reduceCtorEq, not_false_eq_true, List.head_cons, ha2, true_implies] at hi
@@ -292,7 +292,7 @@ def Path.tail (p : Path N) : Path N where
     · exact p.last_last_row
   valid_move_seq := by
     split_ifs
-    · exact List.Chain'.tail p.valid_move_seq
+    · exact List.IsChain.tail p.valid_move_seq
     · exact p.valid_move_seq
 
 lemma Path.tail_induction {motive : Path N → Prop} (ind : ∀ p, motive p.tail → motive p)
@@ -338,7 +338,8 @@ lemma Path.firstMonster_eq_of_findFstEq_mem {p : Path N} {m : MonsterData N}
   induction p using Path.tail_induction
   case base p h0 =>
     have hl := p.one_lt_length_cells
-    have adj : Adjacent p.cells[0] p.cells[1] := List.chain'_iff_get.1 p.valid_move_seq 0 (by omega)
+    have adj : Adjacent p.cells[0] p.cells[1] :=
+      List.isChain_iff_get.1 p.valid_move_seq 0 (by omega)
     simp_rw [Adjacent, Nat.dist] at adj
     have hc0 : (p.cells[0].1 : ℕ) = 0 := by
       convert Fin.ext_iff.1 p.head_first_row
@@ -384,7 +385,7 @@ lemma Path.findFstEq_fst_sub_one_mem (p : Path N) {r : Fin (N + 2)} (hr : r ≠
     simp [List.getElem_zero, head_first_row, hr] at h
   simp_rw [cells.find?_eq_head_dropWhile_not hd, Option.get_some]
   rw [← cells.takeWhile_append_dropWhile (p := fun c ↦ ! decide (r ≤ c.1)),
-    List.chain'_append] at valid_move_seq
+    List.isChain_append] at valid_move_seq
   have ha := valid_move_seq.2.2
   simp only [List.head?_eq_head hd', List.getLast?_eq_getLast ht, Option.mem_def,
     Option.some.injEq, forall_eq'] at ha
@@ -421,7 +422,7 @@ def Path.ofFn {m : ℕ} (f : Fin m → Cell N) (hm : m ≠ 0)
   last_last_row := by
     simp [Fin.last, List.getLast_ofFn, hl]
   valid_move_seq := by
-    rwa [List.chain'_ofFn]
+    rwa [List.isChain_ofFn]
 
 lemma Path.ofFn_cells {m : ℕ} (f : Fin m → Cell N) (hm : m ≠ 0)
     (hf : (f ⟨0, Nat.pos_of_ne_zero hm⟩).1 = 0)
@@ -446,7 +447,7 @@ def Path.reflect (p : Path N) : Path N where
     rw [List.getLast_map]
     exact p.last_last_row
   valid_move_seq := by
-    refine List.chain'_map_of_chain' _ ?_ p.valid_move_seq
+    refine List.isChain_map_of_isChain _ ?_ p.valid_move_seq
     intro x y h
     simp_rw [Adjacent, Nat.dist, Cell.reflect, Fin.rev] at h ⊢
     omega

Cache/IO.lean

@@ -70,7 +70,7 @@ def CURLBIN :=
 
 /-- leantar version at https://github.com/digama0/leangz -/
 def LEANTARVERSION :=
-  "0.1.15"
+  "0.1.16-pre2"
 
 def EXE := if System.Platform.isWindows then ".exe" else ""
 
@@ -317,6 +317,11 @@ def mkBuildPaths (mod : Name) : CacheM <| List (FilePath × Bool) := do
     (packageDir / LIBDIR / path.withExtension "ilean.hash", true),
     (packageDir / IRDIR  / path.withExtension "c", true),
     (packageDir / IRDIR  / path.withExtension "c.hash", true),
+     -- this is needed for packages using the module system:
+    (packageDir / LIBDIR / path.withExtension "olean.private", false),
+    (packageDir / LIBDIR / path.withExtension "olean.private.hash", false),
+    (packageDir / LIBDIR / path.withExtension "olean.server", false),
+    (packageDir / LIBDIR / path.withExtension "olean.server.hash", false),
     (packageDir / LIBDIR / path.withExtension "extra", false)]
 
 /-- Check that all required build files exist. -/

Cache/Requests.lean

@@ -440,23 +440,41 @@ def getProofWidgets (buildDir : FilePath) : IO Unit := do
     -- Check if the ProofWidgets build is out-of-date via `lake`.
     -- This is done through Lake as cache has no simple heuristic
     -- to determine whether the ProofWidgets JS is out-of-date.
-    let exitCode ← (← IO.Process.spawn {cmd := "lake", args := #["-q", "build", "--no-build", "proofwidgets:release"]}).wait
-    if exitCode == 0 then -- up-to-date
+    let out ← IO.Process.output
+      {cmd := "lake", args := #["-v", "build", "--no-build", "proofwidgets:release"]}
+    if out.exitCode == 0 then -- up-to-date
       return
-    else if exitCode == 3 then -- needs fetch (`--no-build` triggered)
+    else if out.exitCode == 3 then -- needs fetch (`--no-build` triggered)
       pure ()
     else
-      throw <| IO.userError s!"Failed to validate ProofWidgets cloud release: lake failed with error code {exitCode}"
+      printLakeOutput out
+      throw <| IO.userError s!"Failed to validate ProofWidgets cloud release: \
+        lake failed with error code {out.exitCode}"
   -- Download and unpack the ProofWidgets cloud release (for its `.js` files)
-  let exitCode ← (← IO.Process.spawn {cmd := "lake", args := #["-q", "build", "proofwidgets:release"]}).wait
-  if exitCode != 0 then
-    throw <| IO.userError s!"Failed to fetch ProofWidgets cloud release: lake failed with error code {exitCode}"
+  IO.print "Fetching ProofWidgets cloud release..."
+  let out ← IO.Process.output
+     {cmd := "lake", args := #["-v", "build", "proofwidgets:release"]}
+  if out.exitCode == 0 then
+    IO.println " done!"
+  else
+    IO.print "\n"
+    printLakeOutput out
+    throw <| IO.userError s!"Failed to fetch ProofWidgets cloud release: \
+      lake failed with error code {out.exitCode}"
   -- Prune non-JS ProofWidgets files (e.g., `olean`, `.c`)
   try
     IO.FS.removeDirAll (buildDir / "lib")
     IO.FS.removeDirAll (buildDir / "ir")
   catch e =>
     throw <| IO.userError s!"Failed to prune ProofWidgets cloud release: {e}"
+where
+  printLakeOutput out := do
+    unless out.stdout.isEmpty do
+      IO.eprintln "lake stdout:"
+      IO.eprint out.stderr
+    unless out.stderr.isEmpty do
+      IO.eprintln "lake stderr:"
+      IO.eprint out.stderr
 
 /-- Downloads missing files, and unpacks files. -/
 def getFiles