fix: add checkSystem and withIncRecDepth to withAutoBoundImplicit

Fix stack overflow crash.

Closes #4117

The fix can be improved: we could try to avoid creating hundreds of
auto implicits before failing.

.github/workflows/ci.yml

@@ -6,6 +6,7 @@ on:
     tags:
       - '*'
   pull_request:
+    types: [opened, synchronize, reopened, labeled]
   merge_group:
   schedule:
     - cron: '0 7 * * *'  # 8AM CET/11PM PT
@@ -40,18 +41,12 @@ jobs:
     steps:
       - name: Run quick CI?
         id: set-quick
-        # We do not use github.event.pull_request.labels.*.name here because
-        # re-running a run does not update that list, and we do want to be able to
-        # rerun the workflow run after settings the `full-ci` label.
-        run: |
-          if [ "${{ github.event_name }}" == 'pull_request' ]
-          then
-            echo "quick=$(gh api repos/${{ github.repository_owner }}/${{ github.event.repository.name }}/pulls/${{ github.event.pull_request.number }} --jq '.labels | any(.name == "full-ci") | not')" >> "$GITHUB_OUTPUT"
-          else
-            echo "quick=false" >> "$GITHUB_OUTPUT"
-          fi
         env:
-          GH_TOKEN: ${{ github.token }}
+          quick: ${{
+            github.event_name == 'pull_request' && !contains( github.event.pull_request.labels.*.name, 'full-ci')
+           }}
+        run: |
+          echo "quick=${{env.quick}}" >> "$GITHUB_OUTPUT"
 
       - name: Configure build matrix
         id: set-matrix

.github/workflows/nix-ci.yml

@@ -6,6 +6,7 @@ on:
     tags:
       - '*'
   pull_request:
+    types: [opened, synchronize, reopened, labeled]
   merge_group:
 
 concurrency:

.github/workflows/restart-on-label.yml

@@ -1,31 +0,0 @@
-name: Restart by label
-on:
-  pull_request_target:
-    types:
-      - unlabeled
-      - labeled
-jobs:
-  restart-on-label:
-    runs-on: ubuntu-latest
-    if: contains(github.event.label.name, 'full-ci')
-    steps:
-    - run: |
-        # Finding latest CI workflow run on current pull request
-        # (unfortunately cannot search by PR number, only base branch,
-        # and that is't even unique given PRs from forks, but the risk
-        # of confusion is low and the danger is mild)
-        run_id=$(gh run list -e pull_request -b "$head_ref" --workflow 'CI' --limit 1 \
-          --limit 1 --json databaseId --jq '.[0].databaseId')
-        echo "Run id: ${run_id}"
-        gh run view "$run_id"
-        echo "Cancelling (just in case)"
-        gh run cancel "$run_id" || echo "(failed)"
-        echo "Waiting for 10s"
-        sleep 10
-        echo "Rerunning"
-        gh run rerun "$run_id"
-      shell: bash
-      env:
-        head_ref: ${{ github.head_ref }}
-        GH_TOKEN: ${{ github.token }}
-        GH_REPO: ${{ github.repository }}

RELEASES.md

@@ -11,18 +11,7 @@ of each version.
 v4.9.0 (development in progress)
 ---------
 
-* Functions defined by well-founded recursion are now marked as
-  `@[irreducible]`, which should prevent expensive and often unfruitful
-  unfolding of such definitions.
-
-  Existing proofs that hold by definitional equality (e.g. `rfl`) can be
-  rewritten to explictly unfold the function definition (using `simp`,
-  `unfold`, `rw`), or the recursive function can be temporariliy made
-  semireducible (using `unseal f in` before the command) or the function
-  definition itself can be marked as `@[semireducible]` to get the previous
-  behavor.
-
-v4.8.0
+v4.8.0 
 ---------
 
 * **Executables configured with `supportInterpreter := true` on Windows should now be run via `lake exe` to function properly.**

src/Init.lean

@@ -34,4 +34,3 @@ import Init.BinderPredicates
 import Init.Ext
 import Init.Omega
 import Init.MacroTrace
-import Init.Grind

src/Init/Data/Array/Subarray.lean

@@ -15,13 +15,13 @@ structure Subarray (α : Type u)  where
   start_le_stop : start ≤ stop
   stop_le_array_size : stop ≤ array.size
 
-@[deprecated Subarray.array (since := "2024-04-13")]
+@[deprecated Subarray.array]
 abbrev Subarray.as (s : Subarray α) : Array α := s.array
 
-@[deprecated Subarray.start_le_stop (since := "2024-04-13")]
+@[deprecated Subarray.start_le_stop]
 theorem Subarray.h₁ (s : Subarray α) : s.start ≤ s.stop := s.start_le_stop
 
-@[deprecated Subarray.stop_le_array_size (since := "2024-04-13")]
+@[deprecated Subarray.stop_le_array_size]
 theorem Subarray.h₂ (s : Subarray α) : s.stop ≤ s.array.size := s.stop_le_array_size
 
 namespace Subarray

src/Init/Data/BitVec/Basic.lean

@@ -34,8 +34,7 @@ structure BitVec (w : Nat) where
   O(1), because we use `Fin` as the internal representation of a bitvector. -/
   toFin : Fin (2^w)
 
-@[deprecated (since := "2024-04-12")]
-protected abbrev Std.BitVec := _root_.BitVec
+@[deprecated] protected abbrev Std.BitVec := _root_.BitVec
 
 -- We manually derive the `DecidableEq` instances for `BitVec` because
 -- we want to have builtin support for bit-vector literals, and we
@@ -74,7 +73,7 @@ protected def toNat (a : BitVec n) : Nat := a.toFin.val
 /-- Return the bound in terms of toNat. -/
 theorem isLt (x : BitVec w) : x.toNat < 2^w := x.toFin.isLt
 
-@[deprecated isLt (since := "2024-03-12")]
+@[deprecated isLt]
 theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.isLt
 
 /-- Theorem for normalizing the bit vector literal representation. -/

src/Init/Data/BitVec/Bitblast.lean

@@ -184,18 +184,4 @@ theorem bit_neg_eq_neg (x : BitVec w) : -x = (adc (((iunfoldr (fun (i : Fin w) c
     simp [← sub_toAdd, BitVec.sub_add_cancel]
   · simp [bit_not_testBit x _]
 
-/-! ### Inequalities (le / lt) -/
-
-theorem ult_eq_not_carry (x y : BitVec w) : x.ult y = !carry w x (~~~y) true := by
-  simp only [BitVec.ult, carry, toNat_mod_cancel, toNat_not, toNat_true, ge_iff_le, ← decide_not,
-    Nat.not_le, decide_eq_decide]
-  rw [Nat.mod_eq_of_lt (by omega)]
-  omega
-
-theorem ule_eq_not_ult (x y : BitVec w) : x.ule y = !y.ult x := by
-  simp [BitVec.ule, BitVec.ult, ← decide_not]
-
-theorem ule_eq_carry (x y : BitVec w) : x.ule y = carry w y (~~~x) true := by
-  simp [ule_eq_not_ult, ult_eq_not_carry]
-
 end BitVec

src/Init/Data/BitVec/Lemmas.lean

@@ -146,8 +146,7 @@ theorem getLsb_ofNat (n : Nat) (x : Nat) (i : Nat) :
   getLsb (x#n) i = (i < n && x.testBit i) := by
   simp [getLsb, BitVec.ofNat, Fin.val_ofNat']
 
-@[simp, deprecated toNat_ofNat (since := "2024-02-22")]
-theorem toNat_zero (n : Nat) : (0#n).toNat = 0 := by trivial
+@[simp, deprecated toNat_ofNat] theorem toNat_zero (n : Nat) : (0#n).toNat = 0 := by trivial
 
 @[simp] theorem getLsb_zero : (0#w).getLsb i = false := by simp [getLsb]
 
@@ -246,12 +245,6 @@ theorem eq_of_toInt_eq {i j : BitVec n} : i.toInt = j.toInt → i = j := by
   have _jlt := j.isLt
   split <;> split <;> omega
 
-theorem toInt_inj (x y : BitVec n) : x.toInt = y.toInt ↔ x = y :=
-  Iff.intro eq_of_toInt_eq (congrArg BitVec.toInt)
-
-theorem toInt_ne (x y : BitVec n) : x.toInt ≠ y.toInt ↔ x ≠ y  := by
-  rw [Ne, toInt_inj]
-
 @[simp] theorem toNat_ofInt {n : Nat} (i : Int) :
   (BitVec.ofInt n i).toNat = (i % (2^n : Nat)).toNat := by
   unfold BitVec.ofInt
@@ -609,17 +602,6 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
     (shiftLeftZeroExtend x i).msb = x.msb := by
   simp [shiftLeftZeroExtend_eq, BitVec.msb]
 
-theorem shiftLeft_shiftLeft {w : Nat} (x : BitVec w) (n m : Nat) :
-    (x <<< n) <<< m = x <<< (n + m) := by
-  ext i
-  simp only [getLsb_shiftLeft, Fin.is_lt, decide_True, Bool.true_and]
-  rw [show i - (n + m) = (i - m - n) by omega]
-  cases h₂ : decide (i < m) <;>
-  cases h₃ : decide (i - m < w) <;>
-  cases h₄ : decide (i - m < n) <;>
-  cases h₅ : decide (i < n + m) <;>
-    simp at * <;> omega
-
 /-! ### ushiftRight -/
 
 @[simp, bv_toNat] theorem toNat_ushiftRight (x : BitVec n) (i : Nat) :
@@ -705,11 +687,6 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
   simp only [getLsb_append, cond_eq_if]
   split <;> simp [*]
 
-theorem shiftRight_shiftRight (w : Nat) (x : BitVec w) (n m : Nat) :
-    (x >>> n) >>> m = x >>> (n + m) := by
-  ext i
-  simp [Nat.add_assoc n m i]
-
 /-! ### rev -/
 
 theorem getLsb_rev (x : BitVec w) (i : Fin w) :

src/Init/Data/Bool.lean

@@ -360,8 +360,7 @@ def toNat (b:Bool) : Nat := cond b 1 0
 theorem toNat_le (c : Bool) : c.toNat ≤ 1 := by
   cases c <;> trivial
 
-@[deprecated toNat_le (since := "2024-02-23")]
-abbrev toNat_le_one := toNat_le
+@[deprecated toNat_le] abbrev toNat_le_one := toNat_le
 
 theorem toNat_lt (b : Bool) : b.toNat < 2 :=
   Nat.lt_succ_of_le (toNat_le _)

src/Init/Data/Fin/Lemmas.lean

@@ -11,9 +11,6 @@ import Init.ByCases
 import Init.Conv
 import Init.Omega
 
--- Remove after the next stage0 update
-set_option allowUnsafeReducibility true
-
 namespace Fin
 
 /-- If you actually have an element of `Fin n`, then the `n` is always positive -/
@@ -62,8 +59,7 @@ theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
 @[simp] theorem val_ofNat' (a : Nat) (is_pos : n > 0) :
   (Fin.ofNat' a is_pos).val = a % n := rfl
 
-@[deprecated ofNat'_zero_val (since := "2024-02-22")]
-theorem ofNat'_zero_val : (Fin.ofNat' 0 h).val = 0 := Nat.zero_mod _
+@[deprecated ofNat'_zero_val] theorem ofNat'_zero_val : (Fin.ofNat' 0 h).val = 0 := Nat.zero_mod _
 
 @[simp] theorem mod_val (a b : Fin n) : (a % b).val = a.val % b.val :=
   rfl

src/Init/Data/Int/DivModLemmas.lean

@@ -14,8 +14,6 @@ import Init.RCases
 # Lemmas about integer division needed to bootstrap `omega`.
 -/
 
--- Remove after the next stage0 update
-set_option allowUnsafeReducibility true
 
 open Nat (succ)
 
@@ -144,14 +142,12 @@ theorem eq_one_of_mul_eq_one_left {a b : Int} (H : 0 ≤ b) (H' : a * b = 1) : b
   | ofNat _ => show ofNat _ = _ by simp
   | -[_+1] => show -ofNat _ = _ by simp
 
-unseal Nat.div in
 @[simp] protected theorem div_zero : ∀ a : Int, div a 0 = 0
   | ofNat _ => show ofNat _ = _ by simp
   | -[_+1] => rfl
 
 @[simp] theorem zero_fdiv (b : Int) : fdiv 0 b = 0 := by cases b <;> rfl
 
-unseal Nat.div in
 @[simp] protected theorem fdiv_zero : ∀ a : Int, fdiv a 0 = 0
   | 0      => rfl
   | succ _ => rfl
@@ -769,13 +765,11 @@ theorem ediv_eq_ediv_of_mul_eq_mul {a b c d : Int}
   | (n:Nat) => congrArg ofNat (Nat.div_one _)
   | -[n+1] => by simp [Int.div, neg_ofNat_succ]; rfl
 
-unseal Nat.div in
 @[simp] protected theorem div_neg : ∀ a b : Int, a.div (-b) = -(a.div b)
   | ofNat m, 0 => show ofNat (m / 0) = -↑(m / 0) by rw [Nat.div_zero]; rfl
   | ofNat m, -[n+1] | -[m+1], succ n => (Int.neg_neg _).symm
   | ofNat m, succ n | -[m+1], 0 | -[m+1], -[n+1] => rfl
 
-unseal Nat.div in
 @[simp] protected theorem neg_div : ∀ a b : Int, (-a).div b = -(a.div b)
   | 0, n => by simp [Int.neg_zero]
   | succ m, (n:Nat) | -[m+1], 0 | -[m+1], -[n+1] => rfl
@@ -944,7 +938,6 @@ theorem fdiv_nonneg {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a.fdiv b :
   match a, b, eq_ofNat_of_zero_le Ha, eq_ofNat_of_zero_le Hb with
   | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => ofNat_fdiv .. ▸ ofNat_zero_le _
 
-unseal Nat.div in
 theorem fdiv_nonpos : ∀ {a b : Int}, 0 ≤ a → b ≤ 0 → a.fdiv b ≤ 0
   | 0, 0, _, _ | 0, -[_+1], _, _ | succ _, 0, _, _ | succ _, -[_+1], _, _ => ⟨_⟩
 

src/Init/Data/List/Lemmas.lean

@@ -777,6 +777,7 @@ theorem exists_cons_of_length_succ :
     ∀ {l : List α}, l.length = n + 1 → ∃ h t, l = h :: t
   | _::_, _ => ⟨_, _, rfl⟩
 
+@[simp]
 theorem length_pos {l : List α} : 0 < length l ↔ l ≠ [] :=
   Nat.pos_iff_ne_zero.trans (not_congr length_eq_zero)
 

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -50,10 +50,7 @@ noncomputable def div2Induction {motive : Nat → Sort u}
       apply hyp
       exact Nat.div_lt_self n_pos (Nat.le_refl _)
 
-@[simp] theorem zero_and (x : Nat) : 0 &&& x = 0 := by
-  simp only [HAnd.hAnd, AndOp.and, land]
-  unfold bitwise
-  simp
+@[simp] theorem zero_and (x : Nat) : 0 &&& x = 0 := by rfl
 
 @[simp] theorem and_zero (x : Nat) : x &&& 0 = 0 := by
   simp only [HAnd.hAnd, AndOp.and, land]

src/Init/Data/Nat/Div.lean

@@ -82,34 +82,28 @@ decreasing_by apply div_rec_lemma; assumption
 
 @[extern "lean_nat_mod"]
 protected def mod : @& Nat → @& Nat → Nat
-  /-
-  Nat.modCore is defined by well-founded recursion and thus irreducible. Nevertheless it is
-  desireable if trivial `Nat.mod` calculations, namely
-  * `Nat.mod 0 m` for all `m`
-  * `Nat.mod n (m+n)` for concrete literals `n`
-  reduce definitionally.
+  /- These four cases are not needed mathematically, they are just special cases of the
+  general case. However, it makes `0 % n = 0` etc. true definitionally rather than just
+  propositionally.
   This property is desirable for `Fin n` literals, as it means `(ofNat 0 : Fin n).val = 0` by
-  definition.
-   -/
+  definition. This was true in lean3 and it simplified things for mathlib if it remains true. -/
   | 0, _ => 0
-  | n@(_ + 1), m =>
-    if m ≤ n -- NB: if n < m does not reduce as well as `m ≤ n`!
-    then Nat.modCore n m
-    else n
+  | 1, 0 => 0
+  | 1, 1 => 0
+  | 1, (_+2) => 1
+  | x@(_ + 2), y => Nat.modCore x y
 
 instance instMod : Mod Nat := ⟨Nat.mod⟩
 
-protected theorem modCore_eq_mod (n m : Nat) : Nat.modCore n m = n % m := by
-  show Nat.modCore n m = Nat.mod n m
-  match n, m with
-  | 0, _ =>
+protected theorem modCore_eq_mod (x y : Nat) : Nat.modCore x y = x % y := by
+  match x, y with
+  | 0, y =>
     rw [Nat.modCore]
     exact if_neg fun ⟨hlt, hle⟩ => Nat.lt_irrefl _ (Nat.lt_of_lt_of_le hlt hle)
-  | (_ + 1), _ =>
-    rw [Nat.mod]; dsimp
-    refine iteInduction (fun _ => rfl) (fun h => ?false) -- cannot use `split` this early yet
-    rw [Nat.modCore]
-    exact if_neg fun ⟨_hlt, hle⟩ => h hle
+  | 1, 0 => rw [Nat.modCore]; rfl
+  | 1, 1 => rw [Nat.modCore, Nat.modCore]; rfl
+  | 1, (_+2) => rw [Nat.modCore]; rfl
+  | (_ + 2), _ => rfl
 
 theorem mod_eq (x y : Nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x := by
   rw [←Nat.modCore_eq_mod, ←Nat.modCore_eq_mod, Nat.modCore]

src/Init/Data/Nat/Gcd.lean

@@ -37,11 +37,11 @@ def gcd (m n : @& Nat) : Nat :=
   termination_by m
   decreasing_by simp_wf; apply mod_lt _ (zero_lt_of_ne_zero _); assumption
 
-@[simp] theorem gcd_zero_left (y : Nat) : gcd 0 y = y := by
-  rw [gcd]; rfl
+@[simp] theorem gcd_zero_left (y : Nat) : gcd 0 y = y :=
+  rfl
 
-theorem gcd_succ (x y : Nat) : gcd (succ x) y = gcd (y % succ x) (succ x) := by
-  rw [gcd]; rfl
+theorem gcd_succ (x y : Nat) : gcd (succ x) y = gcd (y % succ x) (succ x) :=
+  rfl
 
 @[simp] theorem gcd_one_left (n : Nat) : gcd 1 n = 1 := by
   rw [gcd_succ, mod_one]
@@ -64,7 +64,7 @@ instance : Std.IdempotentOp gcd := ⟨gcd_self⟩
 
 theorem gcd_rec (m n : Nat) : gcd m n = gcd (n % m) m :=
   match m with
-  | 0 => by have := (mod_zero n).symm; rwa [gcd, gcd_zero_right]
+  | 0 => by have := (mod_zero n).symm; rwa [gcd_zero_right]
   | _ + 1 => by simp [gcd_succ]
 
 @[elab_as_elim] theorem gcd.induction {P : Nat → Nat → Prop} (m n : Nat)

src/Init/Data/Nat/Lemmas.lean

@@ -137,14 +137,14 @@ protected theorem sub_le_iff_le_add' {a b c : Nat} : a - b ≤ c ↔ a ≤ b + c
 protected theorem le_sub_iff_add_le {n : Nat} (h : k ≤ m) : n ≤ m - k ↔ n + k ≤ m :=
   ⟨Nat.add_le_of_le_sub h, Nat.le_sub_of_add_le⟩
 
-@[deprecated Nat.le_sub_iff_add_le (since := "2024-02-19")]
+@[deprecated Nat.le_sub_iff_add_le]
 protected theorem add_le_to_le_sub (n : Nat) (h : m ≤ k) : n + m ≤ k ↔ n ≤ k - m :=
   (Nat.le_sub_iff_add_le h).symm
 
 protected theorem add_le_of_le_sub' {n k m : Nat} (h : m ≤ k) : n ≤ k - m → m + n ≤ k :=
   Nat.add_comm .. ▸ Nat.add_le_of_le_sub h
 
-@[deprecated Nat.add_le_of_le_sub' (since := "2024-02-19")]
+@[deprecated Nat.add_le_of_le_sub']
 protected theorem add_le_of_le_sub_left {n k m : Nat} (h : m ≤ k) : n ≤ k - m → m + n ≤ k :=
   Nat.add_le_of_le_sub' h
 
@@ -401,11 +401,11 @@ protected theorem mul_min_mul_left (a b c : Nat) : min (a * b) (a * c) = a * min
 
 /-! ### mul -/
 
-@[deprecated Nat.mul_le_mul_left (since := "2024-02-19")]
+@[deprecated Nat.mul_le_mul_left]
 protected theorem mul_le_mul_of_nonneg_left {a b c : Nat} : a ≤ b → c * a ≤ c * b :=
   Nat.mul_le_mul_left c
 
-@[deprecated Nat.mul_le_mul_right (since := "2024-02-19")]
+@[deprecated Nat.mul_le_mul_right]
 protected theorem mul_le_mul_of_nonneg_right {a b c : Nat} : a ≤ b → a * c ≤ b * c :=
   Nat.mul_le_mul_right c
 
@@ -677,10 +677,6 @@ protected theorem pow_lt_pow_iff_right {a n m : Nat} (h : 1 < a) :
 
 /-! ### log2 -/
 
-@[simp]
-theorem log2_zero : Nat.log2 0 = 0 := by
-  simp [Nat.log2]
-
 theorem le_log2 (h : n ≠ 0) : k ≤ n.log2 ↔ 2 ^ k ≤ n := by
   match k with
   | 0 => simp [show 1 ≤ n from Nat.pos_of_ne_zero h]
@@ -701,7 +697,7 @@ theorem log2_self_le (h : n ≠ 0) : 2 ^ n.log2 ≤ n := (le_log2 h).1 (Nat.le_r
 
 theorem lt_log2_self : n < 2 ^ (n.log2 + 1) :=
   match n with
-  | 0 => by simp
+  | 0 => Nat.zero_lt_two
   | n+1 => (log2_lt n.succ_ne_zero).1 (Nat.le_refl _)
 
 /-! ### dvd -/

src/Init/Data/Nat/Linear.lean

@@ -714,10 +714,4 @@ theorem Expr.eq_of_toNormPoly_eq (ctx : Context) (e e' : Expr) (h : e.toNormPoly
   simp [Expr.toNormPoly, Poly.norm] at h
   assumption
 
-end Linear
-
-def elimOffset {α : Sort u} (a b k : Nat) (h₁ : a + k = b + k) (h₂ : a = b → α) : α := by
-  simp_arith at h₁
-  exact h₂ h₁
-
-end Nat
+end Nat.Linear

src/Init/Data/Option/Basic.lean

@@ -18,8 +18,8 @@ def getM [Alternative m] : Option α → m α
   | none     => failure
   | some a   => pure a
 
-@[deprecated getM (since := "2024-04-17")]
-def toMonad [Monad m] [Alternative m] : Option α → m α := getM
+@[deprecated getM] def toMonad [Monad m] [Alternative m] : Option α → m α :=
+  getM
 
 /-- Returns `true` on `some x` and `false` on `none`. -/
 @[inline] def isSome : Option α → Bool

src/Init/Data/String/Basic.lean

@@ -683,15 +683,13 @@ def substrEq (s1 : String) (off1 : String.Pos) (s2 : String) (off2 : String.Pos)
   off1.byteIdx + sz ≤ s1.endPos.byteIdx && off2.byteIdx + sz ≤ s2.endPos.byteIdx && loop off1 off2 { byteIdx := off1.byteIdx + sz }
 where
   loop (off1 off2 stop1 : Pos) :=
-    if _h : off1.byteIdx < stop1.byteIdx then
+    if h : off1.byteIdx < stop1.byteIdx then
       let c₁ := s1.get off1
       let c₂ := s2.get off2
+      have := Nat.sub_lt_sub_left h (Nat.add_lt_add_left (one_le_csize c₁) off1.1)
       c₁ == c₂ && loop (off1 + c₁) (off2 + c₂) stop1
     else true
   termination_by stop1.1 - off1.1
-  decreasing_by
-    have := Nat.sub_lt_sub_left _h (Nat.add_lt_add_left (one_le_csize c₁) off1.1)
-    decreasing_tactic
 
 /-- Return true iff `p` is a prefix of `s` -/
 def isPrefixOf (p : String) (s : String) : Bool :=

src/Init/Grind.lean

@@ -1,8 +0,0 @@
-/-
-Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.Grind.Norm
-import Init.Grind.Tactics

src/Init/Grind/Norm.lean

@@ -1,110 +0,0 @@
-/-
-Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.SimpLemmas
-import Init.Classical
-import Init.ByCases
-
-namespace Lean.Grind
-/-!
-Normalization theorems for the `grind` tactic.
-
-We are also going to use simproc's in the future.
--/
-
--- Not
-attribute [grind_norm] Classical.not_not
-
--- Ne
-attribute [grind_norm] ne_eq
-
--- Iff
-@[grind_norm] theorem iff_eq (p q : Prop) : (p ↔ q) = (p = q) := by
-  by_cases p <;> by_cases q <;> simp [*]
-
--- Eq
-attribute [grind_norm] eq_self heq_eq_eq
-
--- Prop equality
-@[grind_norm] theorem eq_true_eq (p : Prop) : (p = True) = p := by simp
-@[grind_norm] theorem eq_false_eq (p : Prop) : (p = False) = ¬p := by simp
-@[grind_norm] theorem not_eq_prop (p q : Prop) : (¬(p = q)) = (p = ¬q) := by
-  by_cases p <;> by_cases q <;> simp [*]
-
--- True
-attribute [grind_norm] not_true
-
--- False
-attribute [grind_norm] not_false_eq_true
-
--- Implication as a clause
-@[grind_norm] theorem imp_eq (p q : Prop) : (p → q) = (¬ p ∨ q) := by
-  by_cases p <;> by_cases q <;> simp [*]
-
--- And
-@[grind_norm↓] theorem not_and (p q : Prop) : (¬(p ∧ q)) = (¬p ∨ ¬q) := by
-  by_cases p <;> by_cases q <;> simp [*]
-attribute [grind_norm] and_true true_and and_false false_and and_assoc
-
--- Or
-attribute [grind_norm↓] not_or
-attribute [grind_norm] or_true true_or or_false false_or or_assoc
-
--- ite
-attribute [grind_norm] ite_true ite_false
-@[grind_norm↓] theorem not_ite {_ : Decidable p} (q r : Prop) : (¬ite p q r) = ite p (¬q) (¬r) := by
-  by_cases p <;> simp [*]
-
--- Forall
-@[grind_norm↓] theorem not_forall (p : α → Prop) : (¬∀ x, p x) = ∃ x, ¬p x := by simp
-attribute [grind_norm] forall_and
-
--- Exists
-@[grind_norm↓] theorem not_exists (p : α → Prop) : (¬∃ x, p x) = ∀ x, ¬p x := by simp
-attribute [grind_norm] exists_const exists_or
-
--- Bool cond
-@[grind_norm] theorem cond_eq_ite (c : Bool) (a b : α) : cond c a b = ite c a b := by
-  cases c <;> simp [*]
-
--- Bool or
-attribute [grind_norm]
-  Bool.or_false Bool.or_true Bool.false_or Bool.true_or Bool.or_eq_true Bool.or_assoc
-
--- Bool and
-attribute [grind_norm]
-  Bool.and_false Bool.and_true Bool.false_and Bool.true_and Bool.and_eq_true Bool.and_assoc
-
--- Bool not
-attribute [grind_norm]
-  Bool.not_not
-
--- beq
-attribute [grind_norm] beq_iff_eq
-
--- bne
-attribute [grind_norm] bne_iff_ne
-
--- Bool not eq true/false
-attribute [grind_norm] Bool.not_eq_true Bool.not_eq_false
-
--- decide
-attribute [grind_norm] decide_eq_true_eq decide_not not_decide_eq_true
-
--- Nat LE
-attribute [grind_norm] Nat.le_zero_eq
-
--- Nat/Int LT
-@[grind_norm] theorem Nat.lt_eq (a b : Nat) : (a < b) = (a + 1 ≤ b) := by
-  simp [Nat.lt, LT.lt]
-
-@[grind_norm] theorem Int.lt_eq (a b : Int) : (a < b) = (a + 1 ≤ b) := by
-  simp [Int.lt, LT.lt]
-
--- GT GE
-attribute [grind_norm] GT.gt GE.ge
-
-end Lean.Grind

src/Init/Grind/Tactics.lean

@@ -1,14 +0,0 @@
-/-
-Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.Tactics
-
-namespace Lean.Grind
-/-!
-`grind` tactic and related tactics.
--/
-
-end Lean.Grind

src/Init/System/IO.lean

@@ -210,44 +210,8 @@ def sleep (ms : UInt32) : BaseIO Unit :=
 /-- Request cooperative cancellation of the task. The task must explicitly call `IO.checkCanceled` to react to the cancellation. -/
 @[extern "lean_io_cancel"] opaque cancel : @& Task α → BaseIO Unit
 
-/-- The current state of a `Task` in the Lean runtime's task manager. -/
-inductive TaskState
-  /--
-  The `Task` is waiting to be run.
-  It can be waiting for dependencies to complete or
-  sitting in the task manager queue waiting for a thread to run on.
-  -/
-  | waiting
-  /--
-  The `Task` is actively running on a thread or,
-  in the case of a `Promise`, waiting for a call to `IO.Promise.resolve`.
-  -/
-  | running
-  /--
-  The `Task` has finished running and its result is available.
-  Calling `Task.get` or `IO.wait` on the task will not block.
-  -/
-  | finished
-  deriving Inhabited, Repr, DecidableEq, Ord
-
-instance : LT TaskState := ltOfOrd
-instance : LE TaskState := leOfOrd
-instance : Min TaskState := minOfLe
-instance : Max TaskState := maxOfLe
-
-protected def TaskState.toString : TaskState → String
-  | .waiting => "waiting"
-  | .running => "running"
-  | .finished => "finished"
-
-instance : ToString TaskState := ⟨TaskState.toString⟩
-
-/-- Returns current state of the `Task` in the Lean runtime's task manager. -/
-@[extern "lean_io_get_task_state"] opaque getTaskState : @& Task α → BaseIO TaskState
-
 /-- Check if the task has finished execution, at which point calling `Task.get` will return immediately. -/
-@[inline] def hasFinished (task : Task α) : BaseIO Bool := do
-  return (← getTaskState task) matches .finished
+@[extern "lean_io_has_finished"] opaque hasFinished : @& Task α → BaseIO Bool
 
 /-- Wait for the task to finish, then return its result. -/
 @[extern "lean_io_wait"] opaque wait (t : Task α) : BaseIO α :=

src/Init/Tactics.lean

@@ -1425,16 +1425,6 @@ If there are several with the same priority, it is uses the "most recent one". E
 -/
 syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? (ppSpace prio)? : attr
 
-/--
-Theorems tagged with the `grind_norm` attribute are used by the `grind` tactic normalizer/pre-processor.
--/
-syntax (name := grind_norm) "grind_norm" (Tactic.simpPre <|> Tactic.simpPost)? (ppSpace prio)? : attr
-
-/--
-Simplification procedures tagged with the `grind_norm_proc` attribute are used by the `grind` tactic normalizer/pre-processor.
--/
-syntax (name := grind_norm_proc) "grind_norm_proc" (Tactic.simpPre <|> Tactic.simpPost)? : attr
-
 
 /-- The possible `norm_cast` kinds: `elim`, `move`, or `squash`. -/
 syntax normCastLabel := &"elim" <|> &"move" <|> &"squash"

src/Lean.lean

@@ -37,4 +37,3 @@ import Lean.Log
 import Lean.Linter
 import Lean.SubExpr
 import Lean.LabelAttribute
-import Lean.AddDecl

src/Lean/AddDecl.lean

@@ -1,31 +0,0 @@
-/-
-Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.CoreM
-
-namespace Lean
-
-def Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration) : Except KernelException Environment :=
-  addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl
-
-def Environment.addAndCompile (env : Environment) (opts : Options) (decl : Declaration) : Except KernelException Environment := do
-  let env ← addDecl env opts decl
-  compileDecl env opts decl
-
-def addDecl (decl : Declaration) : CoreM Unit := do
-  profileitM Exception "type checking" (← getOptions) do
-    withTraceNode `Kernel (fun _ => return m!"typechecking declaration") do
-      if !(← MonadLog.hasErrors) && decl.hasSorry then
-        logWarning "declaration uses 'sorry'"
-      match (← getEnv).addDecl (← getOptions) decl with
-      | .ok    env => setEnv env
-      | .error ex  => throwKernelException ex
-
-def addAndCompile (decl : Declaration) : CoreM Unit := do
-  addDecl decl
-  compileDecl decl
-
-end Lean

src/Lean/Compiler/InitAttr.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.AddDecl
 import Lean.Elab.InfoTree.Main
 
 namespace Lean

src/Lean/Compiler/Old.lean

@@ -67,4 +67,9 @@ opaque compileDecls (env : Environment) (opt : @& Options) (decls : @& List Name
 def compileDecl (env : Environment) (opt : @& Options) (decl : @& Declaration) : Except KernelException Environment :=
   compileDecls env opt (Compiler.getDeclNamesForCodeGen decl)
 
+
+def addAndCompile (env : Environment) (opt : Options) (decl : Declaration) : Except KernelException Environment := do
+  let env ← addDecl env decl
+  compileDecl env opt decl
+
 end Environment

src/Lean/CoreM.lean

@@ -30,8 +30,6 @@ register_builtin_option maxHeartbeats : Nat := {
   descr := "maximum amount of heartbeats per command. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit"
 }
 
-def useDiagnosticMsg := s!"use `set_option {diagnostics.name} true` to get diagnostic information"
-
 namespace Core
 
 builtin_initialize registerTraceClass `Kernel
@@ -81,6 +79,12 @@ structure Context where
   maxHeartbeats  : Nat := getMaxHeartbeats options
   currMacroScope : MacroScope := firstFrontendMacroScope
   /--
+  If `catchRuntimeEx = false`, then given `try x catch ex => h ex`,
+  an runtime exception occurring in `x` is not handled by `h`.
+  Recall that runtime exceptions are `maxRecDepth` or `maxHeartbeats`.
+  -/
+  catchRuntimeEx : Bool := false
+  /--
   If `diag := true`, different parts of the system collect diagnostics.
   Use the `set_option diag true` to set it to true.
   -/
@@ -246,16 +250,8 @@ protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m
     -- should never be visible to users!
     throw <| Exception.error .missing "elaboration interrupted"
 
-register_builtin_option debug.moduleNameAtTimeout : Bool := {
-  defValue := true
-  group    := "debug"
-  descr    := "include module name in deterministic timeout error messages.\nRemark: we set this option to false to increase the stability of our test suite"
-}
-
 def throwMaxHeartbeat (moduleName : Name) (optionName : Name) (max : Nat) : CoreM Unit := do
-  let includeModuleName := debug.moduleNameAtTimeout.get (← getOptions)
-  let atModuleName := if includeModuleName then s!" at `{moduleName}`" else ""
-  let msg := s!"(deterministic) timeout{atModuleName}, maximum number of heartbeats ({max/1000}) has been reached\nuse `set_option {optionName} <num>` to set the limit\n{useDiagnosticMsg}"
+  let msg := s!"(deterministic) timeout at `{moduleName}`, maximum number of heartbeats ({max/1000}) has been reached\nuse `set_option {optionName} <num>` to set the limit\nuse `set_option {diagnostics.name} true` to get diagnostic information"
   throw <| Exception.error (← getRef) (MessageData.ofFormat (Std.Format.text msg))
 
 def checkMaxHeartbeatsCore (moduleName : String) (optionName : Name) (max : Nat) : CoreM Unit := do
@@ -342,6 +338,15 @@ def mkArrow (d b : Expr) : CoreM Expr :=
 /-- Iterated `mkArrow`, creates the expression `a₁ → a₂ → … → aₙ → b`. Also see `arrowDomainsN`. -/
 def mkArrowN (ds : Array Expr) (e : Expr) : CoreM Expr := ds.foldrM mkArrow e
 
+def addDecl (decl : Declaration) : CoreM Unit := do
+  profileitM Exception "type checking" (← getOptions) do
+    withTraceNode `Kernel (fun _ => return m!"typechecking declaration") do
+      if !(← MonadLog.hasErrors) && decl.hasSorry then
+        logWarning "declaration uses 'sorry'"
+      match (← getEnv).addDecl decl with
+      | Except.ok    env => setEnv env
+      | Except.error ex  => throwKernelException ex
+
 private def supportedRecursors :=
   #[``Empty.rec, ``False.rec, ``Eq.ndrec, ``Eq.rec, ``Eq.recOn, ``Eq.casesOn, ``False.casesOn, ``Empty.casesOn, ``And.rec, ``And.casesOn]
 
@@ -395,6 +400,10 @@ def compileDecls (decls : List Name) : CoreM Unit := do
   | Except.error ex =>
     throwKernelException ex
 
+def addAndCompile (decl : Declaration) : CoreM Unit := do
+  addDecl decl;
+  compileDecl decl
+
 def getDiag (opts : Options) : Bool :=
   diagnostics.get opts
 
@@ -419,36 +428,30 @@ in these monads, but on `CommandElabM`. See issues #2775 and #2744 as well as `M
   try
     x
   catch ex =>
-    if ex.isRuntime then
-      throw ex -- We should use `tryCatchRuntimeEx` for catching runtime exceptions
+    if ex.isRuntime && !(← read).catchRuntimeEx then
+      throw ex
     else
       h ex
 
-@[inline] protected def Core.tryCatchRuntimeEx (x : CoreM α) (h : Exception → CoreM α) : CoreM α := do
-  try
-    x
-  catch ex =>
-    h ex
-
 instance : MonadExceptOf Exception CoreM where
   throw    := throw
   tryCatch := Core.tryCatch
 
-class MonadRuntimeException (m : Type → Type) where
-  tryCatchRuntimeEx (body : m α) (handler : Exception → m α) : m α
-
-export MonadRuntimeException (tryCatchRuntimeEx)
-
-instance : MonadRuntimeException CoreM where
-  tryCatchRuntimeEx := Core.tryCatchRuntimeEx
-
-@[inline] instance [MonadRuntimeException m] : MonadRuntimeException (ReaderT ρ m) where
-  tryCatchRuntimeEx := fun x c r => tryCatchRuntimeEx (x r) (fun e => (c e) r)
-
-@[inline] instance [MonadRuntimeException m] : MonadRuntimeException (StateRefT' ω σ m) where
-  tryCatchRuntimeEx := fun x c s => tryCatchRuntimeEx (x s) (fun e => c e s)
+@[inline] def Core.withCatchingRuntimeEx (flag : Bool) (x : CoreM α) : CoreM α :=
+  withReader (fun ctx => { ctx with catchRuntimeEx := flag }) x
 
 @[inline] def mapCoreM [MonadControlT CoreM m] [Monad m] (f : forall {α}, CoreM α → CoreM α) {α} (x : m α) : m α :=
   controlAt CoreM fun runInBase => f <| runInBase x
 
+/--
+Execute `x` with `catchRuntimeEx = flag`. That is, given `try x catch ex => h ex`,
+if `x` throws a runtime exception, the handler `h` will be invoked if `flag = true`
+Recall that
+-/
+@[inline] def withCatchingRuntimeEx [MonadControlT CoreM m] [Monad m] (x : m α) : m α :=
+  mapCoreM (Core.withCatchingRuntimeEx true) x
+
+@[inline] def withoutCatchingRuntimeEx [MonadControlT CoreM m] [Monad m] (x : m α) : m α :=
+  mapCoreM (Core.withCatchingRuntimeEx false) x
+
 end Lean

src/Lean/Elab/BuiltinCommand.lean

@@ -123,7 +123,7 @@ private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM
   n[1].forArgsM addUnivLevel
 
 @[builtin_command_elab «init_quot»] def elabInitQuot : CommandElab := fun _ => do
-  match (← getEnv).addDecl (← getOptions) Declaration.quotDecl with
+  match (← getEnv).addDecl Declaration.quotDecl with
   | Except.ok env   => setEnv env
   | Except.error ex => throwError (ex.toMessageData (← getOptions))
 

src/Lean/Elab/BuiltinNotation.lean

@@ -205,7 +205,7 @@ private def elabTParserMacroAux (prec lhsPrec e : Term) : TermElabM Syntax := do
   | _                                        => Macro.throwUnsupported
 
 @[builtin_term_elab «sorry»] def elabSorry : TermElab := fun stx expectedType? => do
-  let stxNew ← `(@sorryAx _ false) -- Remark: we use `@` to ensure `sorryAx` will not consume auot params
+  let stxNew ← `(sorryAx _ false)
   withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
 
 /-- Return syntax `Prod.mk elems[0] (Prod.mk elems[1] ... (Prod.mk elems[elems.size - 2] elems[elems.size - 1])))` -/

src/Lean/Elab/Calc.lean

@@ -42,7 +42,7 @@ def mkCalcTrans (result resultType step stepType : Expr) : MetaM (Expr × Expr)
     unless (← getCalcRelation? resultType).isSome do
       throwError "invalid 'calc' step, step result is not a relation{indentExpr resultType}"
     return (result, resultType)
-  | _ => throwError "invalid 'calc' step, failed to synthesize `Trans` instance{indentExpr selfType}\n{useDiagnosticMsg}"
+  | _ => throwError "invalid 'calc' step, failed to synthesize `Trans` instance{indentExpr selfType}"
 
 /--
 Adds a type annotation to a hole that occurs immediately at the beginning of the term.

src/Lean/Elab/PreDefinition/Main.lean

@@ -90,11 +90,6 @@ private def addAsAxioms (preDefs : Array PreDefinition) : TermElabM Unit := do
     applyAttributesOf #[preDef] AttributeApplicationTime.afterTypeChecking
     applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
 
-def ensureFunIndReservedNamesAvailable (preDefs : Array PreDefinition) : MetaM Unit := do
-  preDefs.forM fun preDef =>
-    withRef preDef.ref <| ensureReservedNameAvailable preDef.declName "induct"
-  withRef preDefs[0]!.ref <| ensureReservedNameAvailable preDefs[0]!.declName "mutual_induct"
-
 def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLCtx {} {} do
   for preDef in preDefs do
     trace[Elab.definition.body] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
@@ -126,7 +121,6 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
       addAndCompilePartial preDefs
       preDefs.forM (·.termination.ensureNone "partial")
     else
-      ensureFunIndReservedNamesAvailable preDefs
       try
         let hasHints := preDefs.any fun preDef => preDef.termination.isNotNone
         if hasHints then

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -9,7 +9,6 @@ import Lean.Meta.Tactic.Split
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Eqns
 import Lean.Meta.ArgsPacker.Basic
-import Init.Data.Array.Basic
 
 namespace Lean.Elab.WF
 open Meta
@@ -40,6 +39,41 @@ private def rwFixEq (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
   mvarId.assign (← mkEqTrans h mvarNew)
   return mvarNew.mvarId!
 
+/--
+  Simplify `match`-expressions when trying to prove equation theorems for a recursive declaration defined using well-founded recursion.
+  It is similar to `simpMatch?`, but is also tries to fold `WellFounded.fix` applications occurring in discriminants.
+  See comment at `tryToFoldWellFoundedFix`.
+-/
+def simpMatchWF? (mvarId : MVarId) : MetaM (Option MVarId) :=
+  mvarId.withContext do
+    let target ← instantiateMVars (← mvarId.getType)
+    let discharge? ← mvarId.withContext do SplitIf.mkDischarge?
+    let (targetNew, _) ← Simp.main target (← Split.getSimpMatchContext) (methods := { pre, discharge? })
+    let mvarIdNew ← applySimpResultToTarget mvarId target targetNew
+    if mvarId != mvarIdNew then return some mvarIdNew else return none
+where
+  pre (e : Expr) : SimpM Simp.Step := do
+    let some app ← matchMatcherApp? e
+      | return Simp.Step.continue
+    -- First try to reduce matcher
+    match (← reduceRecMatcher? e) with
+    | some e' => return Simp.Step.done { expr := e' }
+    | none    => Simp.simpMatchCore app.matcherName e
+
+/--
+  Given a goal of the form `|- f.{us} a_1 ... a_n b_1 ... b_m = ...`, return `(us, #[a_1, ..., a_n])`
+  where `f` is a constant named `declName`, and `n = info.fixedPrefixSize`.
+-/
+private def getFixedPrefix (declName : Name) (info : EqnInfo) (mvarId : MVarId) : MetaM (List Level × Array Expr) := mvarId.withContext do
+  let target ← mvarId.getType'
+  let some (_, lhs, _) := target.eq? | unreachable!
+  let lhsArgs := lhs.getAppArgs
+  if lhsArgs.size < info.fixedPrefixSize || !lhs.getAppFn matches .const .. then
+    throwError "failed to generate equational theorem for '{declName}', unexpected number of arguments in the equation left-hand-side\n{mvarId}"
+  let result := lhsArgs[:info.fixedPrefixSize]
+  trace[Elab.definition.wf.eqns] "fixedPrefix: {result}"
+  return (lhs.getAppFn.constLevels!, result)
+
 private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
   trace[Elab.definition.wf.eqns] "proving: {type}"
   withNewMCtxDepth do
@@ -47,11 +81,11 @@ private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
     let (_, mvarId) ← main.mvarId!.intros
     let rec go (mvarId : MVarId) : MetaM Unit := do
       trace[Elab.definition.wf.eqns] "step\n{MessageData.ofGoal mvarId}"
-      if ← withAtLeastTransparency .all (tryURefl mvarId) then
+      if (← tryURefl mvarId) then
         return ()
       else if (← tryContradiction mvarId) then
         return ()
-      else if let some mvarId ← simpMatch? mvarId then
+      else if let some mvarId ← simpMatchWF? mvarId then
         go mvarId
       else if let some mvarId ← simpIf? mvarId then
         go mvarId

src/Lean/Elab/PreDefinition/WF/Main.lean

@@ -132,15 +132,12 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
       return { unaryPreDef with value }
   trace[Elab.definition.wf] ">> {preDefNonRec.declName} :=\n{preDefNonRec.value}"
   let preDefs ← preDefs.mapM fun d => eraseRecAppSyntax d
-  -- Do not complain if the user sets @[semireducible], which usually is a noop,
-  -- we recognize that below and then do not set @[irreducible]
-  withOptions (allowUnsafeReducibility.set · true) do
-    if (← isOnlyOneUnaryDef preDefs fixedPrefixSize) then
+  if (← isOnlyOneUnaryDef preDefs fixedPrefixSize) then
+    addNonRec preDefNonRec (applyAttrAfterCompilation := false)
+  else
+    withEnableInfoTree false do
       addNonRec preDefNonRec (applyAttrAfterCompilation := false)
-    else
-      withEnableInfoTree false do
-        addNonRec preDefNonRec (applyAttrAfterCompilation := false)
-      addNonRecPreDefs fixedPrefixSize argsPacker preDefs preDefNonRec
+    addNonRecPreDefs fixedPrefixSize argsPacker preDefs preDefNonRec
   -- We create the `_unsafe_rec` before we abstract nested proofs.
   -- Reason: the nested proofs may be referring to the _unsafe_rec.
   addAndCompilePartialRec preDefs
@@ -149,10 +146,6 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
   for preDef in preDefs do
     markAsRecursive preDef.declName
     applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
-    -- Unless the user asks for something else, mark the definition as irreducible
-    unless preDef.modifiers.attrs.any fun a =>
-      a.name = `reducible || a.name = `semireducible do
-      setIrreducibleAttribute preDef.declName
 
 builtin_initialize registerTraceClass `Elab.definition.wf
 

src/Lean/Elab/SyntheticMVars.lean

@@ -340,26 +340,26 @@ mutual
     Regarding issue #1380, we addressed the issue by avoiding the elaboration postponement step. However, the same issue can happen
     in more complicated scenarios.
     -/
-    tryCatchRuntimeEx
-      (do let remainingGoals ← withInfoHole mvarId <| Tactic.run mvarId do
-            withTacticInfoContext tacticCode do
-              -- also put an info node on the `by` keyword specifically -- the token may be `canonical` and thus shown in the info
-              -- view even though it is synthetic while a node like `tacticCode` never is (#1990)
-              withTacticInfoContext tacticCode[0] do
-                evalTactic code
-            synthesizeSyntheticMVars (postpone := .no)
-          unless remainingGoals.isEmpty do
-            if report then
-              reportUnsolvedGoals remainingGoals
-            else
-              throwError "unsolved goals\n{goalsToMessageData remainingGoals}")
-      fun ex => do
-        if report && (← read).errToSorry then
-          for mvarId in (← getMVars (mkMVar mvarId)) do
-            mvarId.admit
-          logException ex
+    try
+      let remainingGoals ← withInfoHole mvarId <| Tactic.run mvarId do
+        withTacticInfoContext tacticCode do
+          -- also put an info node on the `by` keyword specifically -- the token may be `canonical` and thus shown in the info
+          -- view even though it is synthetic while a node like `tacticCode` never is (#1990)
+          withTacticInfoContext tacticCode[0] do
+            evalTactic code
+        synthesizeSyntheticMVars (postpone := .no)
+      unless remainingGoals.isEmpty do
+        if report then
+          reportUnsolvedGoals remainingGoals
         else
-          throw ex
+          throwError "unsolved goals\n{goalsToMessageData remainingGoals}"
+    catch ex =>
+      if report && (← read).errToSorry then
+        for mvarId in (← getMVars (mkMVar mvarId)) do
+          mvarId.admit
+        logException ex
+      else
+        throw ex
 
   /-- Try to synthesize the given pending synthetic metavariable. -/
   private partial def synthesizeSyntheticMVar (mvarId : MVarId) (postponeOnError : Bool) (runTactics : Bool) : TermElabM Bool := do

src/Lean/Elab/Tactic/Basic.lean

@@ -231,15 +231,15 @@ def closeUsingOrAdmit (tac : TacticM Unit) : TacticM Unit := do
   /- Important: we must define `closeUsingOrAdmit` before we define
      the instance `MonadExcept` for `TacticM` since it backtracks the state including error messages. -/
   let mvarId :: mvarIds ← getUnsolvedGoals | throwNoGoalsToBeSolved
-  tryCatchRuntimeEx
-    (focusAndDone tac)
-    fun ex => do
-      if (← read).recover then
-        logException ex
-        admitGoal mvarId
-        setGoals mvarIds
-      else
-        throw ex
+  try
+    focusAndDone tac
+  catch ex =>
+    if (← read).recover then
+      logException ex
+      admitGoal mvarId
+      setGoals mvarIds
+    else
+      throw ex
 
 instance : MonadBacktrack SavedState TacticM where
   saveState := Tactic.saveState

src/Lean/Elab/Tactic/Omega/OmegaM.lean

@@ -150,7 +150,7 @@ partial def groundInt? (e : Expr) : Option Int :=
     | _, _ => none
   | _ => e.int?
 where op (f : Int → Int → Int) (x y : Expr) : Option Int :=
-  match groundInt? x, groundInt? y with
+  match groundNat? x, groundNat? y with
     | some x', some y' => some (f x' y')
     | _, _ => none
 
@@ -199,7 +199,7 @@ def analyzeAtom (e : Expr) : OmegaM (HashSet Expr) := do
       | some _ =>
         let b_pos := mkApp4 (.const ``LT.lt [0]) (.const ``Int []) (.const ``Int.instLTInt [])
           (toExpr (0 : Int)) b
-        let pow_pos := mkApp3 (.const ``Lean.Omega.Int.pos_pow_of_pos []) b exp (← mkDecideProof b_pos)
+        let pow_pos := mkApp3 (.const ``Int.pos_pow_of_pos []) b exp (← mkDecideProof b_pos)
         pure <| HashSet.empty.insert
           (mkApp3 (.const ``Int.emod_nonneg []) x k
               (mkApp3 (.const ``Int.ne_of_gt []) k (toExpr (0 : Int)) pow_pos)) |>.insert

src/Lean/Elab/Tactic/Simp.lean

@@ -178,7 +178,9 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
             thms := thms.eraseCore (.fvar fvar.fvarId!)
           else
             let id := arg[1]
-            if let .ok declName ← observing (realizeGlobalConstNoOverloadWithInfo id) then
+            let declNames? ← try pure (some (← realizeGlobalConst id)) catch _ => pure none
+            if let some declNames := declNames? then
+              let declName ← ensureNonAmbiguous id declNames
               if (← Simp.isSimproc declName) then
                 simprocs := simprocs.erase declName
               else if ctx.config.autoUnfold then

src/Lean/Elab/Term.lean

@@ -784,7 +784,7 @@ def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := n
     if (← read).ignoreTCFailures then
       return false
     else
-      throwError "failed to synthesize{indentExpr type}\n{useDiagnosticMsg}"
+      throwError "failed to synthesize instance{indentExpr type}"
 
 def mkCoe (expectedType : Expr) (e : Expr) (f? : Option Expr := none) (errorMsgHeader? : Option String := none) : TermElabM Expr := do
   withTraceNode `Elab.coe (fun _ => return m!"adding coercion for {e} : {← inferType e} =?= {expectedType}") do

src/Lean/Environment.lean

@@ -246,7 +246,7 @@ namespace Environment
 
 /-- Type check given declaration and add it to the environment -/
 @[extern "lean_add_decl"]
-opaque addDeclCore (env : Environment) (maxHeartbeats : USize) (decl : @& Declaration) : Except KernelException Environment
+opaque addDecl (env : Environment) (decl : @& Declaration) : Except KernelException Environment
 
 end Environment
 

src/Lean/Meta/Basic.lean

@@ -212,17 +212,7 @@ instance : Hashable InfoCacheKey :=
   ⟨fun ⟨transparency, expr, nargs⟩ => mixHash (hash transparency) <| mixHash (hash expr) (hash nargs)⟩
 end InfoCacheKey
 
-structure SynthInstanceCacheKey where
-  localInsts        : LocalInstances
-  type              : Expr
-  /--
-  Value of `synthPendingDepth` when instance was synthesized or failed to be synthesized.
-  See issue #2522.
-  -/
-  synthPendingDepth : Nat
-  deriving Hashable, BEq
-
-abbrev SynthInstanceCache := PersistentHashMap SynthInstanceCacheKey (Option Expr)
+abbrev SynthInstanceCache := PersistentHashMap (LocalInstances × Expr) (Option Expr)
 
 abbrev InferTypeCache := PersistentExprStructMap Expr
 abbrev FunInfoCache   := PersistentHashMap InfoCacheKey FunInfo
@@ -283,8 +273,6 @@ structure Diagnostics where
   heuristicCounter : PHashMap Name Nat := {}
   /-- Number of times a TC instance is used. -/
   instanceCounter : PHashMap Name Nat := {}
-  /-- Pending instances that were not synthesized because `maxSynthPendingDepth` has been reached. -/
-  synthPendingFailures : PHashMap Expr MessageData := {}
   deriving Inhabited
 
 /--
@@ -308,11 +296,6 @@ structure SavedState where
   meta        : State
   deriving Nonempty
 
-register_builtin_option maxSynthPendingDepth : Nat := {
-  defValue := 1
-  descr    := "maximum number of nested `synthPending` invocations. When resolving unification constraints, pending type class problems may need to be synthesized. These type class problems may create new unification constraints that again require solving new type class problems. This option puts a threshold on how many nested problems are created."
-}
-
 /--
   Contextual information for the `MetaM` monad.
 -/
@@ -328,8 +311,8 @@ structure Context where
     Track the number of nested `synthPending` invocations. Nested invocations can happen
     when the type class resolution invokes `synthPending`.
 
-    Remark: `synthPending` fails if `synthPendingDepth > maxSynthPendingDepth`.
-  -/
+    Remark: in the current implementation, `synthPending` fails if `synthPendingDepth > 0`.
+    We will add a configuration option if necessary. -/
   synthPendingDepth : Nat                  := 0
   /--
     A predicate to control whether a constant can be unfolded or not at `whnf`.
@@ -487,30 +470,21 @@ variable [MonadControlT MetaM n] [Monad n]
 
 /-- If diagnostics are enabled, record that `declName` has been unfolded. -/
 def recordUnfold (declName : Name) : MetaM Unit := do
-  modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter, synthPendingFailures } =>
+  modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter } =>
     let newC := if let some c := unfoldCounter.find? declName then c + 1 else 1
-    { unfoldCounter := unfoldCounter.insert declName newC, heuristicCounter, instanceCounter, synthPendingFailures }
+    { unfoldCounter := unfoldCounter.insert declName newC, heuristicCounter, instanceCounter }
 
 /-- If diagnostics are enabled, record that heuristic for solving `f a =?= f b` has been used. -/
 def recordDefEqHeuristic (declName : Name) : MetaM Unit := do
-  modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter, synthPendingFailures } =>
+  modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter } =>
     let newC := if let some c := heuristicCounter.find? declName then c + 1 else 1
-    { unfoldCounter, heuristicCounter := heuristicCounter.insert declName newC, instanceCounter, synthPendingFailures }
+    { unfoldCounter, heuristicCounter := heuristicCounter.insert declName newC, instanceCounter }
 
 /-- If diagnostics are enabled, record that instance `declName` was used during TC resolution. -/
 def recordInstance (declName : Name) : MetaM Unit := do
-  modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter, synthPendingFailures } =>
+  modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter } =>
     let newC := if let some c := instanceCounter.find? declName then c + 1 else 1
-    { unfoldCounter, heuristicCounter, instanceCounter := instanceCounter.insert declName newC, synthPendingFailures }
-
-/-- If diagnostics are enabled, record that synth pending failures. -/
-def recordSynthPendingFailure (type : Expr) : MetaM Unit := do
-  if (← isDiagnosticsEnabled) then
-    unless (← get).diag.synthPendingFailures.contains type do
-      -- We need to save the full context since type class resolution uses multiple metavar contexts and different local contexts
-      let msg ← addMessageContextFull m!"{type}"
-      modifyDiag fun { unfoldCounter, heuristicCounter, instanceCounter, synthPendingFailures } =>
-        { unfoldCounter, heuristicCounter, instanceCounter, synthPendingFailures := synthPendingFailures.insert type msg }
+    { unfoldCounter, heuristicCounter, instanceCounter := instanceCounter.insert declName newC }
 
 def getLocalInstances : MetaM LocalInstances :=
   return (← read).localInstances
@@ -655,7 +629,7 @@ Return `none` if `mvarId` has no declaration in the current metavariable context
 def _root_.Lean.MVarId.findDecl? (mvarId : MVarId) : MetaM (Option MetavarDecl) :=
   return (← getMCtx).findDecl? mvarId
 
-@[deprecated MVarId.findDecl? (since := "2022-07-15")]
+@[deprecated MVarId.findDecl?]
 def findMVarDecl? (mvarId : MVarId) : MetaM (Option MetavarDecl) :=
   mvarId.findDecl?
 
@@ -668,7 +642,7 @@ def _root_.Lean.MVarId.getDecl (mvarId : MVarId) : MetaM MetavarDecl := do
   | some d => pure d
   | none   => throwError "unknown metavariable '?{mvarId.name}'"
 
-@[deprecated MVarId.getDecl (since := "2022-07-15")]
+@[deprecated MVarId.getDecl]
 def getMVarDecl (mvarId : MVarId) : MetaM MetavarDecl := do
   mvarId.getDecl
 
@@ -678,7 +652,7 @@ Return `mvarId` kind. Throw an exception if `mvarId` is not declared in the curr
 def _root_.Lean.MVarId.getKind (mvarId : MVarId) : MetaM MetavarKind :=
   return (← mvarId.getDecl).kind
 
-@[deprecated MVarId.getKind (since := "2022-07-15")]
+@[deprecated MVarId.getKind]
 def getMVarDeclKind (mvarId : MVarId) : MetaM MetavarKind :=
   mvarId.getKind
 
@@ -695,7 +669,7 @@ Set `mvarId` kind in the current metavariable context.
 def _root_.Lean.MVarId.setKind (mvarId : MVarId) (kind : MetavarKind) : MetaM Unit :=
   modifyMCtx fun mctx => mctx.setMVarKind mvarId kind
 
-@[deprecated MVarId.setKind (since := "2022-07-15")]
+@[deprecated MVarId.setKind]
 def setMVarKind (mvarId : MVarId) (kind : MetavarKind) : MetaM Unit :=
   mvarId.setKind kind
 
@@ -704,7 +678,7 @@ def setMVarKind (mvarId : MVarId) (kind : MetavarKind) : MetaM Unit :=
 def _root_.Lean.MVarId.setType (mvarId : MVarId) (type : Expr) : MetaM Unit := do
   modifyMCtx fun mctx => mctx.setMVarType mvarId type
 
-@[deprecated MVarId.setType (since := "2022-07-15")]
+@[deprecated MVarId.setType]
 def setMVarType (mvarId : MVarId) (type : Expr) : MetaM Unit := do
   mvarId.setType type
 
@@ -715,7 +689,7 @@ That is, its `depth` is different from the current metavariable context depth.
 def _root_.Lean.MVarId.isReadOnly (mvarId : MVarId) : MetaM Bool := do
   return (← mvarId.getDecl).depth != (← getMCtx).depth
 
-@[deprecated MVarId.isReadOnly (since := "2022-07-15")]
+@[deprecated MVarId.isReadOnly]
 def isReadOnlyExprMVar (mvarId : MVarId) : MetaM Bool := do
   mvarId.isReadOnly
 
@@ -730,7 +704,7 @@ def _root_.Lean.MVarId.isReadOnlyOrSyntheticOpaque (mvarId : MVarId) : MetaM Boo
   | MetavarKind.syntheticOpaque => return !(← getConfig).assignSyntheticOpaque
   | _ => return mvarDecl.depth != (← getMCtx).depth
 
-@[deprecated MVarId.isReadOnlyOrSyntheticOpaque (since := "2022-07-15")]
+@[deprecated MVarId.isReadOnlyOrSyntheticOpaque]
 def isReadOnlyOrSyntheticOpaqueExprMVar (mvarId : MVarId) : MetaM Bool := do
   mvarId.isReadOnlyOrSyntheticOpaque
 
@@ -742,7 +716,7 @@ def _root_.Lean.LMVarId.getLevel (mvarId : LMVarId) : MetaM Nat := do
   | some depth => return depth
   | _          => throwError "unknown universe metavariable '?{mvarId.name}'"
 
-@[deprecated LMVarId.getLevel (since := "2022-07-15")]
+@[deprecated LMVarId.getLevel]
 def getLevelMVarDepth (mvarId : LMVarId) : MetaM Nat :=
   mvarId.getLevel
 
@@ -753,7 +727,7 @@ That is, its `depth` is different from the current metavariable context depth.
 def _root_.Lean.LMVarId.isReadOnly (mvarId : LMVarId) : MetaM Bool :=
   return (← mvarId.getLevel) < (← getMCtx).levelAssignDepth
 
-@[deprecated LMVarId.isReadOnly (since := "2022-07-15")]
+@[deprecated LMVarId.isReadOnly]
 def isReadOnlyLevelMVar (mvarId : LMVarId) : MetaM Bool := do
   mvarId.isReadOnly
 
@@ -763,7 +737,7 @@ Set the user-facing name for the given metavariable.
 def _root_.Lean.MVarId.setUserName (mvarId : MVarId) (newUserName : Name) : MetaM Unit :=
   modifyMCtx fun mctx => mctx.setMVarUserName mvarId newUserName
 
-@[deprecated MVarId.setUserName (since := "2022-07-15")]
+@[deprecated MVarId.setUserName]
 def setMVarUserName (mvarId : MVarId) (userNameNew : Name) : MetaM Unit :=
   mvarId.setUserName userNameNew
 
@@ -773,7 +747,7 @@ Throw an exception saying `fvarId` is not declared in the current local context.
 def _root_.Lean.FVarId.throwUnknown (fvarId : FVarId) : CoreM α :=
   throwError "unknown free variable '{mkFVar fvarId}'"
 
-@[deprecated FVarId.throwUnknown (since := "2022-07-15")]
+@[deprecated FVarId.throwUnknown]
 def throwUnknownFVar (fvarId : FVarId) : MetaM α :=
   fvarId.throwUnknown
 
@@ -783,7 +757,7 @@ Return `some decl` if `fvarId` is declared in the current local context.
 def _root_.Lean.FVarId.findDecl? (fvarId : FVarId) : MetaM (Option LocalDecl) :=
   return (← getLCtx).find? fvarId
 
-@[deprecated FVarId.findDecl? (since := "2022-07-15")]
+@[deprecated FVarId.findDecl?]
 def findLocalDecl? (fvarId : FVarId) : MetaM (Option LocalDecl) :=
   fvarId.findDecl?
 
@@ -796,7 +770,7 @@ def _root_.Lean.FVarId.getDecl (fvarId : FVarId) : MetaM LocalDecl := do
   | some d => return d
   | none   => fvarId.throwUnknown
 
-@[deprecated FVarId.getDecl (since := "2022-07-15")]
+@[deprecated FVarId.getDecl]
 def getLocalDecl (fvarId : FVarId) : MetaM LocalDecl := do
   fvarId.getDecl
 
@@ -863,7 +837,7 @@ contain a metavariable `?m` s.t. local context of `?m` contains a free variable
 def _root_.Lean.Expr.abstractRangeM (e : Expr) (n : Nat) (xs : Array Expr) : MetaM Expr :=
   liftMkBindingM <| MetavarContext.abstractRange e n xs
 
-@[deprecated Expr.abstractRangeM (since := "2022-07-15")]
+@[deprecated Expr.abstractRangeM]
 def abstractRange (e : Expr) (n : Nat) (xs : Array Expr) : MetaM Expr :=
   e.abstractRangeM n xs
 
@@ -874,7 +848,7 @@ Similar to `Expr.abstract`, but handles metavariables correctly.
 def _root_.Lean.Expr.abstractM (e : Expr) (xs : Array Expr) : MetaM Expr :=
   e.abstractRangeM xs.size xs
 
-@[deprecated Expr.abstractM (since := "2022-07-15")]
+@[deprecated Expr.abstractM]
 def abstract (e : Expr) (xs : Array Expr) : MetaM Expr :=
   e.abstractM xs
 
@@ -1087,20 +1061,16 @@ mutual
 
     if `maxFVars?` is `some max`, then we interrupt the telescope construction
     when `fvars.size == max`
-
-
-    If `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.
   -/
   private partial def forallTelescopeReducingAuxAux
       (reducing          : Bool) (maxFVars? : Option Nat)
       (type              : Expr)
-      (k                 : Array Expr → Expr → MetaM α) (cleanupAnnotations : Bool) : MetaM α := do
+      (k                 : Array Expr → Expr → MetaM α) : MetaM α := do
     let rec process (lctx : LocalContext) (fvars : Array Expr) (j : Nat) (type : Expr) : MetaM α := do
       match type with
       | .forallE n d b bi =>
         if fvarsSizeLtMaxFVars fvars maxFVars? then
           let d     := d.instantiateRevRange j fvars.size fvars
-          let d     := if cleanupAnnotations then d.cleanupAnnotations else d
           let fvarId ← mkFreshFVarId
           let lctx  := lctx.mkLocalDecl fvarId n d bi
           let fvar  := mkFVar fvarId
@@ -1125,13 +1095,13 @@ mutual
               k fvars type
     process (← getLCtx) #[] 0 type
 
-  private partial def forallTelescopeReducingAux (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → MetaM α) (cleanupAnnotations : Bool) : MetaM α := do
+  private partial def forallTelescopeReducingAux (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → MetaM α) : MetaM α := do
     match maxFVars? with
     | some 0 => k #[] type
     | _ => do
       let newType ← whnf type
       if newType.isForall then
-        forallTelescopeReducingAuxAux true maxFVars? newType k cleanupAnnotations
+        forallTelescopeReducingAuxAux true maxFVars? newType k
       else
         k #[] type
 
@@ -1155,7 +1125,7 @@ mutual
 
   private partial def isClassExpensive? (type : Expr) : MetaM (Option Name) :=
     withReducible do -- when testing whether a type is a type class, we only unfold reducible constants.
-      forallTelescopeReducingAux type none (cleanupAnnotations := false) fun _ type => isClassApp? type
+      forallTelescopeReducingAux type none fun _ type => isClassApp? type
 
   private partial def isClassImp? (type : Expr) : MetaM (Option Name) := do
     match (← isClassQuick? type) with
@@ -1184,18 +1154,15 @@ private def withNewLocalInstancesImpAux (fvars : Array Expr) (j : Nat) : n α
 partial def withNewLocalInstances (fvars : Array Expr) (j : Nat) : n α → n α :=
   mapMetaM <| withNewLocalInstancesImpAux fvars j
 
-@[inline] private def forallTelescopeImp (type : Expr) (k : Array Expr → Expr → MetaM α) (cleanupAnnotations : Bool) : MetaM α := do
-  forallTelescopeReducingAuxAux (reducing := false) (maxFVars? := none) type k cleanupAnnotations
+@[inline] private def forallTelescopeImp (type : Expr) (k : Array Expr → Expr → MetaM α) : MetaM α := do
+  forallTelescopeReducingAuxAux (reducing := false) (maxFVars? := none) type k
 
 /--
   Given `type` of the form `forall xs, A`, execute `k xs A`.
   This combinator will declare local declarations, create free variables for them,
-  execute `k` with updated local context, and make sure the cache is restored after executing `k`.
-
-  If `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.
--/
-def forallTelescope (type : Expr) (k : Array Expr → Expr → n α) (cleanupAnnotations := false) : n α :=
-  map2MetaM (fun k => forallTelescopeImp type k cleanupAnnotations) k
+  execute `k` with updated local context, and make sure the cache is restored after executing `k`. -/
+def forallTelescope (type : Expr) (k : Array Expr → Expr → n α) : n α :=
+  map2MetaM (fun k => forallTelescopeImp type k) k
 
 /--
 Given a monadic function `f` that takes a type and a term of that type and produces a new term,
@@ -1214,29 +1181,23 @@ and then builds the lambda telescope term for the new term.
 def mapForallTelescope (f : Expr → MetaM Expr) (forallTerm : Expr) : MetaM Expr := do
   mapForallTelescope' (fun _ e => f e) forallTerm
 
-private def forallTelescopeReducingImp (type : Expr) (k : Array Expr → Expr → MetaM α) (cleanupAnnotations : Bool) : MetaM α :=
-  forallTelescopeReducingAux type (maxFVars? := none) k cleanupAnnotations
+private def forallTelescopeReducingImp (type : Expr) (k : Array Expr → Expr → MetaM α) : MetaM α :=
+  forallTelescopeReducingAux type (maxFVars? := none) k
 
 /--
   Similar to `forallTelescope`, but given `type` of the form `forall xs, A`,
-  it reduces `A` and continues building the telescope if it is a `forall`.
+  it reduces `A` and continues building the telescope if it is a `forall`. -/
+def forallTelescopeReducing (type : Expr) (k : Array Expr → Expr → n α) : n α :=
+  map2MetaM (fun k => forallTelescopeReducingImp type k) k
 
-  If `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.
--/
-def forallTelescopeReducing (type : Expr) (k : Array Expr → Expr → n α) (cleanupAnnotations := false) : n α :=
-  map2MetaM (fun k => forallTelescopeReducingImp type k cleanupAnnotations) k
-
-private def forallBoundedTelescopeImp (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → MetaM α) (cleanupAnnotations : Bool) : MetaM α :=
-  forallTelescopeReducingAux type maxFVars? k cleanupAnnotations
+private def forallBoundedTelescopeImp (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → MetaM α) : MetaM α :=
+  forallTelescopeReducingAux type maxFVars? k
 
 /--
   Similar to `forallTelescopeReducing`, stops constructing the telescope when
-  it reaches size `maxFVars`.
-
-  If `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.
--/
-def forallBoundedTelescope (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → n α) (cleanupAnnotations := false) : n α :=
-  map2MetaM (fun k => forallBoundedTelescopeImp type maxFVars? k cleanupAnnotations) k
+  it reaches size `maxFVars`. -/
+def forallBoundedTelescope (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → n α) : n α :=
+  map2MetaM (fun k => forallBoundedTelescopeImp type maxFVars? k) k
 
 private partial def lambdaTelescopeImp (e : Expr) (consumeLet : Bool) (k : Array Expr → Expr → MetaM α) (cleanupAnnotations := false) : MetaM α := do
   process consumeLet (← getLCtx) #[] 0 e
@@ -1526,7 +1487,7 @@ private def withMVarContextImp (mvarId : MVarId) (x : MetaM α) : MetaM α := do
 def _root_.Lean.MVarId.withContext (mvarId : MVarId) : n α → n α :=
   mapMetaM <| withMVarContextImp mvarId
 
-@[deprecated MVarId.withContext (since := "2022-07-15")]
+@[deprecated MVarId.withContext]
 def withMVarContext (mvarId : MVarId) : n α → n α :=
   mvarId.withContext
 

src/Lean/Meta/Canonicalizer.lean

@@ -23,14 +23,16 @@ even if the definitional equality test were inexpensive.
 
 This module aims to efficiently identify terms that are structurally different, definitionally equal, and structurally equal
 when we disregard implicit arguments like `@id (Id Nat) x` and `@id Nat x`. The procedure is straightforward. For each atom,
-we create a hash that ignores all implicit information. Thus the hash for terms are equal `@id (Id Nat) x` and `@id Nat x`.
-To preserve any pre-existing directed acyclic graph (DAG) structure and prevent exponential blowups while computing the hash code,
-we employ unsafe techniques, such as pointer equality. Additionally, we maintain a mapping from hash to lists of terms, where each
-list contains terms sharing the same hash but not definitionally equal. We posit that these lists will be small in practice.
+we create a new abstracted atom by erasing all implicit information. We refer to this abstracted atom as a 'key.' For the two
+terms mentioned, the key would be `@id _ x`, where `_` denotes a placeholder for a dummy term. To preserve any
+pre-existing directed acyclic graph (DAG) structure and prevent exponential blowups while constructing the key, we employ
+unsafe techniques, such as pointer equality. Additionally, we maintain a mapping from keys to lists of terms, where each
+list contains terms sharing the same key but not definitionally equal. We posit that these lists will be small in practice.
 -/
 
 /--
-Auxiliary structure for creating a pointer-equality.
+Auxiliary structure for creating a pointer-equality mapping from `Expr` to `Key`.
+We use this mapping to ensure we preserve the dag-structure of input expressions.
 -/
 structure ExprVisited where
   e : Expr
@@ -42,17 +44,21 @@ unsafe instance : BEq ExprVisited where
 unsafe instance : Hashable ExprVisited where
   hash a := USize.toUInt64 (ptrAddrUnsafe a)
 
+abbrev Key := ExprVisited
+
 /--
 State for the `CanonM` monad.
 -/
 structure State where
-  /-- Mapping from `Expr` to hash. -/
+  /-- "Set" of all keys created so far. This is a hash-consing helper structure available in Lean. -/
+  keys       : ShareCommon.State.{0} Lean.ShareCommon.objectFactory := ShareCommon.State.mk Lean.ShareCommon.objectFactory
+  /-- Mapping from `Expr` to `Key`. See comment at `ExprVisited`. -/
   -- We use `HashMapImp` to ensure we don't have to tag `State` as `unsafe`.
-  cache      : HashMapImp ExprVisited UInt64 := mkHashMapImp
+  cache      : HashMapImp ExprVisited Key := mkHashMapImp
   /--
-  Given a hashcode `k` and `keyToExprs.find? h = some es`, we have that all `es` have hashcode `k`, and
+  Given a key `k` and `keyToExprs.find? k = some es`, we have that all `es` share key `k`, and
   are not definitionally equal modulo the transparency setting used. -/
-  keyToExprs : HashMap UInt64 (List Expr) := mkHashMap
+  keyToExprs : HashMapImp Key (List Expr) := mkHashMapImp
 
 instance : Inhabited State where
   default := {}
@@ -66,20 +72,26 @@ We claim `TransparencyMode.instances` is a good setting for most applications.
 def CanonM.run (x : CanonM α) (transparency := TransparencyMode.instances) : MetaM α :=
   StateRefT'.run' (x transparency) {}
 
-private partial def mkKey (e : Expr) : CanonM UInt64 := do
-  if let some hash := unsafe (← get).cache.find? { e } then
-    return hash
+private def shareCommon (a : α) : CanonM α :=
+  modifyGet fun { keys, cache, keyToExprs } =>
+    let (a, keys) := ShareCommon.State.shareCommon keys a
+    (a, { keys, cache, keyToExprs })
+
+private partial def mkKey (e : Expr) : CanonM Key := do
+  if let some key := unsafe (← get).cache.find? { e } then
+    return key
   else
     let key ← match e with
       | .sort .. | .fvar .. | .bvar .. | .lit .. =>
-        return hash e
+        pure { e := (← shareCommon e) }
       | .const n _ =>
-        return n.hash
+        pure { e := (← shareCommon (.const n [])) }
       | .mvar .. =>
         -- We instantiate assigned metavariables because the
         -- pretty-printer also instantiates them.
         let eNew ← instantiateMVars e
-        if eNew == e then return hash e else mkKey eNew
+        if eNew == e then pure { e := (← shareCommon e) }
+        else mkKey eNew
       | .mdata _ a => mkKey a
       | .app .. =>
         let f := e.getAppFn
@@ -88,23 +100,26 @@ private partial def mkKey (e : Expr) : CanonM UInt64 := do
           unless eNew == e do
             return (← mkKey eNew)
         let info ← getFunInfo f
-        let mut k ← mkKey f
-        for i in [:e.getAppNumArgs] do
+        let args ← e.getAppArgs.mapIdxM fun i arg => do
           if h : i < info.paramInfo.size then
             let info := info.paramInfo[i]
             if info.isExplicit && !info.isProp then
-              k := mixHash k (← mkKey (e.getArg! i))
+              pure (← mkKey arg).e
+            else
+              pure (mkSort 0) -- some dummy value for erasing implicit
           else
-              k := mixHash k (← mkKey (e.getArg! i))
-        return k
-      | .lam _ t b _
-      | .forallE _ t b _ =>
-        return mixHash (← mkKey t) (← mkKey b)
-      | .letE _ _ v b _ =>
-        return mixHash (← mkKey v) (← mkKey b)
-      | .proj _ i s =>
-        return mixHash i.toUInt64 (← mkKey s)
-    unsafe modify fun { cache, keyToExprs} => { keyToExprs, cache := cache.insert { e } key |>.1 }
+            pure (← mkKey arg).e
+        let f' := (← mkKey f).e
+        pure { e := (← shareCommon (mkAppN f' args)) }
+      | .lam n t b i =>
+        pure { e := (← shareCommon (.lam n (← mkKey t).e (← mkKey b).e i)) }
+      | .forallE n t b i =>
+        pure { e := (← shareCommon (.forallE n (← mkKey t).e (← mkKey b).e i)) }
+      | .letE n t v b d =>
+        pure { e := (← shareCommon (.letE n (← mkKey t).e (← mkKey v).e (← mkKey b).e d)) }
+      | .proj t i s =>
+        pure { e := (← shareCommon (.proj t i (← mkKey s).e)) }
+    unsafe modify fun { keys, cache, keyToExprs} => { keys, keyToExprs, cache := cache.insert { e } key |>.1 }
     return key
 
 /--
@@ -120,11 +135,11 @@ def canon (e : Expr) : CanonM Expr := do
         if (← isDefEq e e') then
           return e'
       -- `e` is not definitionally equal to any expression in `es'`. We claim this should be rare.
-      unsafe modify fun { cache, keyToExprs } => { cache, keyToExprs := keyToExprs.insert k (e :: es') }
+      unsafe modify fun { keys, cache, keyToExprs } => { keys, cache, keyToExprs := keyToExprs.insert k (e :: es') |>.1 }
       return e
   else
     -- `e` is the first expression we found with key `k`.
-    unsafe modify fun { cache, keyToExprs } => { cache, keyToExprs := keyToExprs.insert k [e] }
+    unsafe modify fun { keys, cache, keyToExprs } => { keys, cache, keyToExprs := keyToExprs.insert k [e] |>.1 }
     return e
 
 end Canonicalizer

src/Lean/Meta/Closure.lean

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 prelude
 import Lean.MetavarContext
 import Lean.Environment
-import Lean.AddDecl
 import Lean.Util.FoldConsts
 import Lean.Meta.Basic
 import Lean.Meta.Check

src/Lean/Meta/CongrTheorems.lean

@@ -55,8 +55,8 @@ private def setBinderInfosD (ys : Array Expr) (lctx : LocalContext) : LocalConte
 
 partial def mkHCongrWithArity (f : Expr) (numArgs : Nat) : MetaM CongrTheorem := do
   let fType ← inferType f
-  forallBoundedTelescope fType numArgs (cleanupAnnotations := true) fun xs _ =>
-  forallBoundedTelescope fType numArgs (cleanupAnnotations := true) fun ys _ => do
+  forallBoundedTelescope fType numArgs fun xs _ =>
+  forallBoundedTelescope fType numArgs fun ys _ => do
     if xs.size != numArgs then
       throwError "failed to generate hcongr theorem, insufficient number of arguments"
     else
@@ -80,8 +80,8 @@ where
       if  i < xs.size then
         let x := xs[i]!
         let y := ys[i]!
-        let xType := (← inferType x).cleanupAnnotations
-        let yType := (← inferType y).cleanupAnnotations
+        let xType := (← inferType x).consumeTypeAnnotations
+        let yType := (← inferType y).consumeTypeAnnotations
         if xType == yType then
           withLocalDeclD ((`e).appendIndexAfter (i+1)) (← mkEq x y) fun h =>
             loop (i+1) (eqs.push h) (kinds.push CongrArgKind.eq)
@@ -98,9 +98,9 @@ where
     else if let some (_, lhs, _, _) := type.heq? then
       mkHEqRefl lhs
     else
-      forallBoundedTelescope type (some 1) (cleanupAnnotations := true) fun a type =>
+      forallBoundedTelescope type (some 1) fun a type =>
       let a := a[0]!
-      forallBoundedTelescope type (some 1) (cleanupAnnotations := true) fun b motive =>
+      forallBoundedTelescope type (some 1) fun b motive =>
       let b := b[0]!
       let type := type.bindingBody!.instantiate1 a
       withLocalDeclD motive.bindingName! motive.bindingDomain! fun eqPr => do
@@ -159,7 +159,7 @@ private def hasCastLike (kinds : Array CongrArgKind) : Bool :=
   kinds.any fun kind => kind matches CongrArgKind.cast || kind matches CongrArgKind.subsingletonInst
 
 private def withNext (type : Expr) (k : Expr → Expr → MetaM α) : MetaM α := do
-  forallBoundedTelescope type (some 1) (cleanupAnnotations := true) fun xs type => k xs[0]! type
+  forallBoundedTelescope type (some 1) fun xs type => k xs[0]! type
 
 /--
   Test whether we should use `subsingletonInst` kind for instances which depend on `eq`.
@@ -182,7 +182,7 @@ private def getClassSubobjectMask? (f : Expr) : MetaM (Option (Array Bool)) := d
   let .const declName _ := f | return none
   let .ctorInfo val ← getConstInfo declName | return none
   unless isClass (← getEnv) val.induct do return none
-  forallTelescopeReducing val.type (cleanupAnnotations := true) fun xs _ => do
+  forallTelescopeReducing val.type fun xs _ => do
     let env ← getEnv
     let mut mask := #[]
     for i in [:xs.size] do
@@ -255,7 +255,7 @@ where
   mk? (f : Expr) (info : FunInfo) (kinds : Array CongrArgKind) : MetaM (Option CongrTheorem) := do
     try
       let fType ← inferType f
-      forallBoundedTelescope fType kinds.size (cleanupAnnotations := true) fun lhss _ => do
+      forallBoundedTelescope fType kinds.size fun lhss _ => do
         if lhss.size != kinds.size then return none
         let rec go (i : Nat) (rhss : Array Expr) (eqs : Array (Option Expr)) (hyps : Array Expr) : MetaM CongrTheorem := do
           if i == kinds.size then

src/Lean/Meta/Constructions.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.AuxRecursor
-import Lean.AddDecl
 import Lean.Meta.AppBuilder
 
 namespace Lean

src/Lean/Meta/Diagnostics.lean

@@ -60,20 +60,11 @@ def mkDiagSummaryForUnfoldedReducible (counters : PHashMap Name Nat) : MetaM Dia
 def mkDiagSummaryForUsedInstances : MetaM DiagSummary := do
   mkDiagSummary (← get).diag.instanceCounter
 
-def mkDiagSynthPendingFailure (failures : PHashMap Expr MessageData) : MetaM DiagSummary := do
-  if failures.isEmpty then
-    return {}
-  else
-    let mut data := #[]
-    for (_, msg) in failures do
-      data := data.push m!"{if data.isEmpty then "  " else "\n"}{msg}"
-    return { data }
-
-def appendSection (m : MessageData) (cls : Name) (header : String) (s : DiagSummary) (resultSummary := true) : MessageData :=
+def appendSection (m : MessageData) (cls : Name) (header : String) (s : DiagSummary) : MessageData :=
   if s.isEmpty then
     m
   else
-    let header := if resultSummary then s!"{header} (max: {s.max}, num: {s.data.size}):" else header
+    let header := s!"{header} (max: {s.max}, num: {s.data.size}):"
     m ++ .trace { cls } header s.data
 
 def reportDiag : MetaM Unit := do
@@ -84,17 +75,13 @@ def reportDiag : MetaM Unit := do
     let unfoldReducible ← mkDiagSummaryForUnfoldedReducible unfoldCounter
     let heu ← mkDiagSummary (← get).diag.heuristicCounter
     let inst ← mkDiagSummaryForUsedInstances
-    let synthPending ← mkDiagSynthPendingFailure (← get).diag.synthPendingFailures
     let unfoldKernel ← mkDiagSummary (Kernel.getDiagnostics (← getEnv)).unfoldCounter
-    unless unfoldDefault.isEmpty && unfoldInstance.isEmpty && unfoldReducible.isEmpty && heu.isEmpty && inst.isEmpty && synthPending.isEmpty do
+    unless unfoldDefault.isEmpty && unfoldInstance.isEmpty && unfoldReducible.isEmpty && heu.isEmpty && inst.isEmpty do
       let m := MessageData.nil
       let m := appendSection m `reduction "unfolded declarations" unfoldDefault
       let m := appendSection m `reduction "unfolded instances" unfoldInstance
       let m := appendSection m `reduction "unfolded reducible declarations" unfoldReducible
       let m := appendSection m `type_class "used instances" inst
-      let m := appendSection m `type_class
-                 s!"max synth pending failures (maxSynthPendingDepth: {maxSynthPendingDepth.get (← getOptions)}), use `set_option maxSynthPendingDepth <limit>`"
-                 synthPending (resultSummary := false)
       let m := appendSection m `def_eq "heuristic for solving `f a =?= f b`" heu
       let m := appendSection m `kernel "unfolded declarations" unfoldKernel
       let m := m ++ "use `set_option diagnostics.threshold <num>` to control threshold for reporting counters"

src/Lean/Meta/Eqns.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.ReservedNameAction
-import Lean.AddDecl
 import Lean.Meta.Basic
 import Lean.Meta.AppBuilder
 import Lean.Meta.Match.MatcherInfo

src/Lean/Meta/Eval.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich, Leonardo de Moura
 -/
 prelude
-import Lean.AddDecl
 import Lean.Meta.Check
 
 namespace Lean.Meta

src/Lean/Meta/ExprDefEq.lean

@@ -1904,8 +1904,8 @@ private def isDefEqUnitLike (t : Expr) (s : Expr) : MetaM Bool := do
 -/
 private def isDefEqProjInst (t : Expr) (s : Expr) : MetaM LBool := do
   if (← getTransparency) != .instances then return .undef
-  let t? ← unfoldProjInstWhenInstances? t
-  let s? ← unfoldProjInstWhenInstances? s
+  let t? ← unfoldProjInstWhenIntances? t
+  let s? ← unfoldProjInstWhenIntances? s
   if t?.isSome || s?.isSome then
     toLBoolM <| Meta.isExprDefEqAux (t?.getD t) (s?.getD s)
   else

src/Lean/Meta/Injective.lean

@@ -52,13 +52,13 @@ def elimOptParam (type : Expr) : CoreM Expr := do
   Instead of checking the type of every subterm, we only need to check the type of free variables, since free variables introduced in
   the constructor may only appear in the type of other free variables introduced after them.
 -/
-def occursOrInType (lctx : LocalContext) (e : Expr) (t : Expr) : Bool :=
-  t.find? go |>.isSome
-where
-  go s := Id.run do
-    let .fvar fvarId := s | s == e
-    let some decl := lctx.find? fvarId | s == e
-    return s == e || e.occurs decl.type
+def occursOrInType (e : Expr) (t : Expr) : MetaM Bool := do
+  let_fun f (s : Expr) := do
+    if !s.isFVar then
+      return s == e
+    let ty ← inferType s
+    return s == e || e.occurs ty
+  return (← t.findM? f).isSome
 
 private partial def mkInjectiveTheoremTypeCore? (ctorVal : ConstructorVal) (useEq : Bool) : MetaM (Option Expr) := do
   let us := ctorVal.levelParams.map mkLevelParam
@@ -87,7 +87,7 @@ private partial def mkInjectiveTheoremTypeCore? (ctorVal : ConstructorVal) (useE
         match (← whnf type) with
         | Expr.forallE n d b _ =>
           let arg1 := args1.get ⟨i, h⟩
-          if occursOrInType (← getLCtx) arg1 resultType then
+          if ← occursOrInType arg1 resultType then
             mkArgs2 (i + 1) (b.instantiate1 arg1) (args2.push arg1) args2New
           else
             withLocalDecl n (if useEq then BinderInfo.default else BinderInfo.implicit) d fun arg2 =>

src/Lean/Meta/SizeOf.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.List.BasicAux
-import Lean.AddDecl
 import Lean.Meta.AppBuilder
 import Lean.Meta.Instances
 

src/Lean/Meta/SynthInstance.lean

@@ -633,11 +633,14 @@ def main (type : Expr) (maxResultSize : Nat) : MetaM (Option AbstractMVarsResult
      let action : SynthM (Option AbstractMVarsResult) := do
        newSubgoal (← getMCtx) key mvar Waiter.root
        synth
-     tryCatchRuntimeEx
-       (action.run { maxResultSize := maxResultSize, maxHeartbeats := getMaxHeartbeats (← getOptions) } |>.run' {})
-       fun ex =>
+     -- TODO: it would be nice to have a nice notation for the following idiom
+     withCatchingRuntimeEx
+       try
+         withoutCatchingRuntimeEx do
+           action.run { maxResultSize := maxResultSize, maxHeartbeats := getMaxHeartbeats (← getOptions) } |>.run' {}
+       catch ex =>
          if ex.isRuntime then
-           throwError "failed to synthesize{indentExpr type}\n{ex.toMessageData}\n{useDiagnosticMsg}"
+           throwError "failed to synthesize{indentExpr type}\n{ex.toMessageData}"
          else
            throw ex
 
@@ -720,8 +723,7 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
       unless defEq do
         trace[Meta.synthInstance] "{crossEmoji} result type{indentExpr resultType}\nis not definitionally equal to{indentExpr type}"
       return defEq
-    let cacheKey := { localInsts, type, synthPendingDepth := (← read).synthPendingDepth }
-    match s.cache.synthInstance.find? cacheKey with
+    match s.cache.synthInstance.find? (localInsts, type) with
     | some result =>
       trace[Meta.synthInstance] "result {result} (cached)"
       if let some inst := result then
@@ -768,7 +770,7 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
             pure (some result)
           else
             pure none
-      modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey result? }
+      modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert (localInsts, type) result? }
       pure result?
 
 /--
@@ -779,17 +781,14 @@ def trySynthInstance (type : Expr) (maxResultSize? : Option Nat := none) : MetaM
     (toLOptionM <| synthInstance? type maxResultSize?)
     (fun _ => pure LOption.undef)
 
-def throwFailedToSynthesize (type : Expr) : MetaM Expr :=
-  throwError "failed to synthesize{indentExpr type}\n{useDiagnosticMsg}"
-
 def synthInstance (type : Expr) (maxResultSize? : Option Nat := none) : MetaM Expr :=
   catchInternalId isDefEqStuckExceptionId
     (do
       let result? ← synthInstance? type maxResultSize?
       match result? with
       | some result => pure result
-      | none        => throwFailedToSynthesize type)
-    (fun _ => throwFailedToSynthesize type)
+      | none        => throwError "failed to synthesize{indentExpr type}")
+    (fun _ => throwError "failed to synthesize{indentExpr type}")
 
 @[export lean_synth_pending]
 private def synthPendingImp (mvarId : MVarId) : MetaM Bool := withIncRecDepth <| mvarId.withContext do
@@ -803,10 +802,9 @@ private def synthPendingImp (mvarId : MVarId) : MetaM Bool := withIncRecDepth <|
     | none   =>
       return false
     | some _ =>
-      let max := maxSynthPendingDepth.get (← getOptions)
-      if (← read).synthPendingDepth > max then
+      /- TODO: use a configuration option instead of the hard-coded limit `1`. -/
+      if (← read).synthPendingDepth > 1 then
         trace[Meta.synthPending] "too many nested synthPending invocations"
-        recordSynthPendingFailure mvarDecl.type
         return false
       else
         withReader (fun ctx => { ctx with synthPendingDepth := ctx.synthPendingDepth + 1 }) do
@@ -827,7 +825,6 @@ builtin_initialize
   registerTraceClass `Meta.synthInstance
   registerTraceClass `Meta.synthInstance.instances (inherited := true)
   registerTraceClass `Meta.synthInstance.tryResolve (inherited := true)
-  registerTraceClass `Meta.synthInstance.answer (inherited := true)
   registerTraceClass `Meta.synthInstance.resume (inherited := true)
   registerTraceClass `Meta.synthInstance.unusedArgs
   registerTraceClass `Meta.synthInstance.newAnswer

src/Lean/Meta/Tactic.lean

@@ -40,4 +40,3 @@ import Lean.Meta.Tactic.SolveByElim
 import Lean.Meta.Tactic.FunInd
 import Lean.Meta.Tactic.Rfl
 import Lean.Meta.Tactic.Rewrites
-import Lean.Meta.Tactic.Grind

src/Lean/Meta/Tactic/Apply.lean

@@ -185,7 +185,7 @@ def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig :=
     result.forM (·.headBetaType)
     return result
 
-@[deprecated MVarId.apply (since := "2022-07-15")]
+@[deprecated MVarId.apply]
 def apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig := {}) : MetaM (List MVarId) :=
   mvarId.apply e cfg
 
@@ -227,7 +227,7 @@ Apply `And.intro` as much as possible to goal `mvarId`.
 abbrev splitAnd (mvarId : MVarId) : MetaM (List MVarId) :=
   splitAndCore mvarId
 
-@[deprecated splitAnd] -- 2024-03-17
+@[deprecated splitAnd]
 def _root_.Lean.Meta.splitAnd (mvarId : MVarId) : MetaM (List MVarId) :=
   mvarId.splitAnd
 

src/Lean/Meta/Tactic/Assert.lean

@@ -24,7 +24,7 @@ def _root_.Lean.MVarId.assert (mvarId : MVarId) (name : Name) (type : Expr) (val
     mvarId.assign (mkApp newMVar val)
     return newMVar.mvarId!
 
-@[deprecated MVarId.assert (since := "2022-07-15")]
+@[deprecated MVarId.assert]
 def assert (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) : MetaM MVarId :=
   mvarId.assert name type val
 
@@ -46,7 +46,7 @@ def _root_.Lean.MVarId.define (mvarId : MVarId) (name : Name) (type : Expr) (val
     mvarId.assign newMVar
     return newMVar.mvarId!
 
-@[deprecated MVarId.define (since := "2022-07-15")]
+@[deprecated MVarId.define]
 def define (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) : MetaM MVarId := do
   mvarId.define name type val
 
@@ -66,7 +66,7 @@ def _root_.Lean.MVarId.assertExt (mvarId : MVarId) (name : Name) (type : Expr) (
     mvarId.assign (mkApp2 newMVar val rflPrf)
     return newMVar.mvarId!
 
-@[deprecated MVarId.assertExt (since := "2022-07-15")]
+@[deprecated MVarId.assertExt]
 def assertExt (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) (hName : Name := `h) : MetaM MVarId := do
   mvarId.assertExt name type val hName
 
@@ -90,7 +90,7 @@ def _root_.Lean.MVarId.assertAfter (mvarId : MVarId) (fvarId : FVarId) (userName
     subst := subst.insert f (mkFVar fNew)
   return { fvarId := fvarIdNew, mvarId, subst }
 
-@[deprecated MVarId.assertAfter (since := "2022-07-15")]
+@[deprecated MVarId.assertAfter]
 def assertAfter (mvarId : MVarId) (fvarId : FVarId) (userName : Name) (type : Expr) (val : Expr) : MetaM AssertAfterResult := do
   mvarId.assertAfter fvarId userName type val
 
@@ -116,7 +116,7 @@ def _root_.Lean.MVarId.assertHypotheses (mvarId : MVarId) (hs : Array Hypothesis
     mvarId.assign val
     mvarNew.mvarId!.introNP hs.size
 
-@[deprecated MVarId.assertHypotheses (since := "2022-07-15")]
+@[deprecated MVarId.assertHypotheses]
 def assertHypotheses (mvarId : MVarId) (hs : Array Hypothesis) : MetaM (Array FVarId × MVarId) := do
   mvarId.assertHypotheses hs
 

src/Lean/Meta/Tactic/Assumption.lean

@@ -26,7 +26,7 @@ def _root_.Lean.MVarId.assumptionCore (mvarId : MVarId) : MetaM Bool :=
     | none => return false
     | some fvarId => mvarId.assign (mkFVar fvarId); return true
 
-@[deprecated MVarId.assumptionCore (since := "2022-07-15")]
+@[deprecated MVarId.assumptionCore]
 def assumptionCore (mvarId : MVarId) : MetaM Bool :=
   mvarId.assumptionCore
 
@@ -35,7 +35,7 @@ def _root_.Lean.MVarId.assumption (mvarId : MVarId) : MetaM Unit :=
   unless (← mvarId.assumptionCore) do
     throwTacticEx `assumption mvarId
 
-@[deprecated MVarId.assumption (since := "2022-07-15")]
+@[deprecated MVarId.assumption]
 def assumption (mvarId : MVarId) : MetaM Unit :=
   mvarId.assumption
 

src/Lean/Meta/Tactic/AuxLemma.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.AddDecl
 import Lean.Meta.Basic
 
 namespace Lean.Meta

src/Lean/Meta/Tactic/Cases.lean

@@ -200,7 +200,7 @@ private def toCasesSubgoals (s : Array InductionSubgoal) (ctorNames : Array Name
     { ctorName           := ctorName,
       toInductionSubgoal := s }
 
-partial def unifyEqs? (numEqs : Nat) (mvarId : MVarId) (subst : FVarSubst) (caseName? : Option Name := none): MetaM (Option (MVarId × FVarSubst)) := withIncRecDepth do
+partial def unifyEqs? (numEqs : Nat) (mvarId : MVarId) (subst : FVarSubst) (caseName? : Option Name := none): MetaM (Option (MVarId × FVarSubst)) := do
   if numEqs == 0 then
     return some (mvarId, subst)
   else
@@ -269,7 +269,7 @@ Apply `casesOn` using the free variable `majorFVarId` as the major premise (aka
 def _root_.Lean.MVarId.cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array AltVarNames := #[]) (useNatCasesAuxOn : Bool := false) : MetaM (Array CasesSubgoal) :=
   Cases.cases mvarId majorFVarId givenNames (useNatCasesAuxOn := useNatCasesAuxOn)
 
-@[deprecated MVarId.cases (since := "2022-07-15")]
+@[deprecated MVarId.cases]
 def cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array AltVarNames := #[]) : MetaM (Array CasesSubgoal) :=
   Cases.cases mvarId majorFVarId givenNames
 

src/Lean/Meta/Tactic/Cleanup.lean

@@ -72,7 +72,7 @@ where
 abbrev _root_.Lean.MVarId.cleanup (mvarId : MVarId) (toPreserve : Array FVarId := #[]) (indirectProps : Bool := true) : MetaM MVarId := do
   cleanupCore mvarId toPreserve indirectProps
 
-@[deprecated MVarId.cleanup (since := "2022-07-15")]
+@[deprecated MVarId.cleanup]
 abbrev cleanup (mvarId : MVarId) : MetaM MVarId := do
   mvarId.cleanup
 

src/Lean/Meta/Tactic/Clear.lean

@@ -35,7 +35,7 @@ def _root_.Lean.MVarId.clear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId
     pure newMVar.mvarId!
 
 
-@[deprecated MVarId.clear (since := "2022-07-15")]
+@[deprecated MVarId.clear]
 def clear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId :=
   mvarId.clear fvarId
 
@@ -46,7 +46,7 @@ cannot be erased due to forward dependencies.
 def _root_.Lean.MVarId.tryClear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId :=
   mvarId.clear fvarId <|> pure mvarId
 
-@[deprecated MVarId.tryClear (since := "2022-07-15")]
+@[deprecated MVarId.tryClear]
 def tryClear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId :=
   mvarId.tryClear fvarId
 
@@ -56,7 +56,7 @@ Try to erase the given free variables from the goal `mvarId`.
 def _root_.Lean.MVarId.tryClearMany (mvarId : MVarId) (fvarIds : Array FVarId) : MetaM MVarId := do
   fvarIds.foldrM (init := mvarId) fun fvarId mvarId => mvarId.tryClear fvarId
 
-@[deprecated MVarId.tryClearMany (since := "2022-07-15")]
+@[deprecated MVarId.tryClearMany]
 def tryClearMany (mvarId : MVarId) (fvarIds : Array FVarId) : MetaM MVarId := do
   mvarId.tryClearMany fvarIds
 

src/Lean/Meta/Tactic/Constructor.lean

@@ -28,7 +28,7 @@ def _root_.Lean.MVarId.constructor (mvarId : MVarId) (cfg : ApplyConfig := {}) :
             pure ()
         throwTacticEx `constructor mvarId "no applicable constructor found"
 
-@[deprecated MVarId.constructor (since := "2022-07-15")]
+@[deprecated MVarId.constructor]
 def constructor (mvarId : MVarId) (cfg : ApplyConfig := {}) : MetaM (List MVarId) := do
   mvarId.constructor cfg
 
@@ -50,7 +50,7 @@ def _root_.Lean.MVarId.existsIntro (mvarId : MVarId) (w : Expr) : MetaM MVarId :
           | throwTacticEx `exists mvarId "unexpected number of subgoals"
         pure mvarId
 
-@[deprecated MVarId.existsIntro (since := "2022-07-15")]
+@[deprecated MVarId.existsIntro]
 def existsIntro (mvarId : MVarId) (w : Expr) : MetaM MVarId := do
   mvarId.existsIntro w
 

src/Lean/Meta/Tactic/Contradiction.lean

@@ -226,7 +226,7 @@ def _root_.Lean.MVarId.contradiction (mvarId : MVarId) (config : Contradiction.C
   unless (← mvarId.contradictionCore config) do
     throwTacticEx `contradiction mvarId
 
-@[deprecated MVarId.contradiction (since := "2022-07-15")]
+@[deprecated MVarId.contradiction]
 def contradiction (mvarId : MVarId) (config : Contradiction.Config := {}) : MetaM Unit :=
   mvarId.contradiction config
 

src/Lean/Meta/Tactic/Delta.lean

@@ -32,7 +32,7 @@ def _root_.Lean.MVarId.deltaTarget (mvarId : MVarId) (p : Name → Bool) : MetaM
     mvarId.checkNotAssigned `delta
     mvarId.change (← deltaExpand (← mvarId.getType) p) (checkDefEq := false)
 
-@[deprecated MVarId.deltaTarget (since := "2022-07-15")]
+@[deprecated MVarId.deltaTarget]
 def deltaTarget (mvarId : MVarId) (p : Name → Bool) : MetaM MVarId :=
   mvarId.deltaTarget p
 
@@ -44,7 +44,7 @@ def _root_.Lean.MVarId.deltaLocalDecl (mvarId : MVarId) (fvarId : FVarId) (p : N
     mvarId.checkNotAssigned `delta
     mvarId.changeLocalDecl fvarId (← deltaExpand (← mvarId.getType) p) (checkDefEq := false)
 
-@[deprecated MVarId.deltaLocalDecl (since := "2022-07-15")]
+@[deprecated MVarId.deltaLocalDecl]
 def deltaLocalDecl (mvarId : MVarId) (fvarId : FVarId) (p : Name → Bool) : MetaM MVarId :=
   mvarId.deltaLocalDecl fvarId p
 

src/Lean/Meta/Tactic/Generalize.lean

@@ -125,7 +125,7 @@ def _root_.Lean.MVarId.generalize (mvarId : MVarId) (args : Array GeneralizeArg)
     (transparency := TransparencyMode.instances) : MetaM (Array FVarId × MVarId) :=
   generalizeCore mvarId args transparency
 
-@[inherit_doc generalizeCore, deprecated MVarId.generalize (since := "2022-07-15")]
+@[inherit_doc generalizeCore, deprecated MVarId.generalize]
 def generalize (mvarId : MVarId) (args : Array GeneralizeArg)
     (transparency := TransparencyMode.instances) : MetaM (Array FVarId × MVarId) :=
   generalizeCore mvarId args transparency

src/Lean/Meta/Tactic/Grind.lean

@@ -1,11 +0,0 @@
-/-
-Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.Meta.Tactic.Grind.Attr
-import Lean.Meta.Tactic.Grind.RevertAll
-import Lean.Meta.Tactic.Grind.EnsureNoMVar
-import Lean.Meta.Tactic.Grind.Types
-import Lean.Meta.Tactic.Grind.Preprocessor

src/Lean/Meta/Tactic/Grind/Attr.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.Meta.Tactic.Simp.Attr
-import Lean.Meta.Tactic.Simp.Simproc
-
-namespace Lean.Meta.Grind
-open Simp
-
-builtin_initialize grindNormExt : SimpExtension ←
-  registerSimpAttr `grind_norm "simplification/normalization theorems for `grind`"
-
-builtin_initialize grindNormSimprocExt : SimprocExtension ←
-  registerSimprocAttr `grind_norm_proc "simplification/normalization procedured for `grind`" none
-
-end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/EnsureNoMVar.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.Meta.Tactic.Util
-
-namespace Lean.Meta.Grind
-
-/--
-Throws an exception if target of the given goal contains metavariables.
--/
-def _root_.Lean.MVarId.ensureNoMVar (mvarId : MVarId) : MetaM Unit := do
-  let type ← instantiateMVars (← mvarId.getType)
-  if type.hasExprMVar then
-    throwTacticEx `grind mvarId "goal contains metavariables"
-
-end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Preprocessor.lean

@@ -1,123 +0,0 @@
-/-
-Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.Meta.Canonicalizer
-import Lean.Meta.Tactic.Util
-import Lean.Meta.Tactic.Intro
-import Lean.Meta.Tactic.Simp.Main
-import Lean.Meta.Tactic.Grind.Attr
-import Lean.Meta.Tactic.Grind.RevertAll
-import Lean.Meta.Tactic.Grind.EnsureNoMVar
-import Lean.Meta.Tactic.Grind.Types
-
-namespace Lean.Meta.Grind
-namespace Preprocessor
-
--- TODO: use congruence closure and decision procedures during pre-processing
--- TODO: implement `simp` discharger using preprocessor state
-
-structure Context where
-  simp     : Simp.Context
-  simprocs : Array Simp.Simprocs
-  deriving Inhabited
-
-structure State where
-  canon : Canonicalizer.State := {}
-  todo  : List Goal := []
-  goals : PArray Goal := {}
-  simpStats : Simp.Stats := {}
-  deriving Inhabited
-
-structure Result where
-  canon : Canonicalizer.State := {}
-  goals : PArray Goal := {}
-  deriving Inhabited
-
-abbrev M := ReaderT Context $ StateRefT State MetaM
-
-def mkInitialState (mvarId : MVarId) : State :=
-  { todo := [ mkGoal mvarId ] }
-
-def M.run (x : M α) (mvarId : MVarId) : MetaM α := do
-  let thms ← grindNormExt.getTheorems
-  let simprocs := #[(← grindNormSimprocExt.getSimprocs)]
-  let simp : Simp.Context := {
-    simpTheorems := #[thms]
-    congrTheorems := (← getSimpCongrTheorems)
-  }
-  x { simp, simprocs } |>.run' (mkInitialState mvarId)
-
-def simpHyp? (mvarId : MVarId) (fvarId : FVarId) : M (Option (FVarId × MVarId)) := do
-  let simpStats := (← get).simpStats
-  let (result, simpStats) ← simpLocalDecl mvarId fvarId (← read).simp (← read).simprocs (stats := simpStats)
-  modify fun s => { s with simpStats }
-  return result
-
-def getNextGoal? : M (Option Goal) := do
-  match (← get).todo with
-  | [] => return none
-  | goal :: todo =>
-    modify fun s => { s with todo }
-    return some goal
-
-inductive IntroResult where
-  | done | closed
-  | newHyp (fvarId : FVarId) (goal : Goal)
-  | newLocal (fvarId : FVarId) (goal : Goal)
-
-def introNext (goal : Goal) : M IntroResult := do
-  let target ← goal.mvarId.getType
-  if target.isArrow then
-    let (fvarId, mvarId) ← goal.mvarId.intro1P
-    -- TODO: canonicalize subterms
-    mvarId.withContext do
-    if (← isProp (← fvarId.getType)) then
-      let some (fvarId, mvarId) ← simpHyp? mvarId fvarId | return .closed
-      return .newHyp fvarId { goal with mvarId }
-    else
-      return .newLocal fvarId { goal with mvarId }
-  else if target.isLet || target.isForall then
-    -- TODO: canonicalize subterms
-    -- TODO: If forall is of the form `∀ h : <proposition>, A h`, generalize `h`.
-    let (fvarId, mvarId) ← goal.mvarId.intro1P
-    return .newLocal fvarId { goal with mvarId }
-  else
-    return .done
-
-def pushTodo (goal : Goal) : M Unit :=
-  modify fun s => { s with todo := goal :: s.todo }
-
-def pushResult (goal : Goal) : M Unit :=
-  modify fun s => { s with goals := s.goals.push goal }
-
-partial def main (mvarId : MVarId) : MetaM Result := do
-  mvarId.ensureNoMVar
-  let mvarId ← mvarId.revertAll
-  mvarId.ensureNoMVar
-  let s ← (loop *> get) |>.run mvarId
-  return { s with }
-where
-  loop : M Unit := do
-    let some goal ← getNextGoal? | return ()
-    trace[Meta.debug] "{goal.mvarId}"
-    match (← introNext goal) with
-    | .closed => loop
-    | .done =>
-      -- TODO: apply `byContradiction`
-      pushResult goal
-      return ()
-    | .newHyp fvarId goal =>
-      -- TODO: apply eliminators
-      let clause ← goal.mvarId.withContext do mkInputClause fvarId
-      pushTodo { goal with clauses := goal.clauses.push clause }
-      loop
-    | .newLocal _ goal =>
-      -- TODO: apply eliminators
-      pushTodo goal
-      loop
-
-end Preprocessor
-end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/RevertAll.lean

@@ -1,33 +0,0 @@
-/-
-Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.Meta.Tactic.Util
-
-namespace Lean.Meta.Grind
-
-/--
-Revert all free variables at goal `mvarId`.
--/
-def _root_.Lean.MVarId.revertAll (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
-  mvarId.checkNotAssigned `revertAll
-  let fvarIds := (← getLCtx).getFVarIds
-  let fvars ← fvarIds.filterMapM fun fvarId => do
-    if (← fvarId.getDecl).isAuxDecl then
-      return none
-    else
-      return some (mkFVar fvarId)
-  let tag ← mvarId.getTag
-  mvarId.setKind .natural
-  let (e, _) ←
-    try
-      liftMkBindingM <| MetavarContext.revert fvars mvarId (preserveOrder := true)
-    finally
-      mvarId.setKind .syntheticOpaque
-  let mvar := e.getAppFn
-  mvar.mvarId!.setTag tag
-  return mvar.mvarId!
-
-end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -1,31 +0,0 @@
-/-
-Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.Meta.Basic
-import Lean.Meta.Tactic.Util
-
-namespace Lean.Meta.Grind
-
-structure Clause where
-  expr  : Expr
-  proof : Expr
-  deriving Inhabited
-
-def mkInputClause (fvarId : FVarId) : MetaM Clause :=
-  return { expr := (← fvarId.getType), proof := mkFVar fvarId }
-
-structure Goal where
-  mvarId  : MVarId
-  clauses : PArray Clause := {}
-  deriving Inhabited
-
-def mkGoal (mvarId : MVarId) : Goal :=
-  { mvarId }
-
-def Goal.admit (goal : Goal) : MetaM Unit :=
-  goal.mvarId.admit
-
-end Lean.Meta.Grind

src/Lean/Meta/Tactic/Induction.lean

@@ -207,7 +207,7 @@ def _root_.Lean.MVarId.induction (mvarId : MVarId) (majorFVarId : FVarId) (recur
           | _ =>
            throwTacticEx `induction mvarId "major premise is not of the form (C ...)"
 
-@[deprecated MVarId.induction (since := "2022-07-15")]
+@[deprecated MVarId.induction]
 def induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (givenNames : Array AltVarNames := #[]) : MetaM (Array InductionSubgoal) :=
   mvarId.induction majorFVarId recursorName givenNames
 

src/Lean/Meta/Tactic/Intro.lean

@@ -132,7 +132,7 @@ Introduce `n` binders in the goal `mvarId`.
 abbrev _root_.Lean.MVarId.introN (mvarId : MVarId) (n : Nat) (givenNames : List Name := []) (useNamesForExplicitOnly := false) : MetaM (Array FVarId × MVarId) :=
   introNCore mvarId n givenNames (useNamesForExplicitOnly := useNamesForExplicitOnly) (preserveBinderNames := false)
 
-@[deprecated MVarId.introN (since := "2022-07-15")]
+@[deprecated MVarId.introN]
 abbrev introN (mvarId : MVarId) (n : Nat) (givenNames : List Name := []) (useNamesForExplicitOnly := false) : MetaM (Array FVarId × MVarId) :=
   mvarId.introN n givenNames useNamesForExplicitOnly
 
@@ -143,7 +143,7 @@ The suffix `P` stands for "preserving`.
 abbrev _root_.Lean.MVarId.introNP (mvarId : MVarId) (n : Nat) : MetaM (Array FVarId × MVarId) :=
   introNCore mvarId n [] (useNamesForExplicitOnly := false) (preserveBinderNames := true)
 
-@[deprecated MVarId.introNP (since := "2022-07-15")]
+@[deprecated MVarId.introNP]
 abbrev introNP (mvarId : MVarId) (n : Nat) : MetaM (Array FVarId × MVarId) :=
   mvarId.introNP n
 
@@ -154,7 +154,7 @@ def _root_.Lean.MVarId.intro (mvarId : MVarId) (name : Name) : MetaM (FVarId ×
   let (fvarIds, mvarId) ← mvarId.introN 1 [name]
   return (fvarIds[0]!, mvarId)
 
-@[deprecated MVarId.intro (since := "2022-07-15")]
+@[deprecated MVarId.intro]
 def intro (mvarId : MVarId) (name : Name) : MetaM (FVarId × MVarId) := do
   mvarId.intro name
 
@@ -169,7 +169,7 @@ does not start with a forall, lambda or let. -/
 abbrev _root_.Lean.MVarId.intro1 (mvarId : MVarId) : MetaM (FVarId × MVarId) :=
   intro1Core mvarId false
 
-@[deprecated MVarId.intro1 (since := "2022-07-15")]
+@[deprecated MVarId.intro1]
 abbrev intro1 (mvarId : MVarId) : MetaM (FVarId × MVarId) :=
   mvarId.intro1
 
@@ -180,7 +180,7 @@ does not start with a forall, lambda or let. -/
 abbrev _root_.Lean.MVarId.intro1P (mvarId : MVarId) : MetaM (FVarId × MVarId) :=
   intro1Core mvarId true
 
-@[deprecated MVarId.intro1P (since := "2022-07-15")]
+@[deprecated MVarId.intro1P]
 abbrev intro1P (mvarId : MVarId) : MetaM (FVarId × MVarId) :=
   mvarId.intro1P
 
@@ -206,7 +206,7 @@ def _root_.Lean.MVarId.intros (mvarId : MVarId) : MetaM (Array FVarId × MVarId)
   else
     mvarId.introN n
 
-@[deprecated MVarId.intros (since := "2022-07-15")]
+@[deprecated MVarId.intros]
 def intros (mvarId : MVarId) : MetaM (Array FVarId × MVarId) := do
   mvarId.intros
 

src/Lean/Meta/Tactic/Refl.lean

@@ -37,11 +37,11 @@ def _root_.Lean.MVarId.refl (mvarId : MVarId) : MetaM Unit := do
     let α := targetType.appFn!.appFn!.appArg!
     mvarId.assign (mkApp2 (mkConst ``Eq.refl  us) α lhs)
 
-@[deprecated MVarId.refl (since := "2022-07-15")]
+@[deprecated MVarId.refl]
 def refl (mvarId : MVarId) : MetaM Unit := do
   mvarId.refl
 
-@[deprecated MVarId.refl (since := "2022-07-15")]
+@[deprecated MVarId.refl]
 def _root_.Lean.MVarId.applyRefl (mvarId : MVarId) (msg : MessageData := "refl failed") : MetaM Unit :=
   try mvarId.refl catch _ => throwError msg
 

src/Lean/Meta/Tactic/Rename.lean

@@ -18,7 +18,7 @@ def _root_.Lean.MVarId.rename (mvarId : MVarId) (fvarId : FVarId) (userNameNew :
   mvarId.assign mvarNew
   return mvarNew.mvarId!
 
-@[deprecated MVarId.rename (since := "2022-07-15")]
+@[deprecated MVarId.rename]
 def rename (mvarId : MVarId) (fvarId : FVarId) (newUserName : Name) : MetaM MVarId :=
   mvarId.rename fvarId newUserName
 

src/Lean/Meta/Tactic/Replace.lean

@@ -32,7 +32,7 @@ def _root_.Lean.MVarId.replaceTargetEq (mvarId : MVarId) (targetNew : Expr) (eqP
     mvarId.assign val
     return mvarNew.mvarId!
 
-@[deprecated MVarId.replaceTargetEq (since := "2022-07-15")]
+@[deprecated MVarId.replaceTargetEq]
 def replaceTargetEq (mvarId : MVarId) (targetNew : Expr) (eqProof : Expr) : MetaM MVarId :=
   mvarId.replaceTargetEq targetNew eqProof
 
@@ -56,7 +56,7 @@ def _root_.Lean.MVarId.replaceTargetDefEq (mvarId : MVarId) (targetNew : Expr) :
       mvarId.assign newVal
       return mvarNew.mvarId!
 
-@[deprecated MVarId.replaceTargetDefEq (since := "2022-07-15")]
+@[deprecated MVarId.replaceTargetDefEq]
 def replaceTargetDefEq (mvarId : MVarId) (targetNew : Expr) : MetaM MVarId :=
   mvarId.replaceTargetDefEq targetNew
 
@@ -102,7 +102,7 @@ where
 abbrev _root_.Lean.MVarId.replaceLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (eqProof : Expr) : MetaM AssertAfterResult :=
   replaceLocalDeclCore mvarId fvarId typeNew eqProof
 
-@[deprecated MVarId.replaceLocalDecl (since := "2022-07-15")]
+@[deprecated MVarId.replaceLocalDecl]
 abbrev replaceLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (eqProof : Expr) : MetaM AssertAfterResult :=
   mvarId.replaceLocalDecl fvarId typeNew eqProof
 
@@ -121,7 +121,7 @@ def _root_.Lean.MVarId.replaceLocalDeclDefEq (mvarId : MVarId) (fvarId : FVarId)
       mvarId.assign mvarNew
       return mvarNew.mvarId!
 
-@[deprecated MVarId.replaceLocalDeclDefEq (since := "2022-07-15")]
+@[deprecated MVarId.replaceLocalDeclDefEq]
 def replaceLocalDeclDefEq (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) : MetaM MVarId := do
   mvarId.replaceLocalDeclDefEq fvarId typeNew
 
@@ -137,7 +137,7 @@ def _root_.Lean.MVarId.change (mvarId : MVarId) (targetNew : Expr) (checkDefEq :
       throwTacticEx `change mvarId m!"given type{indentExpr targetNew}\nis not definitionally equal to{indentExpr target}"
   mvarId.replaceTargetDefEq targetNew
 
-@[deprecated MVarId.change (since := "2022-07-15")]
+@[deprecated MVarId.change]
 def change (mvarId : MVarId) (targetNew : Expr) (checkDefEq := true) : MetaM MVarId := mvarId.withContext do
   mvarId.change targetNew checkDefEq
 
@@ -222,7 +222,7 @@ def _root_.Lean.MVarId.modifyTarget (mvarId : MVarId) (f : Expr → MetaM Expr)
     mvarId.checkNotAssigned `modifyTarget
     mvarId.change (← f (← mvarId.getType)) (checkDefEq := false)
 
-@[deprecated modifyTarget (since := "2022-07-15")]
+@[deprecated modifyTarget]
 def modifyTarget (mvarId : MVarId) (f : Expr → MetaM Expr) : MetaM MVarId := do
   mvarId.modifyTarget f
 
@@ -237,7 +237,7 @@ def _root_.Lean.MVarId.modifyTargetEqLHS (mvarId : MVarId) (f : Expr → MetaM E
      else
        throwTacticEx `modifyTargetEqLHS mvarId m!"equality expected{indentExpr target}"
 
-@[deprecated MVarId.modifyTargetEqLHS (since := "2022-07-15")]
+@[deprecated MVarId.modifyTargetEqLHS]
 def modifyTargetEqLHS (mvarId : MVarId) (f : Expr → MetaM Expr) : MetaM MVarId := do
   mvarId.modifyTargetEqLHS f
 

src/Lean/Meta/Tactic/Revert.lean

@@ -53,7 +53,7 @@ def _root_.Lean.MVarId.revertAfter (mvarId : MVarId) (fvarId : FVarId) : MetaM (
     let fvarIds := (← getLCtx).foldl (init := #[]) (start := localDecl.index+1) fun fvarIds decl => fvarIds.push decl.fvarId
     mvarId.revert fvarIds (preserveOrder := true) (clearAuxDeclsInsteadOfRevert := true)
 
-@[deprecated MVarId.revert (since := "2022-07-15")]
+@[deprecated MVarId.revert]
 def revert (mvarId : MVarId) (fvarIds : Array FVarId) (preserveOrder : Bool := false) : MetaM (Array FVarId × MVarId) := do
   mvarId.revert fvarIds preserveOrder
 

src/Lean/Meta/Tactic/Rewrite.lean

@@ -74,7 +74,7 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
     | none =>
       cont heq heqType
 
-@[deprecated MVarId.rewrite (since := "2022-07-15")]
+@[deprecated MVarId.rewrite]
 def rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
     (symm : Bool := false) (config := { : Rewrite.Config }) : MetaM RewriteResult :=
   mvarId.rewrite e heq symm config

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -662,30 +662,30 @@ def main (e : Expr) (ctx : Context) (stats : Stats := {}) (methods : Methods :=
     trace[Meta.Tactic.simp.numSteps] "{s.numSteps}"
     return (r, { s with })
 where
-  simpMain (e : Expr) : SimpM Result :=
-    tryCatchRuntimeEx
-      (simp e)
-      fun ex => do
-        reportDiag (← get).diag
-        if ex.isRuntime then
-          throwNestedTacticEx `simp ex
-        else
-          throw ex
+  simpMain (e : Expr) : SimpM Result := withCatchingRuntimeEx do
+    try
+      withoutCatchingRuntimeEx <| simp e
+    catch ex =>
+      reportDiag (← get).diag
+      if ex.isRuntime then
+        throwNestedTacticEx `simp ex
+      else
+        throw ex
 
 def dsimpMain (e : Expr) (ctx : Context) (stats : Stats := {}) (methods : Methods := {}) : MetaM (Expr × Stats) := do
   withSimpContext ctx do
     let (r, s) ← dsimpMain e methods.toMethodsRef ctx |>.run { stats with }
     pure (r, { s with })
 where
-  dsimpMain (e : Expr) : SimpM Expr :=
-    tryCatchRuntimeEx
-      (dsimp e)
-      fun ex => do
-        reportDiag (← get).diag
-        if ex.isRuntime then
-          throwNestedTacticEx `simp ex
-        else
-          throw ex
+  dsimpMain (e : Expr) : SimpM Expr := withCatchingRuntimeEx do
+    try
+      withoutCatchingRuntimeEx <| dsimp e
+    catch ex =>
+      reportDiag (← get).diag
+      if ex.isRuntime then
+        throwNestedTacticEx `simp ex
+      else
+        throw ex
 
 end Simp
 open Simp (SimprocsArray Stats)

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -123,7 +123,6 @@ structure State where
 structure Stats where
   usedTheorems : UsedSimps := {}
   diag : Diagnostics := {}
-  deriving Inhabited
 
 private opaque MethodsRefPointed : NonemptyType.{0}
 

src/Lean/Meta/Tactic/UnifyEq.lean

@@ -21,11 +21,6 @@ structure UnifyEqResult where
   subst     : FVarSubst
   numNewEqs : Nat := 0
 
-private def toOffset? (e : Expr) : MetaM (Option (Expr × Nat)) := do
-  match (← evalNat e) with
-  | some k => return some (mkNatLit 0, k)
-  | none => isOffset? e
-
 /--
   Helper method for methods such as `Cases.unifyEqs?`.
   Given the given goal `mvarId` containing the local hypothesis `eqFVarId`, it performs the following operations:
@@ -74,30 +69,7 @@ def unifyEq? (mvarId : MVarId) (eqFVarId : FVarId) (subst : FVarSubst := {})
             return none -- this alternative has been solved
           else
             throwError "dependent elimination failed, failed to solve equation{indentExpr eqDecl.type}"
-        /- Special support for offset equalities -/
-        let injectionOffset? (a b : Expr) := do
-          unless (← getEnv).contains ``Nat.elimOffset do return none
-          let some (xa, ka) ← toOffset? a | return none
-          let some (xb, kb) ← toOffset? b | return none
-          if ka == 0 || kb == 0 then return none -- use default noConfusion
-          let (x, y, k) ← if ka < kb then
-            pure (xa, (← mkAdd xb (mkNatLit (kb - ka))), ka)
-          else if ka = kb then
-            pure (xa, xb, ka)
-          else
-            pure ((← mkAdd xa (mkNatLit (ka - kb))), xb, kb)
-          let target ← mvarId.getType
-          let u ← getLevel target
-          let newTarget ← mkArrow (← mkEq x y) target
-          let tag ← mvarId.getTag
-          let newMVar ← mkFreshExprSyntheticOpaqueMVar newTarget tag
-          let val := mkAppN (mkConst ``Nat.elimOffset [u]) #[target, x, y, mkNatLit k, eqDecl.toExpr, newMVar]
-          mvarId.assign val
-          let mvarId ← newMVar.mvarId!.tryClear eqDecl.fvarId
-          return some mvarId
         let rec injection (a b : Expr) := do
-          if let some mvarId ← injectionOffset? a b then
-            return some { mvarId, numNewEqs := 1, subst }
           if (← isConstructorApp a <&&> isConstructorApp b) then
             /- ctor_i ... = ctor_j ... -/
             match (← injectionCore mvarId eqFVarId) with

src/Lean/Meta/Tactic/Util.lean

@@ -15,14 +15,14 @@ namespace Lean.Meta
 def _root_.Lean.MVarId.getTag (mvarId : MVarId) : MetaM Name :=
   return (← mvarId.getDecl).userName
 
-@[deprecated MVarId.getTag (since := "2022-07-15")]
+@[deprecated MVarId.getTag]
 def getMVarTag (mvarId : MVarId) : MetaM Name :=
   mvarId.getTag
 
 def _root_.Lean.MVarId.setTag (mvarId : MVarId) (tag : Name) : MetaM Unit := do
   modify fun s => { s with mctx := s.mctx.setMVarUserName mvarId tag }
 
-@[deprecated MVarId.setTag (since := "2022-07-15")]
+@[deprecated MVarId.setTag]
 def setMVarTag (mvarId : MVarId) (tag : Name) : MetaM Unit := do
   mvarId.setTag tag
 
@@ -49,7 +49,7 @@ def _root_.Lean.MVarId.checkNotAssigned (mvarId : MVarId) (tacticName : Name) :
   if (← mvarId.isAssigned) then
     throwTacticEx tacticName mvarId "metavariable has already been assigned"
 
-@[deprecated MVarId.checkNotAssigned (since := "2022-07-15")]
+@[deprecated MVarId.checkNotAssigned]
 def checkNotAssigned (mvarId : MVarId) (tacticName : Name) : MetaM Unit := do
   mvarId.checkNotAssigned tacticName
 
@@ -57,7 +57,7 @@ def checkNotAssigned (mvarId : MVarId) (tacticName : Name) : MetaM Unit := do
 def _root_.Lean.MVarId.getType (mvarId : MVarId) : MetaM Expr :=
   return (← mvarId.getDecl).type
 
-@[deprecated MVarId.getType (since := "2022-07-15")]
+@[deprecated MVarId.getType]
 def getMVarType (mvarId : MVarId) : MetaM Expr :=
   mvarId.getType
 
@@ -69,7 +69,7 @@ weak head normal form. -/
 def _root_.Lean.MVarId.getType' (mvarId : MVarId) : MetaM Expr := do
   instantiateMVars (← whnf (← mvarId.getType))
 
-@[deprecated MVarId.getType' (since := "2022-07-15")]
+@[deprecated MVarId.getType']
 def getMVarType' (mvarId : MVarId) : MetaM Expr := do
   mvarId.getType'
 
@@ -83,7 +83,7 @@ def _root_.Lean.MVarId.admit (mvarId : MVarId) (synthetic := true) : MetaM Unit
     let val ← mkSorry mvarType synthetic
     mvarId.assign val
 
-@[deprecated MVarId.admit (since := "2022-07-15")]
+@[deprecated MVarId.admit]
 def admit (mvarId : MVarId) (synthetic := true) : MetaM Unit :=
   mvarId.admit synthetic
 
@@ -91,7 +91,7 @@ def admit (mvarId : MVarId) (synthetic := true) : MetaM Unit :=
 def _root_.Lean.MVarId.headBetaType (mvarId : MVarId) : MetaM Unit := do
   mvarId.setType (← mvarId.getType).headBeta
 
-@[deprecated MVarId.headBetaType (since := "2022-07-15")]
+@[deprecated MVarId.headBetaType]
 def headBetaMVarType (mvarId : MVarId) : MetaM Unit := do
   mvarId.headBetaType
 
@@ -123,7 +123,7 @@ def _root_.Lean.MVarId.getNondepPropHyps (mvarId : MVarId) : MetaM (Array FVarId
           result := result.push localDecl.fvarId
       return result
 
-@[deprecated MVarId.getNondepPropHyps (since := "2022-07-15")]
+@[deprecated MVarId.getNondepPropHyps]
 def getNondepPropHyps (mvarId : MVarId) : MetaM (Array FVarId) :=
   mvarId.getNondepPropHyps
 

src/Lean/Meta/WHNF.lean

@@ -712,11 +712,11 @@ mutual
     | _ => return none
 
   /--
-    Auxiliary method for unfolding a class projection when transparency is set to `TransparencyMode.instances`.
+    Auxiliary method for unfolding a class projection. when transparency is set to `TransparencyMode.instances`.
     Recall that class instance projections are not marked with `[reducible]` because we want them to be
     in "reducible canonical form".
   -/
-  partial def unfoldProjInstWhenInstances? (e : Expr) : MetaM (Option Expr) := do
+  partial def unfoldProjInstWhenIntances? (e : Expr) : MetaM (Option Expr) := do
     if (← getTransparency) != TransparencyMode.instances then
       return none
     else
@@ -726,7 +726,7 @@ mutual
   partial def unfoldDefinition? (e : Expr) : MetaM (Option Expr) :=
     match e with
     | .app f _ =>
-      matchConstAux f.getAppFn (fun _ => unfoldProjInstWhenInstances? e) fun fInfo fLvls => do
+      matchConstAux f.getAppFn (fun _ => unfoldProjInstWhenIntances? e) fun fInfo fLvls => do
         if fInfo.levelParams.length != fLvls.length then
           return none
         else

src/Lean/MetavarContext.lean

@@ -383,14 +383,14 @@ def isLevelMVarAssigned [Monad m] [MonadMCtx m] (mvarId : LMVarId) : m Bool :=
 def _root_.Lean.MVarId.isAssigned [Monad m] [MonadMCtx m] (mvarId : MVarId) : m Bool :=
   return (← getMCtx).eAssignment.contains mvarId
 
-@[deprecated MVarId.isAssigned (since := "2022-07-15")]
+@[deprecated MVarId.isAssigned]
 def isExprMVarAssigned [Monad m] [MonadMCtx m] (mvarId : MVarId) : m Bool := do
   mvarId.isAssigned
 
 def _root_.Lean.MVarId.isDelayedAssigned [Monad m] [MonadMCtx m] (mvarId : MVarId) : m Bool :=
   return (← getMCtx).dAssignment.contains mvarId
 
-@[deprecated MVarId.isDelayedAssigned (since := "2022-07-15")]
+@[deprecated MVarId.isDelayedAssigned]
 def isMVarDelayedAssigned [Monad m] [MonadMCtx m] (mvarId : MVarId) : m Bool := do
   mvarId.isDelayedAssigned
 
@@ -422,7 +422,7 @@ def _root_.Lean.MVarId.isAssignable [Monad m] [MonadMCtx m] (mvarId : MVarId) :
   let decl := mctx.getDecl mvarId
   return decl.depth == mctx.depth
 
-@[deprecated MVarId.isAssignable (since := "2022-07-15")]
+@[deprecated MVarId.isAssignable]
 def isExprMVarAssignable [Monad m] [MonadMCtx m] (mvarId : MVarId) : m Bool := do
   mvarId.isAssignable
 
@@ -492,7 +492,7 @@ This is a low-level API, and it is safer to use `isDefEq (mkMVar mvarId) x`.
 def _root_.Lean.MVarId.assign [MonadMCtx m] (mvarId : MVarId) (val : Expr) : m Unit :=
   modifyMCtx fun m => { m with eAssignment := m.eAssignment.insert mvarId val }
 
-@[deprecated MVarId.assign (since := "2022-07-15")]
+@[deprecated MVarId.assign]
 def assignExprMVar [MonadMCtx m] (mvarId : MVarId) (val : Expr) : m Unit :=
   mvarId.assign val
 

src/Lean/ReducibilityAttrs.lean

@@ -184,9 +184,4 @@ def isIrreducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
   | .irreducible => return true
   | _ => return false
 
-/-- Set the given declaration as `[irreducible]` -/
-def setIrreducibleAttribute [Monad m] [MonadEnv m] (declName : Name) : m Unit := do
-  setReducibilityStatus declName ReducibilityStatus.irreducible
-
-
 end Lean

src/Lean/Replay.lean

@@ -5,7 +5,6 @@ Authors: Scott Morrison
 -/
 prelude
 import Lean.CoreM
-import Lean.AddDecl
 import Lean.Util.FoldConsts
 
 /-!
@@ -57,7 +56,7 @@ def throwKernelException (ex : KernelException) : M Unit := do
 
 /-- Add a declaration, possibly throwing a `KernelException`. -/
 def addDecl (d : Declaration) : M Unit := do
-  match (← get).env.addDecl {} d with
+  match (← get).env.addDecl d with
   | .ok env => modify fun s => { s with env := env }
   | .error ex => throwKernelException ex
 

src/Lean/ResolveName.lean

@@ -384,16 +384,6 @@ After `open Foo open Boo`, we have
 def resolveGlobalConstNoOverload [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Syntax) : m Name := do
   ensureNonAmbiguous id (← resolveGlobalConst id)
 
-/--
-Finds a name that unambiguously resolves to the given name `n₀`.
-Considers suffixes of `n₀` and suffixes of aliases of `n₀` when "unresolving".
-Aliases are considered first.
-
-When `fullNames` is true, returns either `n₀` or `_root_.n₀`.
-
-This function is meant to be used for pretty printing.
-If `n₀` is an accessible name, then the result will be an accessible name.
--/
 def unresolveNameGlobal [Monad m] [MonadResolveName m] [MonadEnv m] (n₀ : Name) (fullNames := false) : m Name := do
   if n₀.hasMacroScopes then return n₀
   if fullNames then
@@ -403,19 +393,21 @@ def unresolveNameGlobal [Monad m] [MonadResolveName m] [MonadEnv m] (n₀ : Name
   let mut initialNames := (getRevAliases (← getEnv) n₀).toArray
   initialNames := initialNames.push (rootNamespace ++ n₀)
   for initialName in initialNames do
-    if let some n ← unresolveNameCore initialName then
-      return n
+    match (← unresolveNameCore initialName) with
+    | none => continue
+    | some n => return n
   return n₀ -- if can't resolve, return the original
 where
   unresolveNameCore (n : Name) : m (Option Name) := do
-    if n.hasMacroScopes then return none
     let mut revComponents := n.componentsRev
     let mut candidate := Name.anonymous
-    for cmpt in revComponents do
-      candidate := Name.appendCore cmpt candidate
-      if let [(potentialMatch, _)] ← resolveGlobalName candidate then
-        if potentialMatch == n₀ then
-          return some candidate
+    for _ in [:revComponents.length] do
+      match revComponents with
+      | [] => return none
+      | cmpt::rest => candidate := Name.appendCore cmpt candidate; revComponents := rest
+      match (← resolveGlobalName candidate) with
+      | [(potentialMatch, _)] => if potentialMatch == n₀ then return some candidate else continue
+      | _ => continue
     return none
 
 end Lean

src/Lean/Util/FindExpr.lean

@@ -11,17 +11,17 @@ namespace Lean
 namespace Expr
 namespace FindImpl
 
-unsafe abbrev FindM := StateT (PtrSet Expr) Id
+unsafe abbrev FindM (m) := StateT (PtrSet Expr) m
 
-@[inline] unsafe def checkVisited (e : Expr) : OptionT FindM Unit := do
+@[inline] unsafe def checkVisited [Monad m] (e : Expr) : OptionT (FindM m) Unit := do
   if (← get).contains e then
     failure
   modify fun s => s.insert e
 
-unsafe def findM? (p : Expr → Bool) (e : Expr) : OptionT FindM Expr :=
+unsafe def findM? [Monad m] (p : Expr → m Bool) (e : Expr) : OptionT (FindM m) Expr :=
   let rec visit (e : Expr) := do
     checkVisited e
-    if p e then
+    if ← p e then
       pure e
     else match e with
       | .forallE _ d b _ => visit d <|> visit b
@@ -33,29 +33,35 @@ unsafe def findM? (p : Expr → Bool) (e : Expr) : OptionT FindM Expr :=
       | _                => failure
   visit e
 
-unsafe def findUnsafe? (p : Expr → Bool) (e : Expr) : Option Expr :=
-  Id.run <| findM? p e |>.run' mkPtrSet
+unsafe def findUnsafeM? {m} [Monad m] (p : Expr → m Bool) (e : Expr) : m (Option Expr) :=
+  findM? p e |>.run' mkPtrSet
+
+@[inline] unsafe def findUnsafe? (p : Expr → Bool) (e : Expr) : Option Expr := findUnsafeM? (m := Id) p e
 
 end FindImpl
 
-@[implemented_by FindImpl.findUnsafe?]
-def find? (p : Expr → Bool) (e : Expr) : Option Expr :=
-  /- This is a reference implementation for the unsafe one above -/
-  if p e then
-    some e
+@[implemented_by FindImpl.findUnsafeM?]
+/- This is a reference implementation for the unsafe one above -/
+def findM? [Monad m] (p : Expr → m Bool) (e : Expr) : m (Option Expr) := do
+  if ← p e then
+    return some e
   else match e with
-    | .forallE _ d b _ => find? p d <|> find? p b
-    | .lam _ d b _     => find? p d <|> find? p b
-    | .mdata _ b       => find? p b
-    | .letE _ t v b _  => find? p t <|> find? p v <|> find? p b
-    | .app f a         => find? p f <|> find? p a
-    | .proj _ _ b      => find? p b
-    | _                => none
+    | .forallE _ d b _ => findM? p d <||> findM? p b
+    | .lam _ d b _     => findM? p d <||> findM? p b
+    | .mdata _ b       => findM? p b
+    | .letE _ t v b _  => findM? p t <||> findM? p v <||> findM? p b
+    | .app f a         => findM? p f <||> findM? p a
+    | .proj _ _ b      => findM? p b
+    | _                => pure none
+
+@[implemented_by FindImpl.findUnsafe?]
+def find? (p : Expr → Bool) (e : Expr) : Option Expr := findM? (m := Id) p e
 
 /-- Return true if `e` occurs in `t` -/
 def occurs (e : Expr) (t : Expr) : Bool :=
   (t.find? fun s => s == e).isSome
 
+
 /--
   Return type for `findExt?` function argument.
 -/
@@ -66,7 +72,7 @@ inductive FindStep where
 
 namespace FindExtImpl
 
-unsafe def findM? (p : Expr → FindStep) (e : Expr) : OptionT FindImpl.FindM Expr :=
+unsafe def findM? (p : Expr → FindStep) (e : Expr) : OptionT (FindImpl.FindM Id) Expr :=
   visit e
 where
   visitApp (e : Expr) :=

src/Lean/Widget/UserWidget.lean

@@ -346,13 +346,12 @@ structure UserWidgetDefinition where
 instance : ToModule UserWidgetDefinition where
   toModule uwd := { uwd with }
 
-@[deprecated (since := "2023-12-21")] private def widgetAttrImpl : AttributeImpl where
+private def widgetAttrImpl : AttributeImpl where
   name := `widget
   descr := "The `@[widget]` attribute has been deprecated, use `@[widget_module]` instead."
   applicationTime := AttributeApplicationTime.afterCompilation
   add := widgetModuleAttrImpl.add
 
-set_option linter.deprecated false in
 builtin_initialize registerBuiltinAttribute widgetAttrImpl
 
 private unsafe def evalUserWidgetDefinitionUnsafe [Monad m] [MonadEnv m] [MonadOptions m] [MonadError m]
@@ -365,7 +364,7 @@ opaque evalUserWidgetDefinition [Monad m] [MonadEnv m] [MonadOptions m] [MonadEr
 
 /-- Save a user-widget instance to the infotree.
     The given `widgetId` should be the declaration name of the widget definition. -/
-@[deprecated savePanelWidgetInfo (since := "2023-12-21")] def saveWidgetInfo (widgetId : Name) (props : Json)
+@[deprecated savePanelWidgetInfo] def saveWidgetInfo (widgetId : Name) (props : Json)
     (stx : Syntax) : CoreM Unit := do
   let uwd ← evalUserWidgetDefinition widgetId
   savePanelWidgetInfo (ToModule.toModule uwd).javascriptHash (pure props) stx
@@ -440,6 +439,6 @@ def getWidgets (pos : Lean.Lsp.Position) : RequestM (RequestTask (GetWidgetsResp
 builtin_initialize
   Server.registerBuiltinRpcProcedure ``getWidgets _ _ getWidgets
 
-attribute [deprecated Module (since := "2023-12-21")] UserWidgetDefinition
+attribute [deprecated Module] UserWidgetDefinition
 
 end Lean.Widget

src/include/lean/lean.h

@@ -1110,8 +1110,8 @@ static inline lean_obj_res lean_task_get_own(lean_obj_arg t) {
 LEAN_EXPORT bool lean_io_check_canceled_core(void);
 /* primitive for implementing `IO.cancel : Task a -> IO Unit` */
 LEAN_EXPORT void lean_io_cancel_core(b_lean_obj_arg t);
-/* primitive for implementing `IO.getTaskState : Task a -> IO TaskState` */
-LEAN_EXPORT uint8_t lean_io_get_task_state_core(b_lean_obj_arg t);
+/* primitive for implementing `IO.hasFinished : Task a -> IO Unit` */
+LEAN_EXPORT bool lean_io_has_finished_core(b_lean_obj_arg t);
 /* primitive for implementing `IO.waitAny : List (Task a) -> IO (Task a)` */
 LEAN_EXPORT b_lean_obj_res lean_io_wait_any_core(b_lean_obj_arg task_list);
 

src/kernel/environment.cpp

@@ -292,8 +292,7 @@ environment environment::add(declaration const & d, bool check) const {
     lean_unreachable();
 }
 
-extern "C" LEAN_EXPORT object * lean_add_decl(object * env, size_t max_heartbeat, object * decl) {
-    scope_max_heartbeat s(max_heartbeat);
+extern "C" LEAN_EXPORT object * lean_add_decl(object * env, object * decl) {
     return catch_kernel_exceptions<environment>([&]() {
             return environment(env).add(declaration(decl, true));
         });

src/lake/Lake/Build/Actions.lean

@@ -40,7 +40,8 @@ def compileLeanModule
   for dynlib in dynlibs do
     args := args.push s!"--load-dynlib={dynlib}"
   args := args.push "--json"
-  withLogErrorPos do
+  show LogIO _ from do
+  let iniSz ← getLogSize
   let out ← rawProc {
     args
     cmd := lean.toString
@@ -65,7 +66,8 @@ def compileLeanModule
   unless out.stderr.isEmpty do
     logInfo s!"stderr:\n{out.stderr}"
   if out.exitCode ≠ 0 then
-    error s!"Lean exited with code {out.exitCode}"
+    logError s!"Lean exited with code {out.exitCode}"
+    throw iniSz
 
 def compileO
   (oFile srcFile : FilePath)

src/lake/Lake/Build/Basic.lean

@@ -33,7 +33,7 @@ structure BuildConfig where
   /-- Report build output on `stdout`. Otherwise, Lake uses `stderr`. -/
   useStdout : Bool := false
 
-abbrev JobResult α := ELogResult α
+abbrev JobResult α := EResult Nat Log α
 abbrev JobTask α := BaseIOTask (JobResult α)
 
 /-- A Lake job. -/
@@ -51,14 +51,11 @@ abbrev BuildT := ReaderT BuildContext
 instance [Pure m] : MonadLift LakeM (BuildT m) where
   monadLift x := fun ctx => pure <| x.run ctx.toContext
 
-@[inline] def getBuildContext [Monad m] : BuildT m BuildContext :=
-  readThe BuildContext
-
 @[inline] def getLeanTrace [Monad m] : BuildT m BuildTrace :=
-  (·.leanTrace) <$> getBuildContext
+  (·.leanTrace) <$> readThe BuildContext
 
 @[inline] def getBuildConfig [Monad m] : BuildT m BuildConfig :=
-  (·.toBuildConfig) <$> getBuildContext
+  (·.toBuildConfig) <$> readThe BuildContext
 
 @[inline] def getIsOldMode [Monad m] : BuildT m Bool :=
   (·.oldMode) <$> getBuildConfig

src/lake/Lake/Build/Common.lean

@@ -97,12 +97,12 @@ def replayBuildLog (logFile : FilePath) : LogIO PUnit := do
 
 /-- Saves the log produce by `build` as JSON to `logFile`. -/
 def cacheBuildLog (logFile : FilePath) (build : JobM PUnit) : JobM PUnit := do
-  let iniPos ← getLogPos
-  let errPos? ← try build; pure none catch errPos => pure (some errPos)
-  let log := (← getLog).takeFrom iniPos
+  let iniSz ← getLogSize
+  build
+  let log ← getLog
+  let log := log.entries.extract iniSz log.entries.size
   unless log.isEmpty do
     IO.FS.writeFile logFile (toJson log).pretty
-  if let some errPos := errPos? then throw errPos
 
 /--
 Builds `file` using `build` unless it already exists and `depTrace` matches
@@ -115,8 +115,8 @@ For example, given `file := "foo.c"`, compares `depTrace` with that in
 `foo.c.trace` with the hash cache in `foo.c.hash` and the log cache in
 `foo.c.log.json`.
 -/
-def buildFileUnlessUpToDate
-  (file : FilePath) (depTrace : BuildTrace) (build : JobM PUnit)
+def buildFileUnlessUpToDate (
+  file : FilePath) (depTrace : BuildTrace) (build : JobM PUnit)
 : JobM BuildTrace := do
   let traceFile := FilePath.mk <| file.toString ++ ".trace"
   let logFile := FilePath.mk <| file.toString ++ ".log.json"

src/lake/Lake/Build/Fetch.lean

@@ -20,23 +20,13 @@ using the `fetch` function defined in this module.
 namespace Lake
 
 /-- A recursive build of a Lake build store that may encounter a cycle. -/
-abbrev RecBuildM :=
-  CallStackT BuildKey <| BuildT <| ELogT <| StateT BuildStore <| BaseIO
-
-instance : MonadLift IO RecBuildM := ⟨MonadError.runIO⟩
-
-@[inline] def RecBuildM.runLogIO (x : LogIO α) : RecBuildM α :=
-  fun _ _ log store => (·, store) <$> x log
-
-instance : MonadLift LogIO RecBuildM := ⟨RecBuildM.runLogIO⟩
+abbrev RecBuildM := CallStackT BuildKey <| StateT BuildStore <| CoreBuildM
 
 /-- Run a recursive build. -/
 @[inline] def RecBuildM.run
   (stack : CallStack BuildKey) (store : BuildStore) (build : RecBuildM α)
-: CoreBuildM (α × BuildStore) := fun ctx log => do
-  match (← build stack ctx log store) with
-  | (.ok a log, store) => return .ok (a, store) log
-  | (.error e log, _) => return .error e log
+: CoreBuildM (α × BuildStore) := do
+  build stack store
 
 /-- Run a recursive build in a fresh build store. -/
 @[inline] def RecBuildM.run' (build : RecBuildM α) : CoreBuildM α := do
@@ -71,20 +61,3 @@ abbrev FetchM := IndexT RecBuildM
   fun build => cast (by simp) <| build self
 
 export BuildInfo (fetch)
-
-/-- Register the produced job for the CLI progress UI.  -/
-def withRegisterJob
-  (caption : String) (x : FetchM (Job α))
-: FetchM (Job α) := fun fetch stack ctx log store => do
-  let iniPos := log.endPos
-  match (← (withLoggedIO x) fetch stack ctx log store) with
-  | (.ok job log, store) =>
-    let (log, jobLog) := log.split iniPos
-    let regJob := job.mapResult (discard <| ·.modifyState (jobLog ++  ·))
-    ctx.registeredJobs.modify (·.push (caption, regJob))
-    return (.ok job.clearLog log, store)
-  | (.error _ log, store) =>
-    let (log, jobLog) := log.split iniPos
-    let regJob := ⟨Task.pure <| .error 0 jobLog⟩
-    ctx.registeredJobs.modify (·.push (caption, regJob))
-    return (.ok .error log, store)

src/lake/Lake/Build/Imports.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lake.Build.Module
+import Lake.Build.Index
 
 /-!
 Definitions to support `lake setup-file` builds.
@@ -13,25 +13,41 @@ open System
 namespace Lake
 
 /--
-Builds an `Array` of module imports for a Lean file.
-Used by `lake setup-file` to build modules for the Lean server and
-by `lake lean` to build the imports of a file.
+Recursively build a set of imported modules and return their build jobs,
+the build jobs of their precompiled modules and the build jobs of said modules'
+external libraries.
+-/
+def recBuildImports (imports : Array Module)
+: FetchM (Array (BuildJob Unit) × Array (BuildJob Dynlib) × Array (BuildJob Dynlib)) := do
+  let mut modJobs := #[]
+  let mut precompileImports := OrdModuleSet.empty
+  for mod in imports do
+    if mod.shouldPrecompile then
+      precompileImports := precompileImports.appendArray (← mod.transImports.fetch) |>.insert mod
+    else
+      precompileImports := precompileImports.appendArray (← mod.precompileImports.fetch)
+    modJobs := modJobs.push <| ← mod.leanArts.fetch
+  let pkgs := precompileImports.foldl (·.insert ·.pkg) OrdPackageSet.empty |>.toArray
+  let externJobs ← pkgs.concatMapM (·.externLibs.mapM (·.dynlib.fetch))
+  let precompileJobs ← precompileImports.toArray.mapM (·.dynlib.fetch)
+  return (modJobs, precompileJobs, externJobs)
+
+/--
+Builds an `Array` of module imports. Used by `lake setup-file` to build modules
+for the Lean server and by `lake lean` to build the imports of a file.
 Returns the set of module dynlibs built (so they can be loaded by Lean).
 -/
-def buildImportsAndDeps (leanFile : FilePath) (imports : Array Module) : FetchM (BuildJob (Array FilePath)) := do
-  withRegisterJob s!"Building imports of '{leanFile}'" do
+def buildImportsAndDeps (imports : Array Module) : FetchM (BuildJob (Array FilePath)) := do
   if imports.isEmpty then
     -- build the package's (and its dependencies') `extraDepTarget`
     (← getRootPackage).extraDep.fetch <&> (·.map fun _ => #[])
   else
     -- build local imports from list
-    let modJob ← BuildJob.mixArray <| ← imports.mapM (·.olean.fetch)
-    let precompileImports ← computePrecompileImportsAux leanFile imports
-    let pkgs := precompileImports.foldl (·.insert ·.pkg) OrdPackageSet.empty |>.toArray
-    let externLibJob ← BuildJob.collectArray <| ←
-      pkgs.concatMapM (·.externLibs.mapM (·.dynlib.fetch))
-    let precompileJob ← BuildJob.collectArray <| ←
-      precompileImports.mapM (·.dynlib.fetch)
+    let (modJobs, precompileJobs, externLibJobs) ←
+      recBuildImports imports
+    let modJob ← BuildJob.mixArray modJobs
+    let precompileJob ← BuildJob.collectArray precompileJobs
+    let externLibJob ← BuildJob.collectArray externLibJobs
     let job ←
       modJob.bindAsync fun _ modTrace =>
       precompileJob.bindAsync fun modLibs modLibTrace =>

src/lake/Lake/Build/Job.lean

@@ -21,7 +21,7 @@ instance [Inhabited α] : Inhabited (Job α) := ⟨pure default⟩
 @[inline] protected def nop : Job Unit :=
   pure ()
 
-@[inline] protected def error (l : Log := {}) : Job α :=
+@[inline] protected def error (l : Log) : Job α :=
   {task := Task.pure (.error 0 l)}
 
 @[inline] def mapResult
@@ -45,19 +45,19 @@ instance : Functor Job where map := Job.map
 
 @[inline] def attempt (self : Job α) : Job Bool :=
   self.mapResult (sync := true) fun
-  | .error n l => .ok false (l.dropFrom n)
+  | .error n l => .ok false (l.shrink n)
   | .ok _ l => .ok true l
 
 @[inline] def attempt? (self : Job α) : Job (Option α) :=
   self.mapResult (sync := true) fun
-  | .error n l => .ok none (l.dropFrom n)
+  | .error n l => .ok none (l.shrink n)
   | .ok a l => .ok (some a) l
 
 /-- Spawn a job that asynchronously performs `act`. -/
 @[inline] protected def async
   (act : JobM α) (prio := Task.Priority.default)
 : SpawnM (Job α) := fun ctx => Job.mk <$> do
-  BaseIO.asTask (prio := prio) do (withLoggedIO act) ctx {}
+  BaseIO.asTask (act ctx {}) prio
 
 /-- Wait a the job to complete and return the result. -/
 @[inline] protected def wait (self : Job α) : BaseIO (JobResult α) := do
@@ -87,8 +87,9 @@ after the job `a` completes.
   (self : Job α) (f : α → JobM β)
   (prio := Task.Priority.default) (sync := false)
 : SpawnM (Job β) := fun ctx => Job.mk <$> do
-  BaseIO.mapTask (t := self.task) (prio := prio) (sync := sync) fun
-    | EResult.ok a l => (withLoggedIO (f a)) ctx l
+  BaseIO.mapTask (t := self.task) (prio := prio) (sync := sync) fun r=>
+    match r with
+    | EResult.ok a l => f a ctx l
     | EResult.error n l => return .error n l
 
 /--
@@ -105,7 +106,7 @@ after the job `a` completes and then merges into the job produced by `b`.
       if l.isEmpty then return job.task else
       return job.task.map (prio := prio) (sync := true) fun
       | EResult.ok a l' => .ok a (l ++ l')
-      | EResult.error n l' => .error ⟨l.size + n.val⟩ (l ++ l')
+      | EResult.error n l' => .error (l.size + n) (l ++ l')
     | .error n l => return Task.pure (.error n l)
 
 /--
@@ -117,13 +118,24 @@ results of `a` and `b`. The job `c` errors if either `a` or `b` error.
   (prio := Task.Priority.default) (sync := false)
 : BaseIO (Job γ) := Job.mk <$> do
   BaseIO.bindTask x.task (prio := prio) (sync := true) fun rx =>
-  BaseIO.mapTask (t := y.task) (prio := prio) (sync := sync) fun ry =>
+  BaseIO.bindTask y.task (prio := prio) (sync := sync) fun ry =>
   match rx, ry with
-  | .ok a la, .ok b lb => return .ok (f a b) (la ++ lb)
-  | rx, ry => return .error 0 (rx.state ++ ry.state)
+  | .ok a la, .ok b lb => return Task.pure (EResult.ok (f a b) (la ++ lb))
+  | rx, ry => return Task.pure (EResult.error 0 (rx.state ++ ry.state))
 
 end Job
 
+/-- Register the produced job for the CLI progress UI.  -/
+@[inline] def withRegisterJob
+  [Monad m] [MonadReaderOf BuildContext m] [MonadLiftT BaseIO m]
+  (caption : String) (x : m (Job α))
+: m (Job α) := do
+  let job ← x
+  let ctx ← read
+  liftM (m := BaseIO) do
+  ctx.registeredJobs.modify (·.push (caption, discard job))
+  return job.clearLog
+
 /-- A Lake build job. -/
 abbrev BuildJob α := Job (α × BuildTrace)
 

src/lake/Lake/Build/Module.lean

@@ -26,12 +26,48 @@ def recBuildExternDynlibs (pkgs : Array Package)
     jobs := jobs.append <| ← pkg.externLibs.mapM (·.dynlib.fetch)
   return (jobs, libDirs)
 
+/--
+Build the dynlibs of the transitive imports that want precompilation
+and the dynlibs of *their* imports.
+-/
+partial def recBuildPrecompileDynlibs (imports : Array Module)
+: FetchM (Array (BuildJob Dynlib) × Array (BuildJob Dynlib) × Array FilePath) := do
+  let (pkgs, _, jobs) ←
+    go imports OrdPackageSet.empty ModuleSet.empty #[] false
+  return (jobs, ← recBuildExternDynlibs pkgs.toArray)
+where
+  go imports pkgs modSet jobs shouldPrecompile := do
+    let mut pkgs := pkgs
+    let mut modSet := modSet
+    let mut jobs := jobs
+    for mod in imports do
+      if modSet.contains mod then
+        continue
+      modSet := modSet.insert mod
+      let shouldPrecompile := shouldPrecompile || mod.shouldPrecompile
+      if shouldPrecompile then
+        pkgs := pkgs.insert mod.pkg
+        jobs := jobs.push <| (←  mod.dynlib.fetch)
+      let recImports ← mod.imports.fetch
+      (pkgs, modSet, jobs) ← go recImports pkgs modSet jobs shouldPrecompile
+    return (pkgs, modSet, jobs)
+
 /--
 Recursively parse the Lean files of a module and its imports
 building an `Array` product of its direct local imports.
 -/
 def Module.recParseImports (mod : Module) : FetchM (Array Module) := do
-  let contents ← IO.FS.readFile mod.leanFile
+  let callstack ← getCallStack
+  let contents ← liftM <| tryCatch (IO.FS.readFile mod.leanFile) fun err =>
+    -- filter out only modules from build key, and remove adjacent duplicates (squeeze),
+    -- since Lake visits multiple nested facets of the same module.
+    let callstack := callstack.filterMap (fun bk =>
+      match bk with
+      | .moduleFacet mod .. => .some s!"'{mod.toString}'"
+      | _ => .none
+    ) |> List.squeeze
+    let breadcrumb := String.intercalate " ▸ " callstack.reverse
+    error s!"{breadcrumb}: {err}"
   let imports ← Lean.parseImports' contents mod.leanFile.toString
   let mods ← imports.foldlM (init := OrdModuleSet.empty) fun set imp =>
     findModule? imp.module <&> fun | some mod => set.insert mod | none => set
@@ -41,48 +77,22 @@ def Module.recParseImports (mod : Module) : FetchM (Array Module) := do
 def Module.importsFacetConfig : ModuleFacetConfig importsFacet :=
   mkFacetConfig (·.recParseImports)
 
-@[inline] def collectImportsAux
-  (leanFile : FilePath) (imports : Array Module)
-  (f : Module → FetchM (Bool × Array Module))
-: FetchM (Array Module) := do
-  withLogErrorPos do
-  let mut didError := false
-  let mut importSet := OrdModuleSet.empty
-  for imp in imports do
-    try
-      let (includeSelf, transImps) ← f imp
-      importSet := importSet.appendArray transImps
-      if includeSelf then importSet := importSet.insert imp
-    catch errPos =>
-      dropLogFrom errPos
-      logError s!"{leanFile}: bad import '{imp.name}'"
-      didError := true
-  if didError then
-    failure
-  else
-    return importSet.toArray
-
 /-- Recursively compute a module's transitive imports. -/
 def Module.recComputeTransImports (mod : Module) : FetchM (Array Module) := do
-  collectImportsAux mod.leanFile (← mod.imports.fetch) fun imp =>
-    (true, ·) <$> imp.transImports.fetch
+  (·.toArray) <$> (← mod.imports.fetch).foldlM (init := OrdModuleSet.empty) fun set imp => do
+    return set.appendArray (← imp.transImports.fetch) |>.insert imp
 
 /-- The `ModuleFacetConfig` for the builtin `transImportsFacet`. -/
 def Module.transImportsFacetConfig : ModuleFacetConfig transImportsFacet :=
   mkFacetConfig (·.recComputeTransImports)
 
-@[inline] def computePrecompileImportsAux
-  (leanFile : FilePath) (imports : Array Module)
-: FetchM (Array Module) := do
-  collectImportsAux leanFile imports fun imp =>
-    if imp.shouldPrecompile then
-      (true, ·) <$> imp.transImports.fetch
-    else
-      (false, ·) <$> imp.precompileImports.fetch
-
 /-- Recursively compute a module's precompiled imports. -/
 def Module.recComputePrecompileImports (mod : Module) : FetchM (Array Module) := do
-  computePrecompileImportsAux mod.leanFile (← mod.imports.fetch)
+  (·.toArray) <$> (← mod.imports.fetch).foldlM (init := OrdModuleSet.empty) fun set imp => do
+    if imp.shouldPrecompile then
+      return set.appendArray (← imp.transImports.fetch) |>.insert imp
+    else
+      return set.appendArray (← imp.precompileImports.fetch)
 
 /-- The `ModuleFacetConfig` for the builtin `precompileImportsFacet`. -/
 def Module.precompileImportsFacetConfig : ModuleFacetConfig precompileImportsFacet :=
@@ -95,25 +105,14 @@ Recursively build a module's dependencies, including:
 * `extraDepTargets` of its library
 -/
 def Module.recBuildDeps (mod : Module) : FetchM (BuildJob (SearchPath × Array FilePath)) := do
+  let imports ← mod.imports.fetch
   let extraDepJob ← mod.lib.extraDep.fetch
-
-  /-
-  Remark: We must build direct imports before we fetch the transitive
-  precompiled imports so that errors in the import block of transitive imports
-  will not kill this job before the direct imports are built.
-  -/
-  let directImports ← try mod.imports.fetch
-    catch errPos => return Job.error (← takeLogFrom errPos)
-  let importJob ← BuildJob.mixArray <| ← directImports.mapM fun imp => do
-    if imp.name = mod.name then
-      logError s!"{mod.leanFile}: module imports itself"
-    imp.olean.fetch
-  let precompileImports ← try mod.precompileImports.fetch
-    catch errPos => return Job.error (← takeLogFrom errPos)
+  let precompileImports ← mod.precompileImports.fetch
   let modJobs ← precompileImports.mapM (·.dynlib.fetch)
   let pkgs := precompileImports.foldl (·.insert ·.pkg)
     OrdPackageSet.empty |>.insert mod.pkg |>.toArray
   let (externJobs, libDirs) ← recBuildExternDynlibs pkgs
+  let importJob ← BuildJob.mixArray <| ← imports.mapM (·.olean.fetch)
   let externDynlibsJob ← BuildJob.collectArray externJobs
   let modDynlibsJob ← BuildJob.collectArray modJobs
 

src/lake/Lake/Build/Package.lean

@@ -49,7 +49,7 @@ def Package.extraDepFacetConfig : PackageFacetConfig extraDepFacet :=
   mkFacetJobConfig Package.recBuildExtraDepTargets
 
 /-- Download and unpack the package's prebuilt release archive (from GitHub). -/
-def Package.fetchRelease (self : Package) : FetchM (BuildJob Unit) :=
+def Package.fetchRelease (self : Package) : SpawnM (BuildJob Unit) :=
   withRegisterJob s!"Fetching {self.name} cloud release" <| Job.async do
   let repo := GitRepo.mk self.dir
   let repoUrl? := self.releaseRepo? <|> self.remoteUrl?