chore: fix explicitness of List.bind_map

.github/workflows/ci.yml

@@ -467,7 +467,6 @@ jobs:
         with:
           files: artifacts/*/*
           fail_on_unmatched_files: true
-          prerelease: ${{ !startsWith(github.ref, 'refs/tags/v') || contains(github.ref, '-rc') }}
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
 

nix/bootstrap.nix

@@ -152,9 +152,11 @@ rec {
         '';
         meta.mainProgram = "lean";
       };
-      cacheRoots = linkFarmFromDrvs "cacheRoots" ([
+      cacheRoots = linkFarmFromDrvs "cacheRoots" [
         stage0 lean leanc lean-all iTree modDepsFiles depRoots Leanc.src
-      ] ++ map (lib: lib.oTree) stdlib);
+        # .o files are not a runtime dependency on macOS because of lack of thin archives
+        Init.oTree Std.oTree Lean.oTree Lake.oTree
+      ];
       test = buildCMake {
         name = "lean-test-${desc}";
         realSrc = lib.sourceByRegex src [ "src.*" "tests.*" ];
@@ -177,7 +179,7 @@ rec {
         '';
       };
       update-stage0 =
-        let cTree = symlinkJoin { name = "cs"; paths = map (lib: lib.cTree) stdlib; }; in
+        let cTree = symlinkJoin { name = "cs"; paths = [ Init.cTree Lean.cTree Lake.cTree ]; }; in
         writeShellScriptBin "update-stage0" ''
           CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/lib/update-stage0"}
         '';

src/Init/Core.lean

@@ -1191,10 +1191,7 @@ def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂
     (f : α₁ → α₂) (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂
   | (a, b) => (f a, g b)
 
-@[simp] theorem Prod.map_apply (f : α → β) (g : γ → δ) (x) (y) :
-    Prod.map f g (x, y) = (f x, g y) := rfl
-@[simp] theorem Prod.map_fst (f : α → β) (g : γ → δ) (x) : (Prod.map f g x).1 = f x.1 := rfl
-@[simp] theorem Prod.map_snd (f : α → β) (g : γ → δ) (x) : (Prod.map f g x).2 = g x.2 := rfl
+@[simp] theorem Prod.map_apply : Prod.map f g (x, y) = (f x, g y) := rfl
 
 /-! # Dependent products -/
 

src/Init/Data/Array/Basic.lean

@@ -60,6 +60,8 @@ def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
 instance : GetElem (Array α) USize α fun xs i => i.toNat < xs.size where
   getElem xs i h := xs.uget i h
 
+instance : LawfulGetElem (Array α) USize α fun xs i => i.toNat < xs.size where
+
 def back [Inhabited α] (a : Array α) : α :=
   a.get! (a.size - 1)
 

src/Init/Data/Array/Lemmas.lean

@@ -220,7 +220,7 @@ theorem getElem?_len_le (a : Array α) {i : Nat} (h : a.size ≤ i) : a[i]? = no
 theorem getD_get? (a : Array α) (i : Nat) (d : α) :
   Option.getD a[i]? d = if p : i < a.size then a[i]'p else d := by
   if h : i < a.size then
-    simp [setD, h, getElem?_def]
+    simp [setD, h, getElem?]
   else
     have p : i ≥ a.size := Nat.le_of_not_gt h
     simp [setD, getElem?_len_le _ p, h]
@@ -383,18 +383,18 @@ theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x el
   | Or.inl g =>
     have h1 : i < a.size + 1 := by omega
     have h2 : i ≠ a.size := by omega
-    simp [getElem?_def, size_push, g, h1, h2, get_push_lt]
+    simp [getElem?, size_push, g, h1, h2, get_push_lt]
   | Or.inr (Or.inl heq) =>
     simp [heq, getElem?_pos, get_push_eq]
   | Or.inr (Or.inr g) =>
-    simp only [getElem?_def, size_push]
+    simp only [getElem?, size_push]
     have h1 : ¬ (i < a.size) := by omega
     have h2 : ¬ (i < a.size + 1) := by omega
     have h3 : i ≠ a.size := by omega
     simp [h1, h2, h3]
 
 @[simp] theorem get?_size {a : Array α} : a[a.size]? = none := by
-  simp only [getElem?_def, Nat.lt_irrefl, dite_false]
+  simp only [getElem?, Nat.lt_irrefl, dite_false]
 
 @[simp] theorem data_set (a : Array α) (i v) : (a.set i v).data = a.data.set i.1 v := rfl
 

src/Init/Data/Array/Subarray.lean

@@ -47,6 +47,8 @@ def get (s : Subarray α) (i : Fin s.size) : α :=
 instance : GetElem (Subarray α) Nat α fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
+instance : LawfulGetElem (Subarray α) Nat α fun xs i => i < xs.size where
+
 @[inline] def getD (s : Subarray α) (i : Nat) (v₀ : α) : α :=
   if h : i < s.size then s.get ⟨i, h⟩ else v₀
 

src/Init/Data/BitVec/Basic.lean

@@ -614,13 +614,6 @@ theorem ofBool_append (msb : Bool) (lsbs : BitVec w) :
     ofBool msb ++ lsbs = (cons msb lsbs).cast (Nat.add_comm ..) :=
   rfl
 
-/--
-`twoPow w i` is the bitvector `2^i` if `i < w`, and `0` otherwise.
-That is, 2 to the power `i`.
-For the bitwise point of view, it has the `i`th bit as `1` and all other bits as `0`.
--/
-def twoPow (w : Nat) (i : Nat) : BitVec w := 1#w <<< i
-
 end bitwise
 
 section normalization_eqs

src/Init/Data/BitVec/Lemmas.lean

@@ -1367,51 +1367,4 @@ theorem getLsb_rotateRight {x : BitVec w} {r i : Nat} :
   · simp
   · rw [← rotateRight_mod_eq_rotateRight, getLsb_rotateRight_of_le (Nat.mod_lt _ (by omega))]
 
-/- ## twoPow -/
-
-@[simp, bv_toNat]
-theorem toNat_twoPow (w : Nat) (i : Nat) : (twoPow w i).toNat = 2^i % 2^w := by
-  rcases w with rfl | w
-  · simp [Nat.mod_one]
-  · simp only [twoPow, toNat_shiftLeft, toNat_ofNat]
-    have h1 : 1 < 2 ^ (w + 1) := Nat.one_lt_two_pow (by omega)
-    rw [Nat.mod_eq_of_lt h1, Nat.shiftLeft_eq, Nat.one_mul]
-
-@[simp]
-theorem getLsb_twoPow (i j : Nat) : (twoPow w i).getLsb j = ((i < w) && (i = j)) := by
-  rcases w with rfl | w
-  · simp; omega
-  · simp only [twoPow, getLsb_shiftLeft, getLsb_ofNat]
-    by_cases hj : j < i
-    · simp only [hj, decide_True, Bool.not_true, Bool.and_false, Bool.false_and, Bool.false_eq,
-      Bool.and_eq_false_imp, decide_eq_true_eq, decide_eq_false_iff_not]
-      omega
-    · by_cases hi : Nat.testBit 1 (j - i)
-      · obtain hi' := Nat.testBit_one_eq_true_iff_self_eq_zero.mp hi
-        have hij : j = i := by omega
-        simp_all
-      · have hij : i ≠ j := by
-          intro h; subst h
-          simp at hi
-        simp_all
-
-theorem and_twoPow_eq (x : BitVec w) (i : Nat) :
-    x &&& (twoPow w i) = if x.getLsb i then twoPow w i else 0#w := by
-  ext j
-  simp only [getLsb_and, getLsb_twoPow]
-  by_cases hj : i = j <;> by_cases hx : x.getLsb i <;> simp_all
-
-@[simp]
-theorem mul_twoPow_eq_shiftLeft (x : BitVec w) (i : Nat) :
-    x * (twoPow w i) = x <<< i := by
-  apply eq_of_toNat_eq
-  simp only [toNat_mul, toNat_twoPow, toNat_shiftLeft, Nat.shiftLeft_eq]
-  by_cases hi : i < w
-  · have hpow : 2^i < 2^w := Nat.pow_lt_pow_of_lt (by omega) (by omega)
-    rw [Nat.mod_eq_of_lt hpow]
-  · have hpow : 2 ^ i % 2 ^ w = 0 := by
-      rw [Nat.mod_eq_zero_of_dvd]
-      apply Nat.pow_dvd_pow 2 (by omega)
-    simp [Nat.mul_mod, hpow]
-
 end BitVec

src/Init/Data/ByteArray/Basic.lean

@@ -52,9 +52,13 @@ def get : (a : @& ByteArray) → (@& Fin a.size) → UInt8
 instance : GetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
+instance : LawfulGetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
+
 instance : GetElem ByteArray USize UInt8 fun xs i => i.val < xs.size where
   getElem xs i h := xs.uget i h
 
+instance : LawfulGetElem ByteArray USize UInt8 fun xs i => i.val < xs.size where
+
 @[extern "lean_byte_array_set"]
 def set! : ByteArray → (@& Nat) → UInt8 → ByteArray
   | ⟨bs⟩, i, b => ⟨bs.set! i b⟩

src/Init/Data/FloatArray/Basic.lean

@@ -58,9 +58,13 @@ def get? (ds : FloatArray) (i : Nat) : Option Float :=
 instance : GetElem FloatArray Nat Float fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
+instance : LawfulGetElem FloatArray Nat Float fun xs i => i < xs.size where
+
 instance : GetElem FloatArray USize Float fun xs i => i.val < xs.size where
   getElem xs i h := xs.uget i h
 
+instance : LawfulGetElem FloatArray USize Float fun xs i => i.val < xs.size where
+
 @[extern "lean_float_array_uset"]
 def uset : (a : FloatArray) → (i : USize) → Float → i.toNat < a.size → FloatArray
   | ⟨ds⟩, i, v, h => ⟨ds.uset i v h⟩

src/Init/Data/List/Basic.lean

@@ -67,9 +67,6 @@ namespace List
 
 @[simp 1100] theorem length_singleton (a : α) : length [a] = 1 := rfl
 
-@[simp] theorem length_cons {α} (a : α) (as : List α) : (cons a as).length = as.length + 1 :=
-  rfl
-
 /-! ### set -/
 
 @[simp] theorem length_set (as : List α) (i : Nat) (a : α) : (as.set i a).length = as.length := by

src/Init/Data/List/Lemmas.lean

@@ -154,7 +154,7 @@ theorem get?_eq_none : l.get? n = none ↔ length l ≤ n :=
   ⟨fun e => Nat.ge_of_not_lt (fun h' => by cases e ▸ get?_eq_some.2 ⟨h', rfl⟩), get?_len_le⟩
 
 @[simp] theorem get?_eq_getElem? (l : List α) (i : Nat) : l.get? i = l[i]? := by
-  simp only [getElem?, decidableGetElem?]; split
+  simp only [getElem?]; split
   · exact (get?_eq_get ‹_›)
   · exact (get?_eq_none.2 <| Nat.not_lt.1 ‹_›)
 
@@ -923,12 +923,12 @@ theorem map_filter_eq_foldr (f : α → β) (p : α → Bool) (as : List α) :
   | a :: l₁, l₂ => by simp [filter]; split <;> simp [filter_append l₁]
 
 theorem filter_congr {p q : α → Bool} :
-    ∀ {l : List α}, (∀ x ∈ l, p x = q x) → filter p l = filter q l
+    ∀ {l : List α}, (∀ x ∈ l, p x ↔ q x) → filter p l = filter q l
   | [], _ => rfl
   | a :: l, h => by
     rw [forall_mem_cons] at h; by_cases pa : p a
-    · simp [pa, h.1 ▸ pa, filter_congr h.2]
-    · simp [pa, h.1 ▸ pa, filter_congr h.2]
+    · simp [pa, h.1.1 pa, filter_congr h.2]
+    · simp [pa, mt h.1.2 pa, filter_congr h.2]
 
 @[deprecated filter_congr (since := "2024-06-20")] abbrev filter_congr' := @filter_congr
 

src/Init/Data/List/TakeDrop.lean

@@ -364,24 +364,4 @@ theorem zip_eq_zip_take_min : ∀ (l₁ : List α) (l₂ : List β),
   rw [zip_eq_zip_take_min]
   simp
 
-/-! ### minimum? -/
-
--- A specialization of `minimum?_eq_some_iff` to Nat.
-theorem minimum?_eq_some_iff' {xs : List Nat} :
-    xs.minimum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) :=
-  minimum?_eq_some_iff
-    (le_refl := Nat.le_refl)
-    (min_eq_or := fun _ _ => by omega)
-    (le_min_iff := fun _ _ _ => by omega)
-
-/-! ### maximum? -/
-
--- A specialization of `maximum?_eq_some_iff` to Nat.
-theorem maximum?_eq_some_iff' {xs : List Nat} :
-    xs.maximum? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, b ≤ a) :=
-  maximum?_eq_some_iff
-    (le_refl := Nat.le_refl)
-    (max_eq_or := fun _ _ => by omega)
-    (max_le_iff := fun _ _ _ => by omega)
-
 end List

src/Init/Data/Nat/Basic.lean

@@ -278,7 +278,7 @@ theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by
   | zero      => exact rfl
   | succ m ih => apply congrArg pred ih
 
-theorem pred_le : ∀ (n : Nat), pred n ≤ n
+@[simp] theorem pred_le : ∀ (n : Nat), pred n ≤ n
   | zero   => Nat.le.refl
   | succ _ => le_succ _
 
@@ -288,7 +288,7 @@ theorem pred_lt : ∀ {n : Nat}, n ≠ 0 → pred n < n
 
 theorem sub_one_lt : ∀ {n : Nat}, n ≠ 0 → n - 1 < n := pred_lt
 
-@[simp] theorem sub_le (n m : Nat) : n - m ≤ n := by
+theorem sub_le (n m : Nat) : n - m ≤ n := by
   induction m with
   | zero      => exact Nat.le_refl (n - 0)
   | succ m ih => apply Nat.le_trans (pred_le (n - m)) ih

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

@@ -310,11 +310,6 @@ theorem testBit_bool_to_nat (b : Bool) (i : Nat) :
         ←Nat.div_div_eq_div_mul _ 2, one_div_two,
         Nat.mod_eq_of_lt]
 
-/-- `testBit 1 i` is true iff the index `i` equals 0. -/
-theorem testBit_one_eq_true_iff_self_eq_zero {i : Nat} :
-    Nat.testBit 1 i = true ↔ i = 0 := by
-  cases i <;> simp
-
 /-! ### bitwise -/
 
 theorem testBit_bitwise

src/Init/Data/Nat/Div.lean

@@ -285,7 +285,7 @@ theorem add_mul_div_right (x y : Nat) {z : Nat} (H : 0 < z) : (x + y * z) / z =
 @[simp] theorem mul_mod_left (m n : Nat) : (m * n) % n = 0 := by
   rw [Nat.mul_comm, mul_mod_right]
 
-protected theorem div_eq_of_lt_le (lo : k * n ≤ m) (hi : m < (k + 1) * n) : m / n = k :=
+protected theorem div_eq_of_lt_le (lo : k * n ≤ m) (hi : m < succ k * n) : m / n = k :=
 have npos : 0 < n := (eq_zero_or_pos _).resolve_left fun hn => by
   rw [hn, Nat.mul_zero] at hi lo; exact absurd lo (Nat.not_le_of_gt hi)
 Nat.le_antisymm
@@ -307,7 +307,7 @@ theorem sub_mul_div (x n p : Nat) (h₁ : n*p ≤ x) : (x - n*p) / n = x / n - p
       rw [sub_succ, ← IH h₂, div_eq_sub_div h₀ h₃]
       simp [Nat.pred_succ, mul_succ, Nat.sub_sub]
 
-theorem mul_sub_div (x n p : Nat) (h₁ : x < n*p) : (n * p - (x + 1)) / n = p - ((x / n) + 1) := by
+theorem mul_sub_div (x n p : Nat) (h₁ : x < n*p) : (n * p - succ x) / n = p - succ (x / n) := by
   have npos : 0 < n := (eq_zero_or_pos _).resolve_left fun n0 => by
     rw [n0, Nat.zero_mul] at h₁; exact not_lt_zero _ h₁
   apply Nat.div_eq_of_lt_le

src/Init/Data/Option/Basic.lean

@@ -119,7 +119,7 @@ def merge (fn : α → α → α) : Option α → Option α → Option α
 
 
 /-- An elimination principle for `Option`. It is a nondependent version of `Option.recOn`. -/
-@[inline] protected def elim : Option α → β → (α → β) → β
+@[simp, inline] protected def elim : Option α → β → (α → β) → β
   | some x, _, f => f x
   | none, y, _ => y
 

src/Init/Data/Option/Lemmas.lean

@@ -208,9 +208,9 @@ theorem liftOrGet_eq_or_eq {f : α → α → α} (h : ∀ a b, f a b = a ∨ f
 @[simp] theorem liftOrGet_some_some {f} {a b : α} :
   liftOrGet f (some a) (some b) = f a b := rfl
 
-@[simp] theorem elim_none (x : β) (f : α → β) : none.elim x f = x := rfl
+theorem elim_none (x : β) (f : α → β) : none.elim x f = x := rfl
 
-@[simp] theorem elim_some (x : β) (f : α → β) (a : α) : (some a).elim x f = f a := rfl
+theorem elim_some (x : β) (f : α → β) (a : α) : (some a).elim x f = f a := rfl
 
 @[simp] theorem getD_map (f : α → β) (x : α) (o : Option α) :
   (o.map f).getD (f x) = f (getD o x) := by cases o <;> rfl

src/Init/GetElem.lean

@@ -7,57 +7,22 @@ prelude
 import Init.Util
 
 @[never_extract]
-def outOfBounds [Inhabited α] : α :=
+private def outOfBounds [Inhabited α] : α :=
   panic! "index out of bounds"
 
-theorem outOfBounds_eq_default [Inhabited α] : (outOfBounds : α) = default := rfl
-
 /--
-The classes `GetElem` and `GetElem?` implement lookup notation,
-specifically `xs[i]`, `xs[i]?`, `xs[i]!`, and `xs[i]'p`.
-
-Both classes are indexed by types `coll`, `idx`, and `elem` which are
-the collection, the index, and the element types.
-A single collection may support lookups with multiple index
-types. The relation `valid` determines when the index is guaranteed to be
-valid; lookups of valid indices are guaranteed not to fail.
-
-For example, an instance for arrays looks like
-`GetElem (Array α) Nat α (fun xs i => i < xs.size)`. In other words, given an
-array `xs` and a natural number `i`, `xs[i]` will return an `α` when `valid xs i`
-holds, which is true when `i` is less than the size of the array. `Array`
-additionally supports indexing with `USize` instead of `Nat`.
-In either case, because the bounds are checked at compile time,
-no runtime check is required.
-
+The class `GetElem coll idx elem valid` implements the `xs[i]` notation.
 Given `xs[i]` with `xs : coll` and `i : idx`, Lean looks for an instance of
-`GetElem coll idx elem valid` and uses this to infer the type of the return
-value `elem` and side condition `valid` required to ensure `xs[i]` yields
-a valid value of type `elem`. The tactic `get_elem_tactic` is
-invoked to prove validity automatically. The `xs[i]'p` notation uses the
-proof `p` to satisfy the validity condition.
-If the proof `p` is long, it is often easier to place the
-proof in the context using `have`, because `get_elem_tactic` tries
-`assumption`.
+`GetElem coll idx elem valid` and uses this to infer the type of return
+value `elem` and side conditions `valid` required to ensure `xs[i]` yields
+a valid value of type `elem`.
 
+For example, the instance for arrays looks like
+`GetElem (Array α) Nat α (fun xs i => i < xs.size)`.
 
 The proof side-condition `valid xs i` is automatically dispatched by the
-`get_elem_tactic` tactic; this tactic can be extended by adding more clauses to
-`get_elem_tactic_trivial` using `macro_rules`.
-
-`xs[i]?` and `xs[i]!` do not impose a proof obligation; the former returns
-an `Option elem`, with `none` signalling that the value isn't present, and
-the latter returns `elem` but panics if the value isn't there, returning
-`default : elem` based on the `Inhabited elem` instance.
-These are provided by the `GetElem?` class, for which there is a default instance
-generated from a `GetElem` class as long as `valid xs i` is always decidable.
-
-Important instances include:
-  * `arr[i] : α` where `arr : Array α` and `i : Nat` or `i : USize`: does array
-    indexing with no runtime bounds check and a proof side goal `i < arr.size`.
-  * `l[i] : α` where `l : List α` and `i : Nat`: index into a list, with proof
-    side goal `i < l.length`.
-
+`get_elem_tactic` tactic, which can be extended by adding more clauses to
+`get_elem_tactic_trivial`.
 -/
 class GetElem (coll : Type u) (idx : Type v) (elem : outParam (Type w))
               (valid : outParam (coll → idx → Prop)) where
@@ -65,10 +30,33 @@ class GetElem (coll : Type u) (idx : Type v) (elem : outParam (Type w))
   The syntax `arr[i]` gets the `i`'th element of the collection `arr`. If there
   are proof side conditions to the application, they will be automatically
   inferred by the `get_elem_tactic` tactic.
+
+  The actual behavior of this class is type-dependent, but here are some
+  important implementations:
+  * `arr[i] : α` where `arr : Array α` and `i : Nat` or `i : USize`: does array
+    indexing with no bounds check and a proof side goal `i < arr.size`.
+  * `l[i] : α` where `l : List α` and `i : Nat`: index into a list, with proof
+    side goal `i < l.length`.
+  * `stx[i] : Syntax` where `stx : Syntax` and `i : Nat`: get a syntax argument,
+    no side goal (returns `.missing` out of range)
+
+  There are other variations on this syntax:
+  * `arr[i]!` is syntax for `getElem! arr i` which should panic and return
+    `default : α` if the index is not valid.
+  * `arr[i]?` is syntax for `getElem?` which should return `none` if the index
+    is not valid.
+  * `arr[i]'h` is syntax for `getElem arr i h` with `h` an explicit proof the
+    index is valid.
   -/
   getElem (xs : coll) (i : idx) (h : valid xs i) : elem
 
-export GetElem (getElem)
+  getElem? (xs : coll) (i : idx) [Decidable (valid xs i)] : Option elem :=
+    if h : _ then some (getElem xs i h) else none
+
+  getElem! [Inhabited elem] (xs : coll) (i : idx) [Decidable (valid xs i)] : elem :=
+    match getElem? xs i with | some e => e | none => outOfBounds
+
+export GetElem (getElem getElem! getElem?)
 
 @[inherit_doc getElem]
 syntax:max term noWs "[" withoutPosition(term) "]" : term
@@ -78,30 +66,6 @@ macro_rules | `($x[$i]) => `(getElem $x $i (by get_elem_tactic))
 syntax term noWs "[" withoutPosition(term) "]'" term:max : term
 macro_rules | `($x[$i]'$h) => `(getElem $x $i $h)
 
-/-- Helper function for implementation of `GetElem?.getElem?`. -/
-abbrev decidableGetElem? [GetElem coll idx elem valid] (xs : coll) (i : idx) [Decidable (valid xs i)] :
-    Option elem :=
-  if h : valid xs i then some xs[i] else none
-
-@[inherit_doc GetElem]
-class GetElem? (coll : Type u) (idx : Type v) (elem : outParam (Type w))
-    (valid : outParam (coll → idx → Prop)) extends GetElem coll idx elem valid where
-  /--
-  The syntax `arr[i]?` gets the `i`'th element of the collection `arr`,
-  if it is present (and wraps it in `some`), and otherwise returns `none`.
-  -/
-  getElem? : coll → idx → Option elem
-
-  /--
-  The syntax `arr[i]!` gets the `i`'th element of the collection `arr`,
-  if it is present, and otherwise panics at runtime and returns the `default` term
-  from `Inhabited elem`.
-  -/
-  getElem! [Inhabited elem] (xs : coll) (i : idx) : elem :=
-    match getElem? xs i with | some e => e | none => outOfBounds
-
-export GetElem? (getElem? getElem!)
-
 /--
 The syntax `arr[i]?` gets the `i`'th element of the collection `arr` or
 returns `none` if `i` is out of bounds.
@@ -114,43 +78,32 @@ panics `i` is out of bounds.
 -/
 macro:max x:term noWs "[" i:term "]" noWs "!" : term => `(getElem! $x $i)
 
-instance (priority := low) [GetElem coll idx elem valid] [∀ xs i, Decidable (valid xs i)] :
-    GetElem? coll idx elem valid where
-  getElem? xs i := decidableGetElem? xs i
-
 class LawfulGetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w))
-   (dom : outParam (cont → idx → Prop)) [ge : GetElem? cont idx elem dom] : Prop where
+   (dom : outParam (cont → idx → Prop)) [ge : GetElem cont idx elem dom] : Prop where
 
   getElem?_def (c : cont) (i : idx) [Decidable (dom c i)] :
-      c[i]? = if h : dom c i then some (c[i]'h) else none := by
-    intros
-    try simp only [getElem?] <;> congr
-  getElem!_def [Inhabited elem] (c : cont) (i : idx) :
-      c[i]! = match c[i]? with | some e => e | none => default := by
-    intros
-    simp only [getElem!, getElem?, outOfBounds_eq_default]
+    c[i]? = if h : dom c i then some (c[i]'h) else none := by intros; eq_refl
+  getElem!_def [Inhabited elem] (c : cont) (i : idx) [Decidable (dom c i)] :
+    c[i]! = match c[i]? with | some e => e | none => default := by intros; eq_refl
 
 export LawfulGetElem (getElem?_def getElem!_def)
 
-instance (priority := low) [GetElem coll idx elem valid] [∀ xs i, Decidable (valid xs i)] :
-    LawfulGetElem coll idx elem valid where
-
-theorem getElem?_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+theorem getElem?_pos [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
     (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] : c[i]? = some (c[i]'h) := by
   rw [getElem?_def]
   exact dif_pos h
 
-theorem getElem?_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+theorem getElem?_neg [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
     (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]? = none := by
   rw [getElem?_def]
   exact dif_neg h
 
-theorem getElem!_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+theorem getElem!_pos [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
     [Inhabited elem] (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] :
     c[i]! = c[i]'h := by
   simp only [getElem!_def, getElem?_def, h]
 
-theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
+theorem getElem!_neg [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom]
     [Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]! = default := by
   simp only [getElem!_def, getElem?_def, h]
 
@@ -158,23 +111,22 @@ namespace Fin
 
 instance instGetElemFinVal [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i where
   getElem xs i h := getElem xs i.1 h
-
-instance instGetElem?FinVal [GetElem? cont Nat elem dom] : GetElem? cont (Fin n) elem fun xs i => dom xs i where
   getElem? xs i := getElem? xs i.val
   getElem! xs i := getElem! xs i.val
 
-instance [GetElem? cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] :
+instance [GetElem cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] :
       LawfulGetElem cont (Fin n) elem fun xs i => dom xs i where
-  getElem?_def _c _i _d := h.getElem?_def ..
-  getElem!_def _c _i := h.getElem!_def ..
 
-@[simp] theorem getElem_fin [GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
+  getElem?_def _c _i _d := h.getElem?_def ..
+  getElem!_def _c _i _d := h.getElem!_def ..
+
+@[simp] theorem getElem_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
     a[i] = a[i.1] := rfl
 
-@[simp] theorem getElem?_fin [h : GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n)
+@[simp] theorem getElem?_fin [h : GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n)
     [Decidable (Dom a i)] : a[i]? = a[i.1]? := by rfl
 
-@[simp] theorem getElem!_fin [GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n)
+@[simp] theorem getElem!_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n)
     [Decidable (Dom a i)] [Inhabited Elem] : a[i]! = a[i.1]! := rfl
 
 macro_rules
@@ -187,6 +139,8 @@ namespace List
 instance : GetElem (List α) Nat α fun as i => i < as.length where
   getElem as i h := as.get ⟨i, h⟩
 
+instance : LawfulGetElem (List α) Nat α fun as i => i < as.length where
+
 @[simp] theorem getElem_cons_zero (a : α) (as : List α) (h : 0 < (a :: as).length) : getElem (a :: as) 0 h = a := by
   rfl
 
@@ -209,6 +163,8 @@ namespace Array
 instance : GetElem (Array α) Nat α fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
 
+instance : LawfulGetElem (Array α) Nat α fun xs i => i < xs.size where
+
 end Array
 
 namespace Lean.Syntax
@@ -216,4 +172,6 @@ namespace Lean.Syntax
 instance : GetElem Syntax Nat Syntax fun _ _ => True where
   getElem stx i _ := stx.getArg i
 
+instance : LawfulGetElem Syntax Nat Syntax fun _ _ => True where
+
 end Lean.Syntax

src/Init/Prelude.lean

@@ -2329,6 +2329,9 @@ without running out of stack space.
 def List.lengthTR (as : List α) : Nat :=
   lengthTRAux as 0
 
+@[simp] theorem List.length_cons {α} (a : α) (as : List α) : Eq (cons a as).length as.length.succ :=
+  rfl
+
 /--
 `as.get i` returns the `i`'th element of the list `as`.
 This version of the function uses `i : Fin as.length` to ensure that it will

src/Init/Tactics.lean

@@ -373,8 +373,7 @@ reflexivity theorems (e.g., `Iff.rfl`).
 macro "rfl" : tactic => `(tactic| case' _ => fail "The rfl tactic failed. Possible reasons:
 - The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
 - The arguments of the relation are not equal.
-Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
-`exact HEq.rfl` etc.")
+Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.")
 
 macro_rules | `(tactic| rfl) => `(tactic| eq_refl)
 macro_rules | `(tactic| rfl) => `(tactic| exact HEq.rfl)

src/Lean/AddDecl.lean

@@ -8,17 +8,8 @@ import Lean.CoreM
 
 namespace Lean
 
-register_builtin_option debug.skipKernelTC : Bool := {
-  defValue := false
-  group    := "debug"
-  descr    := "skip kernel type checker. WARNING: setting this option to true may compromise soundness because your proofs will not be checked by the Lean kernel"
-}
-
 def Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration) : Except KernelException Environment :=
-  if debug.skipKernelTC.get opts then
-    addDeclWithoutChecking env decl
-  else
-    addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl
+  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

src/Lean/BuiltinDocAttr.lean

@@ -5,12 +5,12 @@ Authors: Mario Carneiro
 -/
 prelude
 import Lean.Compiler.InitAttr
-import Lean.DocString.Extension
+import Lean.DocString
 
 namespace Lean
 
 def declareBuiltinDocStringAndRanges (declName : Name) : AttrM Unit := do
-  if let some doc ← findSimpleDocString? (← getEnv) declName (includeBuiltin := false) then
+  if let some doc ← findDocString? (← getEnv) declName (includeBuiltin := false) then
     declareBuiltin (declName ++ `docString) (mkAppN (mkConst ``addBuiltinDocString) #[toExpr declName, toExpr doc])
   if let some declRanges ← findDeclarationRanges? declName then
     declareBuiltin (declName ++ `declRange) (mkAppN (mkConst ``addBuiltinDeclarationRanges) #[toExpr declName, toExpr declRanges])

src/Lean/Compiler/FFI.lean

@@ -18,13 +18,6 @@ private opaque getLeancExtraFlags : Unit → String
 def getCFlags (leanSysroot : FilePath) : Array String :=
   #["-I", (leanSysroot / "include").toString] ++ (getLeancExtraFlags ()).trim.splitOn
 
-@[extern "lean_get_leanc_internal_flags"]
-private opaque getLeancInternalFlags : Unit → String
-
-/-- Return C compiler flags needed to use the C compiler bundled with the Lean toolchain. -/
-def getInternalCFlags (leanSysroot : FilePath) : Array String :=
-  (getLeancInternalFlags ()).trim.splitOn.toArray.map (·.replace "ROOT" leanSysroot.toString)
-
 @[extern "lean_get_linker_flags"]
 private opaque getBuiltinLinkerFlags (linkStatic : Bool) : String
 
@@ -32,11 +25,4 @@ private opaque getBuiltinLinkerFlags (linkStatic : Bool) : String
 def getLinkerFlags (leanSysroot : FilePath) (linkStatic := true) : Array String :=
   #["-L", (leanSysroot / "lib" / "lean").toString] ++ (getBuiltinLinkerFlags linkStatic).trim.splitOn
 
-@[extern "lean_get_internal_linker_flags"]
-private opaque getBuiltinInternalLinkerFlags : Unit → String
-
-/-- Return linker flags needed to use the linker bundled with the Lean toolchain. -/
-def getInternalLinkerFlags (leanSysroot : FilePath) : Array String :=
-  (getBuiltinInternalLinkerFlags ()).trim.splitOn.toArray.map (·.replace "ROOT" leanSysroot.toString)
-
 end Lean.Compiler.FFI

src/Lean/CoreM.lean

@@ -472,30 +472,23 @@ def Exception.isInterrupt : Exception → Bool
 
 /--
 Custom `try-catch` for all monads based on `CoreM`. We usually don't want to catch "runtime
-exceptions" these monads, but on `CommandElabM` or, in specific cases, using `tryCatchRuntimeEx`.
-See issues #2775 and #2744 as well as `MonadAlwaysExcept`. Also, we never want to catch interrupt
-exceptions inside the elaborator.
+exceptions" these monads, but on `CommandElabM`. See issues #2775 and #2744 as well as
+`MonadAlwaysExcept`. Also, we never want to catch interrupt exceptions inside the elaborator.
 -/
 @[inline] protected def Core.tryCatch (x : CoreM α) (h : Exception → CoreM α) : CoreM α := do
   try
     x
   catch ex =>
     if ex.isInterrupt || ex.isRuntime then
-      throw ex
+
+      throw ex -- We should use `tryCatchRuntimeEx` for catching runtime exceptions
     else
       h ex
 
-/--
-A variant of `tryCatch` that also catches runtime exception (see also `tryCatch` documentation).
-Like `tryCatch`, this function does not catch interrupt exceptions, which are not considered runtime
-exceptions.
--/
 @[inline] protected def Core.tryCatchRuntimeEx (x : CoreM α) (h : Exception → CoreM α) : CoreM α := do
   try
     x
   catch ex =>
-    if ex.isInterrupt then
-      throw ex
     h ex
 
 instance : MonadExceptOf Exception CoreM where

src/Lean/Data/HashMap.lean

@@ -223,6 +223,8 @@ def insertIfNew (m : HashMap α β) (a : α) (b : β) : HashMap α β × Option
 instance : GetElem (HashMap α β) α (Option β) fun _ _ => True where
   getElem m k _ := m.find? k
 
+instance : LawfulGetElem (HashMap α β) α (Option β) fun _ _ => True where
+
 @[inline] def contains (m : HashMap α β) (a : α) : Bool :=
   match m with
   | ⟨ m, _ ⟩ => m.contains a

src/Lean/Data/PersistentArray.lean

@@ -72,6 +72,8 @@ def get! [Inhabited α] (t : PersistentArray α) (i : Nat) : α :=
 instance [Inhabited α] : GetElem (PersistentArray α) Nat α fun as i => i < as.size where
   getElem xs i _ := xs.get! i
 
+instance [Inhabited α] : LawfulGetElem (PersistentArray α) Nat α fun as i => i < as.size where
+
 partial def setAux : PersistentArrayNode α → USize → USize → α → PersistentArrayNode α
   | node cs, i, shift, a =>
     let j     := div2Shift i shift

src/Lean/Data/PersistentHashMap.lean

@@ -161,6 +161,8 @@ def find? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → Op
 instance {_ : BEq α} {_ : Hashable α} : GetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where
   getElem m i _ := m.find? i
 
+instance {_ : BEq α} {_ : Hashable α} : LawfulGetElem (PersistentHashMap α β) α (Option β) fun _ _ => True where
+
 @[inline] def findD {_ : BEq α} {_ : Hashable α} (m : PersistentHashMap α β) (a : α) (b₀ : β) : β :=
   (m.find? a).getD b₀
 

src/Lean/DocString.lean

@@ -4,26 +4,58 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.DocString.Extension
-import Lean.Parser.Tactic.Doc
-
-set_option linter.missingDocs true
-
--- This module contains the main query interface for docstrings, which assembles user-visible
--- docstrings.
--- The module `Lean.DocString.Extension` contains the underlying data.
+import Lean.DeclarationRange
+import Lean.MonadEnv
+import Init.Data.String.Extra
 
 namespace Lean
-open Lean.Parser.Tactic.Doc
 
-/--
-Finds the docstring for a name, taking tactic alternate forms and documentation extensions into
-account.
+private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) ← IO.mkRef {}
+private builtin_initialize docStringExt : MapDeclarationExtension String ← mkMapDeclarationExtension
 
-Use `Lean.findSimpleDocString?` to look up the raw docstring without resolving alternate forms or
-including extensions.
--/
-def findDocString? (env : Environment) (declName : Name) (includeBuiltin := true) : IO (Option String) := do
-  let declName := alternativeOfTactic env declName |>.getD declName
-  let exts := getTacticExtensionString env declName
-  return (← findSimpleDocString? env declName (includeBuiltin := includeBuiltin)).map (· ++ exts)
+def addBuiltinDocString (declName : Name) (docString : String) : IO Unit :=
+  builtinDocStrings.modify (·.insert declName docString.removeLeadingSpaces)
+
+def addDocString [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString : String) : m Unit := do
+  unless (← getEnv).getModuleIdxFor? declName |>.isNone do
+    throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
+  modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces
+
+def addDocString' [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit :=
+  match docString? with
+  | some docString => addDocString declName docString
+  | none => return ()
+
+def findDocString? (env : Environment) (declName : Name) (includeBuiltin := true) : IO (Option String) :=
+  if let some docStr := docStringExt.find? env declName then
+    return some docStr
+  else if includeBuiltin then
+    return (← builtinDocStrings.get).find? declName
+  else
+    return none
+
+structure ModuleDoc where
+  doc : String
+  declarationRange : DeclarationRange
+
+private builtin_initialize moduleDocExt : SimplePersistentEnvExtension ModuleDoc (PersistentArray ModuleDoc) ← registerSimplePersistentEnvExtension {
+  addImportedFn := fun _ => {}
+  addEntryFn    := fun s e => s.push e
+  toArrayFn     := fun es => es.toArray
+}
+
+def addMainModuleDoc (env : Environment) (doc : ModuleDoc) : Environment :=
+  moduleDocExt.addEntry env doc
+
+def getMainModuleDoc (env : Environment) : PersistentArray ModuleDoc :=
+  moduleDocExt.getState env
+
+def getModuleDoc? (env : Environment) (moduleName : Name) : Option (Array ModuleDoc) :=
+  env.getModuleIdx? moduleName |>.map fun modIdx => moduleDocExt.getModuleEntries env modIdx
+
+def getDocStringText [Monad m] [MonadError m] (stx : TSyntax `Lean.Parser.Command.docComment) : m String :=
+  match stx.raw[1] with
+  | Syntax.atom _ val => return val.extract 0 (val.endPos - ⟨2⟩)
+  | _                 => throwErrorAt stx "unexpected doc string{indentD stx.raw[1]}"
+
+end Lean

src/Lean/DocString/Extension.lean

@@ -1,69 +0,0 @@
-/-
-Copyright (c) 2021 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.DeclarationRange
-import Lean.MonadEnv
-import Init.Data.String.Extra
-
--- This module contains the underlying data for docstrings, with as few imports as possible, so that
--- docstrings can be saved in as much of the compiler as possible.
--- The module `Lean.DocString` contains the query interface, which needs to look at additional data
--- to construct user-visible docstrings.
-
-namespace Lean
-
-private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) ← IO.mkRef {}
-private builtin_initialize docStringExt : MapDeclarationExtension String ← mkMapDeclarationExtension
-
-def addBuiltinDocString (declName : Name) (docString : String) : IO Unit :=
-  builtinDocStrings.modify (·.insert declName docString.removeLeadingSpaces)
-
-def addDocString [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString : String) : m Unit := do
-  unless (← getEnv).getModuleIdxFor? declName |>.isNone do
-    throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
-  modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces
-
-def addDocString' [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit :=
-  match docString? with
-  | some docString => addDocString declName docString
-  | none => return ()
-
-/--
-Finds a docstring without performing any alias resolution or enrichment with extra metadata.
-
-Docstrings to be shown to a user should be looked up with `Lean.findDocString?` instead.
--/
-def findSimpleDocString? (env : Environment) (declName : Name) (includeBuiltin := true) : IO (Option String) :=
-  if let some docStr := docStringExt.find? env declName then
-    return some docStr
-  else if includeBuiltin then
-    return (← builtinDocStrings.get).find? declName
-  else
-    return none
-
-structure ModuleDoc where
-  doc : String
-  declarationRange : DeclarationRange
-
-private builtin_initialize moduleDocExt : SimplePersistentEnvExtension ModuleDoc (PersistentArray ModuleDoc) ← registerSimplePersistentEnvExtension {
-  addImportedFn := fun _ => {}
-  addEntryFn    := fun s e => s.push e
-  toArrayFn     := fun es => es.toArray
-}
-
-def addMainModuleDoc (env : Environment) (doc : ModuleDoc) : Environment :=
-  moduleDocExt.addEntry env doc
-
-def getMainModuleDoc (env : Environment) : PersistentArray ModuleDoc :=
-  moduleDocExt.getState env
-
-def getModuleDoc? (env : Environment) (moduleName : Name) : Option (Array ModuleDoc) :=
-  env.getModuleIdx? moduleName |>.map fun modIdx => moduleDocExt.getModuleEntries env modIdx
-
-def getDocStringText [Monad m] [MonadError m] (stx : TSyntax `Lean.Parser.Command.docComment) : m String :=
-  match stx.raw[1] with
-  | Syntax.atom _ val => return val.extract 0 (val.endPos - ⟨2⟩)
-  | _                 => throwErrorAt stx "unexpected doc string{indentD stx.raw[1]}"

src/Lean/Elab.lean

@@ -50,4 +50,3 @@ import Lean.Elab.ParseImportsFast
 import Lean.Elab.GuardMsgs
 import Lean.Elab.CheckTactic
 import Lean.Elab.MatchExpr
-import Lean.Elab.Tactic.Doc

src/Lean/Elab/BuiltinTerm.lean

@@ -157,19 +157,9 @@ private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr :=
   registerSyntheticMVar ref mvarId <| SyntheticMVarKind.tactic tacticCode (← saveContext)
   return mvar
 
-register_builtin_option debug.byAsSorry : Bool := {
-  defValue := false
-  group    := "debug"
-  descr    := "replace `by ..` blocks with `sorry` IF the expected type is a proposition"
-}
-
 @[builtin_term_elab byTactic] def elabByTactic : TermElab := fun stx expectedType? => do
   match expectedType? with
-  | some expectedType =>
-    if ← pure (debug.byAsSorry.get (← getOptions)) <&&> isProp expectedType then
-      mkSorry expectedType false
-    else
-      mkTacticMVar expectedType stx
+  | some expectedType => mkTacticMVar expectedType stx
   | none =>
     tryPostpone
     throwError ("invalid 'by' tactic, expected type has not been provided")

src/Lean/Elab/Command.lean

@@ -81,10 +81,7 @@ Remark: see comment at TermElabM
 @[always_inline]
 instance : Monad CommandElabM := let i := inferInstanceAs (Monad CommandElabM); { pure := i.pure, bind := i.bind }
 
-/--
-Like `Core.tryCatchRuntimeEx`; runtime errors are generally used to abort term elaboration, so we do
-want to catch and process them at the command level.
--/
+/-- Like `Core.tryCatch` but do catch runtime exceptions. -/
 @[inline] protected def tryCatch (x : CommandElabM α) (h : Exception → CommandElabM α) :
     CommandElabM α := do
   try

src/Lean/Elab/InheritDoc.lean

@@ -5,7 +5,7 @@ Authors: Mario Carneiro
 -/
 prelude
 import Lean.Elab.InfoTree.Main
-import Lean.DocString.Extension
+import Lean.DocString
 
 namespace Lean
 
@@ -21,9 +21,9 @@ builtin_initialize
         let some id := id?
           | throwError "invalid `[inherit_doc]` attribute, could not infer doc source"
         let declName ← Elab.realizeGlobalConstNoOverloadWithInfo id
-        if (← findSimpleDocString? (← getEnv) decl).isSome then
+        if (← findDocString? (← getEnv) decl).isSome then
           logWarning m!"{← mkConstWithLevelParams decl} already has a doc string"
-        let some doc ← findSimpleDocString? (← getEnv) declName
+        let some doc ← findDocString? (← getEnv) declName
           | logWarningAt id m!"{← mkConstWithLevelParams declName} does not have a doc string"
         addDocString decl doc
       | _  => throwError "invalid `[inherit_doc]` attribute"

src/Lean/Elab/LetRec.lean

@@ -30,24 +30,20 @@ structure LetRecView where
 
 /-  group ("let " >> nonReservedSymbol "rec ") >> sepBy1 (group (optional «attributes» >> letDecl)) ", " >> "; " >> termParser -/
 private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
-  let mut decls : Array LetRecDeclView := #[]
-  for attrDeclStx in letRec[1][0].getSepArgs do
+  let decls ← letRec[1][0].getSepArgs.mapM fun (attrDeclStx : Syntax) => do
     let docStr? ← expandOptDocComment? attrDeclStx[0]
     let attrOptStx := attrDeclStx[1]
     let attrs ← if attrOptStx.isNone then pure #[] else elabDeclAttrs attrOptStx[0]
     let decl := attrDeclStx[2][0]
     if decl.isOfKind `Lean.Parser.Term.letPatDecl then
       throwErrorAt decl "patterns are not allowed in 'let rec' expressions"
-    else if decl.isOfKind ``Lean.Parser.Term.letIdDecl || decl.isOfKind ``Lean.Parser.Term.letEqnsDecl then
+    else if decl.isOfKind `Lean.Parser.Term.letIdDecl || decl.isOfKind `Lean.Parser.Term.letEqnsDecl then
       let declId := decl[0]
       unless declId.isIdent do
         throwErrorAt declId "'let rec' expressions must be named"
       let shortDeclName := declId.getId
       let currDeclName? ← getDeclName?
       let declName := currDeclName?.getD Name.anonymous ++ shortDeclName
-      if decls.any fun decl => decl.declName == declName then
-        withRef declId do
-          throwError "'{declName}' has already been declared"
       checkNotAlreadyDeclared declName
       applyAttributesAt declName attrs AttributeApplicationTime.beforeElaboration
       addDocString' declName docStr?
@@ -66,10 +62,8 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
       else
         liftMacroM <| expandMatchAltsIntoMatch decl decl[3]
       let termination ← WF.elabTerminationHints ⟨attrDeclStx[3]⟩
-      decls := decls.push {
-        ref := declId, attrs, shortDeclName, declName,
-        binderIds, type, mvar, valStx, termination
-      }
+      pure { ref := declId, attrs, shortDeclName, declName, binderIds, type, mvar, valStx,
+             termination : LetRecDeclView }
     else
       throwUnsupportedSyntax
   return { decls, body := letRec[3] }

src/Lean/Elab/MutualDef.lean

@@ -846,7 +846,7 @@ private def levelMVarToParamHeaders (views : Array DefView) (headers : Array Def
   let rec process : StateRefT Nat TermElabM (Array DefViewElabHeader) := do
     let mut newHeaders := #[]
     for view in views, header in headers do
-      if ← pure view.kind.isTheorem <||> isProp header.type then
+      if view.kind.isTheorem then
         newHeaders ←
           withLevelNames header.levelNames do
             return newHeaders.push { header with type := (← levelMVarToParam header.type), levelNames := (← getLevelNames) }

src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean

@@ -35,61 +35,12 @@ private def hasBadParamDep? (ys : Array Expr) (indParams : Array Expr) : MetaM (
         return some (p, y)
   return none
 
-/--
-Pass to `k` the `RecArgInfo` for the `i`th parameter in the parameter list `xs`. This performs
-various sanity checks on the argument (is it even an inductive type etc).
-Also wraps all errors in a common “argument cannot be used” header
--/
-def withRecArgInfo (numFixed : Nat) (xs : Array Expr) (i : Nat) (k : RecArgInfo → M α) : M α := do
-  mapError
-    (f := fun msg => m!"argument #{i+1} cannot be used for structural recursion{indentD msg}") do
-  if h : i < xs.size then
-    if i < numFixed then
-      throwError "it is unchanged in the recursive calls"
-    let x := xs[i]
-    let localDecl ← getFVarLocalDecl x
-    if localDecl.isLet then
-      throwError "it is a let-binding"
-    let xType ← whnfD localDecl.type
-    matchConstInduct xType.getAppFn (fun _ => throwError "its type is not an inductive") fun indInfo us => do
-    if !(← hasConst (mkBRecOnName indInfo.name)) then
-      throwError "its type does not have a recursor"
-    else if indInfo.isReflexive && !(← hasConst (mkBInductionOnName indInfo.name)) && !(← isInductivePredicate indInfo.name) then
-      throwError "its type is a reflexive inductive, but {mkBInductionOnName indInfo.name} does not exist and it is not an inductive predicate"
-    else
-      let indArgs    := xType.getAppArgs
-      let indParams  := indArgs.extract 0 indInfo.numParams
-      let indIndices := indArgs.extract indInfo.numParams indArgs.size
-      if !indIndices.all Expr.isFVar then
-        throwError "its type is an inductive family and indices are not variables{indentExpr xType}"
-      else if !indIndices.allDiff then
-        throwError " its type is an inductive family and indices are not pairwise distinct{indentExpr xType}"
-      else
-        let indexMinPos := getIndexMinPos xs indIndices
-        let numFixed    := if indexMinPos < numFixed then indexMinPos else numFixed
-        let fixedParams := xs.extract 0 numFixed
-        let ys          := xs.extract numFixed xs.size
-        match (← hasBadIndexDep? ys indIndices) with
-        | some (index, y) =>
-          throwError "its type is an inductive family{indentExpr xType}\nand index{indentExpr index}\ndepends on the non index{indentExpr y}"
-        | none =>
-          match (← hasBadParamDep? ys indParams) with
-          | some (indParam, y) =>
-            throwError "its type is an inductive datatype{indentExpr xType}\nand parameter{indentExpr indParam}\ndepends on{indentExpr y}"
-          | none =>
-            let indicesPos := indIndices.map fun index => match ys.indexOf? index with | some i => i.val | none => unreachable!
-            k { fixedParams := fixedParams
-                ys          := ys
-                pos         := i - fixedParams.size
-                indicesPos  := indicesPos
-                indName     := indInfo.name
-                indLevels   := us
-                indParams   := indParams
-                indIndices  := indIndices
-                reflexive   := indInfo.isReflexive
-                indPred     := ←isInductivePredicate indInfo.name }
-    else
-      throwError "the index #{i+1} exceeds {xs.size}, the number of parameters"
+private def throwStructuralFailed : MetaM α :=
+  throwError "structural recursion cannot be used"
+
+private def orelse' (x y : M α) : M α := do
+  let saveState ← get
+  orelseMergeErrors x (do set saveState; y)
 
 /--
   Try to find an argument that is structurally smaller in every recursive application.
@@ -98,10 +49,16 @@ def withRecArgInfo (numFixed : Nat) (xs : Array Expr) (i : Nat) (k : RecArgInfo
   We give preference for arguments that are *not* indices of inductive types of other arguments.
   See issue #837 for an example where we can show termination using the index of an inductive family, but
   we don't get the desired definitional equalities.
+
+  We perform two passes. In the first-pass, we only consider arguments that are not indices.
+  In the second pass, we consider them.
+
+  TODO: explore whether there are better solutions, and whether there are other ways to break the heuristic used
+  for creating the smart unfolding auxiliary definition.
 -/
 partial def findRecArg (numFixed : Nat) (xs : Array Expr) (k : RecArgInfo → M α) : M α := do
   /- Collect arguments that are indices. See comment above. -/
-  let indicesRef : IO.Ref (Array Nat) ← IO.mkRef {}
+  let indicesRef : IO.Ref FVarIdSet ← IO.mkRef {}
   for x in xs do
     let xType ← inferType x
     /- Traverse all sub-expressions in the type of `x` -/
@@ -111,22 +68,75 @@ partial def findRecArg (numFixed : Nat) (xs : Array Expr) (k : RecArgInfo → M
         if info.numIndices > 0 && info.numParams + info.numIndices == e.getAppNumArgs then
           for arg in e.getAppArgs[info.numParams:] do
             forEachExpr arg fun e => do
-              if let .some idx := xs.getIdx? e then
-                indicesRef.modify fun indices => indices.push idx
+              if e.isFVar && xs.any (· == e) then
+                indicesRef.modify fun indices => indices.insert e.fvarId!
   let indices ← indicesRef.get
-  let nonIndices := (Array.range xs.size).filter (fun i => !(indices.contains i))
-  let mut errors : Array MessageData := Array.mkArray xs.size m!""
-  let saveState ← get -- backtrack the state for each argument
-  for i in id (nonIndices ++ indices) do
-    let x := xs[i]!
-    trace[Elab.definition.structural] "findRecArg x: {x}"
-    try
-      set saveState
-      return (← withRecArgInfo numFixed xs i k)
-    catch e => errors := errors.set! i e.toMessageData
-  throwError
-    errors.foldl
-      (init := m!"structural recursion cannot be used:")
-      (f := (· ++ Format.line ++ Format.line ++ .))
+  /- We perform two passes. See comment above. -/
+  let rec go (i : Nat) (firstPass : Bool) : M α := do
+    if h : i < xs.size then
+      let x := xs.get ⟨i, h⟩
+      trace[Elab.definition.structural] "findRecArg x: {x}, firstPass: {firstPass}"
+      let localDecl ← getFVarLocalDecl x
+      if localDecl.isLet then
+        throwStructuralFailed
+      else if firstPass == indices.contains localDecl.fvarId then
+        go (i+1) firstPass
+      else
+        let xType ← whnfD localDecl.type
+        matchConstInduct xType.getAppFn (fun _ => go (i+1) firstPass) fun indInfo us => do
+        if !(← hasConst (mkBRecOnName indInfo.name)) then
+          go (i+1) firstPass
+        else if indInfo.isReflexive && !(← hasConst (mkBInductionOnName indInfo.name)) && !(← isInductivePredicate indInfo.name) then
+          go (i+1) firstPass
+        else
+          let indArgs    := xType.getAppArgs
+          let indParams  := indArgs.extract 0 indInfo.numParams
+          let indIndices := indArgs.extract indInfo.numParams indArgs.size
+          if !indIndices.all Expr.isFVar then
+            orelse'
+              (throwError "argument #{i+1} was not used because its type is an inductive family and indices are not variables{indentExpr xType}")
+              (go (i+1) firstPass)
+          else if !indIndices.allDiff then
+            orelse'
+              (throwError "argument #{i+1} was not used because its type is an inductive family and indices are not pairwise distinct{indentExpr xType}")
+              (go (i+1) firstPass)
+          else
+            let indexMinPos := getIndexMinPos xs indIndices
+            let numFixed    := if indexMinPos < numFixed then indexMinPos else numFixed
+            let fixedParams := xs.extract 0 numFixed
+            let ys          := xs.extract numFixed xs.size
+            match (← hasBadIndexDep? ys indIndices) with
+            | some (index, y) =>
+              orelse'
+                (throwError "argument #{i+1} was not used because its type is an inductive family{indentExpr xType}\nand index{indentExpr index}\ndepends on the non index{indentExpr y}")
+                (go (i+1) firstPass)
+            | none =>
+              match (← hasBadParamDep? ys indParams) with
+              | some (indParam, y) =>
+                orelse'
+                  (throwError "argument #{i+1} was not used because its type is an inductive datatype{indentExpr xType}\nand parameter{indentExpr indParam}\ndepends on{indentExpr y}")
+                  (go (i+1) firstPass)
+              | none =>
+                let indicesPos := indIndices.map fun index => match ys.indexOf? index with | some i => i.val | none => unreachable!
+                orelse'
+                  (mapError
+                    (k { fixedParams := fixedParams
+                         ys          := ys
+                         pos         := i - fixedParams.size
+                         indicesPos  := indicesPos
+                         indName     := indInfo.name
+                         indLevels   := us
+                         indParams   := indParams
+                         indIndices  := indIndices
+                         reflexive := indInfo.isReflexive
+                         indPred := ←isInductivePredicate indInfo.name })
+                    (fun msg => m!"argument #{i+1} was not used for structural recursion{indentD msg}"))
+                  (go (i+1) firstPass)
+    else if firstPass then
+      go (i := numFixed) (firstPass := false)
+    else
+      throwStructuralFailed
+
+  go (i := numFixed) (firstPass := true)
 
 end Lean.Elab.Structural

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

@@ -66,6 +66,7 @@ private def elimRecursion (preDef : PreDefinition) : M (Nat × PreDefinition) :=
     let numFixed ← getFixedPrefix preDef.declName xs value
     trace[Elab.definition.structural] "numFixed: {numFixed}"
     findRecArg numFixed xs fun recArgInfo => do
+      -- when (recArgInfo.indName == `Nat) throwStructuralFailed -- HACK to skip Nat argument
       let valueNew ← if recArgInfo.indPred then
         mkIndPredBRecOn preDef.declName recArgInfo value
       else

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -199,7 +199,7 @@ def evalTacticCDot : Tactic := fun stx => do
   -- but the token antiquotation does not copy trailing whitespace, leading to
   -- differences in the goal display (#2153)
   let initInfo ← mkInitialTacticInfo stx[0]
-  withCaseRef stx[0] stx[1] <| closeUsingOrAdmit do
+  withRef stx[0] <| closeUsingOrAdmit do
     -- save state before/after entering focus on `·`
     withInfoContext (pure ()) initInfo
     Term.withNarrowedArgTacticReuse (argIdx := 1) evalTactic stx

src/Lean/Elab/Tactic/Doc.lean

@@ -1,178 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: David Thrane Christiansen
--/
-prelude
-import Lean.DocString
-import Lean.Elab.Command
-import Lean.Parser.Tactic.Doc
-import Lean.Parser.Command
-
-namespace Lean.Elab.Tactic.Doc
-open Lean.Parser.Tactic.Doc
-open Lean.Elab.Command
-open Lean.Parser.Command
-
-@[builtin_command_elab «tactic_extension»] def elabTacticExtension : CommandElab
-  | `(«tactic_extension»|tactic_extension%$cmd $_) => do
-    throwErrorAt cmd "Missing documentation comment"
-  | `(«tactic_extension»|$docs:docComment tactic_extension $tac:ident) => do
-    let tacName ← liftTermElabM <| realizeGlobalConstNoOverloadWithInfo tac
-
-    if let some tgt' := alternativeOfTactic (← getEnv) tacName then
-        throwErrorAt tac "'{tacName}' is an alternative form of '{tgt'}'"
-    if !(isTactic (← getEnv) tacName) then
-      throwErrorAt tac "'{tacName}' is not a tactic"
-
-    modifyEnv (tacticDocExtExt.addEntry · (tacName, docs.getDocString))
-    pure ()
-  | _ => throwError "Malformed tactic extension command"
-
-@[builtin_command_elab «register_tactic_tag»] def elabRegisterTacticTag : CommandElab
-  | `(«register_tactic_tag»|$[$doc:docComment]? register_tactic_tag $tag:ident $user:str) => do
-    let docstring ← doc.mapM getDocStringText
-    modifyEnv (knownTacticTagExt.addEntry · (tag.getId, user.getString, docstring))
-  | _ => throwError "Malformed 'register_tactic_tag' command"
-
-/--
-Gets the first string token in a parser description. For example, for a declaration like
-`syntax "squish " term " with " term : tactic`, it returns `some "squish "`, and for a declaration
-like `syntax tactic " <;;;> " tactic : tactic`, it returns `some " <;;;> "`.
-
-Returns `none` for syntax declarations that don't contain a string constant.
--/
-private partial def getFirstTk (e : Expr) : MetaM (Option String) := do
-  match (← Meta.whnf e).getAppFnArgs with
-  | (``ParserDescr.node, #[_, _, p]) => getFirstTk p
-  | (``ParserDescr.trailingNode, #[_, _, _, p]) => getFirstTk p
-  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "withPosition")), p]) => getFirstTk p
-  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "atomic")), p]) => getFirstTk p
-  | (``ParserDescr.binary, #[.app _ (.lit (.strVal "andthen")), p, _]) => getFirstTk p
-  | (``ParserDescr.nonReservedSymbol, #[.lit (.strVal tk), _]) => pure (some tk)
-  | (``ParserDescr.symbol, #[.lit (.strVal tk)]) => pure (some tk)
-  | (``Parser.withAntiquot, #[_, p]) => getFirstTk p
-  | (``Parser.leadingNode, #[_, _, p]) => getFirstTk p
-  | (``HAndThen.hAndThen, #[_, _, _, _, p1, p2]) =>
-    if let some tk ← getFirstTk p1 then pure (some tk)
-    else getFirstTk (.app p2 (.const ``Unit.unit []))
-  | (``Parser.nonReservedSymbol, #[.lit (.strVal tk), _]) => pure (some tk)
-  | (``Parser.symbol, #[.lit (.strVal tk)]) => pure (some tk)
-  | _ => pure none
-
-
-/--
-Creates some `MessageData` for a parser name.
-
-If the parser name maps to a description with an
-identifiable leading token, then that token is shown. Otherwise, the underlying name is shown
-without an `@`. The name includes metadata that makes infoview hovers and the like work. This
-only works for global constants, as the local context is not included.
--/
-private def showParserName (n : Name) : MetaM MessageData := do
-  let env ← getEnv
-  let params :=
-    env.constants.find?' n |>.map (·.levelParams.map Level.param) |>.getD []
-  let tok ←
-    if let some descr := env.find? n |>.bind (·.value?) then
-      if let some tk ← getFirstTk descr then
-        pure <| Std.Format.text tk.trim
-      else pure <| format n
-    else pure <| format n
-  pure <| .ofFormatWithInfos {
-    fmt := "'" ++ .tag 0 tok ++ "'",
-    infos :=
-      .fromList [(0, .ofTermInfo {
-        lctx := .empty,
-        expr := .const n params,
-        stx := .ident .none (toString n).toSubstring n [.decl n []],
-        elaborator := `Delab,
-        expectedType? := none
-      })] _
-  }
-
-
-/--
-Displays all available tactic tags, with documentation.
--/
-@[builtin_command_elab printTacTags] def elabPrintTacTags : CommandElab := fun _stx => do
-  let all :=
-    tacticTagExt.toEnvExtension.getState (← getEnv)
-      |>.importedEntries |>.push (tacticTagExt.exportEntriesFn (tacticTagExt.getState (← getEnv)))
-  let mut mapping : NameMap NameSet := {}
-  for arr in all do
-    for (tac, tag) in arr do
-      mapping := mapping.insert tag (mapping.findD tag {} |>.insert tac)
-
-  let showDocs : Option String → MessageData
-    | none => .nil
-    | some d => Format.line ++ MessageData.joinSep ((d.splitOn "\n").map toMessageData) Format.line
-
-  let showTactics (tag : Name) : MetaM MessageData := do
-    match mapping.find? tag with
-    | none => pure .nil
-    | some tacs =>
-      if tacs.isEmpty then pure .nil
-      else
-        let tacs := tacs.toArray.qsort (·.toString < ·.toString) |>.toList
-        pure (Format.line ++ MessageData.joinSep (← tacs.mapM showParserName) ", ")
-
-  let tagDescrs ← liftTermElabM <| (← allTagsWithInfo).mapM fun (name, userName, docs) => do
-    pure <| m!"• " ++
-      MessageData.nestD (m!"'{name}'" ++
-        (if name.toString != userName then m!" — \"{userName}\"" else MessageData.nil) ++
-        showDocs docs ++
-        (← showTactics name))
-
-  let tagList : MessageData :=
-    m!"Available tags: {MessageData.nestD (Format.line ++ .joinSep tagDescrs Format.line)}"
-
-  logInfo tagList
-
-/--
-The information needed to display all documentation for a tactic.
--/
-structure TacticDoc where
-  /-- The name of the canonical parser for the tactic -/
-  internalName : Name
-  /-- The user-facing name to display (typically the first keyword token) -/
-  userName : String
-  /-- The tags that have been applied to the tactic -/
-  tags : NameSet
-  /-- The docstring for the tactic -/
-  docString : Option String
-  /-- Any docstring extensions that have been specified -/
-  extensionDocs : Array String
-
-def allTacticDocs : MetaM (Array TacticDoc) := do
-  let env ← getEnv
-  let all :=
-    tacticTagExt.toEnvExtension.getState (← getEnv)
-      |>.importedEntries |>.push (tacticTagExt.exportEntriesFn (tacticTagExt.getState (← getEnv)))
-  let mut tacTags : NameMap NameSet := {}
-  for arr in all do
-    for (tac, tag) in arr do
-      tacTags := tacTags.insert tac (tacTags.findD tac {} |>.insert tag)
-
-  let mut docs := #[]
-
-  let some tactics := (Lean.Parser.parserExtension.getState env).categories.find? `tactic
-    | return #[]
-  for (tac, _) in tactics.kinds do
-    -- Skip noncanonical tactics
-    if let some _ := alternativeOfTactic env tac then continue
-    let userName : String ←
-      if let some descr := env.find? tac |>.bind (·.value?) then
-        if let some tk ← getFirstTk descr then
-          pure tk.trim
-        else pure tac.toString
-      else pure tac.toString
-
-    docs := docs.push {
-      internalName := tac,
-      userName := userName,
-      tags := tacTags.findD tac {},
-      docString := ← findDocString? env tac,
-      extensionDocs := getTacticExtensions env tac
-    }
-  return docs

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -22,15 +22,12 @@ Runs a term elaborator inside a tactic.
 This function ensures that term elaboration fails when backtracking,
 i.e., in `first| tac term | other`.
 -/
-def runTermElab (k : TermElabM α) (mayPostpone := false) : TacticM α :=
-  -- We disable incrementality here so that nested tactics do not unexpectedly use and affect the
-  -- incrementality state of a calling incrementality-enabled tactic.
-  Term.withoutTacticIncrementality true do
-    /- If error recovery is disabled, we disable `Term.withoutErrToSorry` -/
-    if (← read).recover then
-      go
-    else
-      Term.withoutErrToSorry go
+def runTermElab (k : TermElabM α) (mayPostpone := false) : TacticM α := do
+  /- If error recovery is disabled, we disable `Term.withoutErrToSorry` -/
+  if (← read).recover then
+    go
+  else
+    Term.withoutErrToSorry go
 where
   go := k <* Term.synthesizeSyntheticMVars (postpone := .ofBool mayPostpone)
 

src/Lean/Elab/Term.lean

@@ -1259,8 +1259,8 @@ private def isNoImplicitLambda (stx : Syntax) : Bool :=
 
 private def isTypeAscription (stx : Syntax) : Bool :=
   match stx with
-  | `(($_ : $[$_]?)) => true
-  | _                => false
+  | `(($_ : $_)) => true
+  | _            => false
 
 def hasNoImplicitLambdaAnnotation (type : Expr) : Bool :=
   annotation? `noImplicitLambda type |>.isSome

src/Lean/Environment.lean

@@ -244,21 +244,10 @@ inductive KernelException where
 
 namespace Environment
 
-/--
-Type check given declaration and add it to the 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
 
-/--
-Add declaration to kernel without type checking it.
-**WARNING** This function is meant for temporarily working around kernel performance issues.
-It compromises soundness because, for example, a buggy tactic may produce an invalid proof,
-and the kernel will not catch it if the new option is set to true.
--/
-@[extern "lean_add_decl_without_checking"]
-opaque addDeclWithoutChecking (env : Environment) (decl : @& Declaration) : Except KernelException Environment
-
 end Environment
 
 namespace ConstantInfo

src/Lean/Meta/AbstractMVars.lean

@@ -7,6 +7,13 @@ prelude
 import Lean.Meta.Basic
 
 namespace Lean.Meta
+
+structure AbstractMVarsResult where
+  paramNames : Array Name
+  numMVars   : Nat
+  expr       : Expr
+  deriving Inhabited, BEq
+
 namespace AbstractMVars
 
 structure State where

src/Lean/Meta/Basic.lean

@@ -222,14 +222,7 @@ structure SynthInstanceCacheKey where
   synthPendingDepth : Nat
   deriving Hashable, BEq
 
-/-- Resulting type for `abstractMVars` -/
-structure AbstractMVarsResult where
-  paramNames : Array Name
-  numMVars   : Nat
-  expr       : Expr
-  deriving Inhabited, BEq
-
-abbrev SynthInstanceCache := PersistentHashMap SynthInstanceCacheKey (Option AbstractMVarsResult)
+abbrev SynthInstanceCache := PersistentHashMap SynthInstanceCacheKey (Option Expr)
 
 abbrev InferTypeCache := PersistentExprStructMap Expr
 abbrev FunInfoCache   := PersistentHashMap InfoCacheKey FunInfo

src/Lean/Meta/Constructions.lean

@@ -8,17 +8,26 @@ import Lean.AuxRecursor
 import Lean.AddDecl
 import Lean.Meta.AppBuilder
 import Lean.Meta.CompletionName
-import Lean.Meta.Constructions.RecOn
-import Lean.Meta.Constructions.BRecOn
 
 namespace Lean
 
+@[extern "lean_mk_rec_on"] opaque mkRecOnImp (env : Environment) (declName : @& Name) : Except KernelException Declaration
 @[extern "lean_mk_cases_on"] opaque mkCasesOnImp (env : Environment) (declName : @& Name) : Except KernelException Declaration
 @[extern "lean_mk_no_confusion_type"] opaque mkNoConfusionTypeCoreImp (env : Environment) (declName : @& Name) : Except KernelException Declaration
 @[extern "lean_mk_no_confusion"] opaque mkNoConfusionCoreImp (env : Environment) (declName : @& Name) : Except KernelException Declaration
+@[extern "lean_mk_below"] opaque mkBelowImp (env : Environment) (declName : @& Name) (ibelow : Bool) : Except KernelException Declaration
+@[extern "lean_mk_brec_on"] opaque mkBRecOnImp (env : Environment) (declName : @& Name) (ind : Bool) : Except KernelException Declaration
 
 open Meta
 
+def mkRecOn (declName : Name) : MetaM Unit := do
+  let name := mkRecOnName declName
+  let decl ← ofExceptKernelException (mkRecOnImp (← getEnv) declName)
+  addDecl decl
+  setReducibleAttribute name
+  modifyEnv fun env => markAuxRecursor env name
+  modifyEnv fun env => addProtected env name
+
 def mkCasesOn (declName : Name) : MetaM Unit := do
   let name := mkCasesOnName declName
   let decl ← ofExceptKernelException (mkCasesOnImp (← getEnv) declName)
@@ -27,6 +36,52 @@ def mkCasesOn (declName : Name) : MetaM Unit := do
   modifyEnv fun env => markAuxRecursor env name
   modifyEnv fun env => addProtected env name
 
+private def mkBelowOrIBelow (declName : Name) (ibelow : Bool) : MetaM Unit := do
+  let .inductInfo indVal ← getConstInfo declName | return
+  unless indVal.isRec do return
+  if ← isPropFormerType indVal.type then return
+
+  let decl ← ofExceptKernelException (mkBelowImp (← getEnv) declName ibelow)
+  let name := decl.definitionVal!.name
+  addDecl decl
+  setReducibleAttribute name
+  modifyEnv fun env => addToCompletionBlackList env name
+  modifyEnv fun env => addProtected env name
+
+def mkBelow (declName : Name) : MetaM Unit := mkBelowOrIBelow declName true
+def mkIBelow (declName : Name) : MetaM Unit := mkBelowOrIBelow declName false
+
+private def mkBRecOrBInductionOn (declName : Name) (ind : Bool) : MetaM Unit := do
+  let .inductInfo indVal ← getConstInfo declName | return
+  unless indVal.isRec do return
+  if ← isPropFormerType indVal.type then return
+  let .recInfo recInfo ← getConstInfo (mkRecName declName) | return
+  unless recInfo.numMotives = indVal.all.length do
+    /-
+    The mutual declaration containing `declName` contains nested inductive datatypes.
+    We don't support this kind of declaration here yet. We probably never will :)
+    To support it, we will need to generate an auxiliary `below` for each nested inductive
+    type since their default `below` is not good here. For example, at
+    ```
+    inductive Term
+    | var : String -> Term
+    | app : String -> List Term -> Term
+    ```
+    The `List.below` is not useful since it will not allow us to recurse over the nested terms.
+    We need to generate another one using the auxiliary recursor `Term.rec_1` for `List Term`.
+    -/
+    return
+
+  let decl ← ofExceptKernelException (mkBRecOnImp (← getEnv) declName ind)
+  let name := decl.definitionVal!.name
+  addDecl decl
+  setReducibleAttribute name
+  modifyEnv fun env => markAuxRecursor env name
+  modifyEnv fun env => addProtected env name
+
+def mkBRecOn (declName : Name) : MetaM Unit := mkBRecOrBInductionOn declName false
+def mkBInductionOn (declName : Name) : MetaM Unit := mkBRecOrBInductionOn declName true
+
 def mkNoConfusionCore (declName : Name) : MetaM Unit := do
   -- Do not do anything unless can_elim_to_type. TODO: Extract to util
   let .inductInfo indVal ← getConstInfo declName | return
@@ -56,6 +111,7 @@ def mkNoConfusionEnum (enumName : Name) : MetaM Unit := do
     -- `noConfusionEnum` was not defined yet, so we use `mkNoConfusionCore`
     mkNoConfusionCore enumName
 where
+
   mkToCtorIdx : MetaM Unit := do
     let ConstantInfo.inductInfo info ← getConstInfo enumName | unreachable!
     let us := info.levelParams.map mkLevelParam

src/Lean/Meta/Constructions/BRecOn.lean

@@ -1,393 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Joachim Breitner
--/
-prelude
-import Lean.Meta.InferType
-import Lean.AuxRecursor
-import Lean.AddDecl
-import Lean.Meta.CompletionName
-
-namespace Lean
-open Meta
-
-section PProd
-
-/--!
-Helpers to construct types and values of `PProd` and project out of them, set up to use `And`
-instead of `PProd` if the universes allow. Maybe be extracted into a Utils module when useful
-elsewhere.
--/
-
-private def mkPUnit : Level → Expr
-  | .zero => .const ``True []
-  | lvl   => .const ``PUnit [lvl]
-
-private def mkPProd (e1 e2 : Expr) : MetaM Expr := do
-  let lvl1 ← getLevel e1
-  let lvl2 ← getLevel e2
-  if lvl1 matches .zero && lvl2 matches .zero then
-    return mkApp2 (.const `And []) e1 e2
-  else
-    return mkApp2 (.const ``PProd [lvl1, lvl2]) e1 e2
-
-private def mkNProd (lvl : Level) (es : Array Expr) : MetaM Expr :=
-  es.foldrM (init := mkPUnit lvl) mkPProd
-
-private def mkPUnitMk : Level → Expr
-  | .zero => .const ``True.intro []
-  | lvl   => .const ``PUnit.unit [lvl]
-
-private def mkPProdMk (e1 e2 : Expr) : MetaM Expr := do
-  let t1 ← inferType e1
-  let t2 ← inferType e2
-  let lvl1 ← getLevel t1
-  let lvl2 ← getLevel t2
-  if lvl1 matches .zero && lvl2 matches .zero then
-    return mkApp4 (.const ``And.intro []) t1 t2 e1 e2
-  else
-    return mkApp4 (.const ``PProd.mk [lvl1, lvl2]) t1 t2 e1 e2
-
-private def mkNProdMk (lvl : Level) (es : Array Expr) : MetaM Expr :=
-  es.foldrM (init := mkPUnitMk lvl) mkPProdMk
-
-/-- `PProd.fst` or `And.left` (as projections) -/
-private def mkPProdFst (e : Expr) : MetaM Expr := do
-  let t ← whnf (← inferType e)
-  match_expr t with
-  | PProd _ _ => return .proj ``PProd 0 e
-  | And _ _ =>   return .proj ``And 0 e
-  | _ => throwError "Cannot project .1 out of{indentExpr e}\nof type{indentExpr t}"
-
-/-- `PProd.snd` or `And.right` (as projections) -/
-private def mkPProdSnd (e : Expr) : MetaM Expr := do
-  let t ← whnf (← inferType e)
-  match_expr t with
-  | PProd _ _ => return .proj ``PProd 1 e
-  | And _ _ =>   return .proj ``And 1 e
-  | _ => throwError "Cannot project .2 out of{indentExpr e}\nof type{indentExpr t}"
-
-end PProd
-
-/--
-If `minorType` is the type of a minor premies of a recursor, such as
-```
-  (cons : (head : α) → (tail : List α) → (tail_hs : motive tail) → motive (head :: tail))
-```
-of `List.rec`, constructs the corresponding argument to `List.rec` in the construction
-of `.below` definition; in this case
-```
-fun head tail tail_ih =>
-  PProd (PProd (motive tail) tail_ih) PUnit
-```
-of type
-```
-α → List α → Sort (max 1 u_1) → Sort (max 1 u_1)
-```
-The parameter `typeFormers` are the `motive`s.
--/
-private def buildBelowMinorPremise (rlvl : Level) (typeFormers : Array Expr) (minorType : Expr) : MetaM Expr :=
-  forallTelescope minorType fun minor_args _ => do go #[] minor_args.toList
-where
-  ibelow := rlvl matches .zero
-  go (prods : Array Expr) : List Expr → MetaM Expr
-  | [] => mkNProd rlvl prods
-  | arg::args => do
-    let argType ← inferType arg
-    forallTelescope argType fun arg_args arg_type => do
-      if typeFormers.contains arg_type.getAppFn then
-        let name ← arg.fvarId!.getUserName
-        let type' ← forallTelescope argType fun args _ => mkForallFVars args (.sort rlvl)
-        withLocalDeclD name type' fun arg' => do
-          let snd ← mkForallFVars arg_args (mkAppN arg' arg_args)
-          let e' ← mkPProd argType snd
-          mkLambdaFVars #[arg'] (← go (prods.push e') args)
-      else
-        mkLambdaFVars #[arg] (← go prods args)
-
-/--
-Constructs the `.below` or `.ibelow` definition for a inductive predicate.
-
-For example for the `List` type, it constructs,
-```
-@[reducible] protected def List.below.{u_1, u} : {α : Type u} →
-  {motive : List α → Sort u_1} → List α → Sort (max 1 u_1) :=
-fun {α} {motive} t =>
-  List.rec PUnit (fun head tail tail_ih => PProd (PProd (motive tail) tail_ih) PUnit) t
-```
-and
-```
-@[reducible] protected def List.ibelow.{u} : {α : Type u} →
-  {motive : List α → Prop} → List α → Prop :=
-fun {α} {motive} t =>
-  List.rec True (fun head tail tail_ih => (motive tail ∧ tail_ih) ∧ True) t
-```
--/
-private def mkBelowOrIBelow (indName : Name) (ibelow : Bool) : MetaM Unit := do
-  let .inductInfo indVal ← getConstInfo indName | return
-  unless indVal.isRec do return
-  if ← isPropFormerType indVal.type then return
-
-  let recName := mkRecName indName
-  -- The construction follows the type of `ind.rec`
-  let .recInfo recVal ← getConstInfo recName
-    | throwError "{recName} not a .recInfo"
-  let lvl::lvls := recVal.levelParams.map (Level.param ·)
-    | throwError "recursor {recName} has no levelParams"
-  let lvlParam := recVal.levelParams.head!
-  -- universe parameter names of ibelow/below
-  let blvls :=
-    -- For ibelow we instantiate the first universe parameter of `.rec` to `.zero`
-    if ibelow then recVal.levelParams.tail!
-              else recVal.levelParams
-  let .some ilvl ← typeFormerTypeLevel indVal.type
-    | throwError "type {indVal.type} of inductive {indVal.name} not a type former?"
-
-  -- universe level of the resultant type
-  let rlvl : Level :=
-    if ibelow then
-      0
-    else if indVal.isReflexive then
-      if let .max 1 lvl := ilvl then
-        mkLevelMax' (.succ lvl) lvl
-      else
-        mkLevelMax' (.succ lvl) ilvl
-    else
-      mkLevelMax' 1 lvl
-
-  let refType :=
-    if ibelow then
-      recVal.type.instantiateLevelParams [lvlParam] [0]
-    else if indVal.isReflexive then
-      recVal.type.instantiateLevelParams [lvlParam] [lvl.succ]
-    else
-      recVal.type
-
-  let decl ← forallTelescope refType fun refArgs _ => do
-    assert! refArgs.size == indVal.numParams + recVal.numMotives + recVal.numMinors + indVal.numIndices + 1
-    let params      : Array Expr := refArgs[:indVal.numParams]
-    let typeFormers : Array Expr := refArgs[indVal.numParams:indVal.numParams + recVal.numMotives]
-    let minors      : Array Expr := refArgs[indVal.numParams + recVal.numMotives:indVal.numParams + recVal.numMotives + recVal.numMinors]
-    let remaining   : Array Expr := refArgs[indVal.numParams + recVal.numMotives + recVal.numMinors:]
-
-    let mut val := .const recName (rlvl.succ :: lvls)
-    -- add parameters
-    val := mkAppN val params
-    -- add type formers
-    for typeFormer in typeFormers do
-      let arg ← forallTelescope (← inferType typeFormer) fun targs _ =>
-        mkLambdaFVars targs (.sort rlvl)
-      val := .app val arg
-    -- add minor premises
-    for minor in minors do
-      let arg ← buildBelowMinorPremise rlvl typeFormers (← inferType minor)
-      val := .app val arg
-    -- add indices and major premise
-    val := mkAppN val remaining
-
-    -- All paramaters of `.rec` besides the `minors` become parameters of `.below`
-    let below_params := params ++ typeFormers ++ remaining
-    let type ← mkForallFVars below_params (.sort rlvl)
-    val ← mkLambdaFVars below_params val
-
-    let name := if ibelow then mkIBelowName indName else mkBelowName indName
-    mkDefinitionValInferrringUnsafe name blvls type val .abbrev
-
-  addDecl (.defnDecl decl)
-  setReducibleAttribute decl.name
-  modifyEnv fun env => markAuxRecursor env decl.name
-  modifyEnv fun env => addProtected env decl.name
-
-def mkBelow (declName : Name) : MetaM Unit := mkBelowOrIBelow declName true
-def mkIBelow (declName : Name) : MetaM Unit := mkBelowOrIBelow declName false
-
-/--
-If `minorType` is the type of a minor premies of a recursor, such as
-```
-  (cons : (head : α) → (tail : List α) → (tail_hs : motive tail) → motive (head :: tail))
-```
-of `List.rec`, constructs the corresponding argument to `List.rec` in the construction
-of `.brecOn` definition; in this case
-```
-fun head tail tail_ih =>
-  ⟨F_1 (head :: tail) ⟨tail_ih, PUnit.unit⟩, ⟨tail_ih, PUnit.unit⟩⟩
-```
-of type
-```
-(head : α) → (tail : List α) →
-  PProd (motive tail) (List.below tail) →
-  PProd (motive (head :: tail)) (PProd (PProd (motive tail) (List.below tail)) PUnit)
-```
-The parameter `typeFormers` are the `motive`s.
--/
-private def buildBRecOnMinorPremise (rlvl : Level) (typeFormers : Array Expr)
-    (belows : Array Expr) (fs : Array Expr) (minorType : Expr) : MetaM Expr :=
-  forallTelescope minorType fun minor_args minor_type => do
-    let rec go (prods : Array Expr) : List Expr → MetaM Expr
-      | [] => minor_type.withApp fun minor_type_fn minor_type_args => do
-          let b ← mkNProdMk rlvl prods
-          let .some ⟨idx, _⟩ := typeFormers.indexOf? minor_type_fn
-            | throwError m!"Did not find {minor_type} in {typeFormers}"
-          mkPProdMk (mkAppN fs[idx]! (minor_type_args.push b)) b
-      | arg::args => do
-        let argType ← inferType arg
-        forallTelescope argType fun arg_args arg_type => do
-          arg_type.withApp fun arg_type_fn arg_type_args => do
-            if let .some idx := typeFormers.indexOf? arg_type_fn then
-              let name ← arg.fvarId!.getUserName
-              let type' ← mkForallFVars arg_args
-                (← mkPProd arg_type (mkAppN belows[idx]! arg_type_args) )
-              withLocalDeclD name type' fun arg' => do
-                if arg_args.isEmpty then
-                  mkLambdaFVars #[arg'] (← go (prods.push arg') args)
-                else
-                  let r := mkAppN arg' arg_args
-                  let r₁ ← mkLambdaFVars arg_args (← mkPProdFst r)
-                  let r₂ ← mkLambdaFVars arg_args (← mkPProdSnd r)
-                  let r ← mkPProdMk r₁ r₂
-                  mkLambdaFVars #[arg'] (← go (prods.push r) args)
-            else
-              mkLambdaFVars #[arg] (← go prods args)
-    go #[] minor_args.toList
-
-/--
-Constructs the `.brecon` or `.binductionon` definition for a inductive predicate.
-
-For example for the `List` type, it constructs,
-```
-@[reducible] protected def List.brecOn.{u_1, u} : {α : Type u} → {motive : List α → Sort u_1} →
-  (t : List α) → ((t : List α) → List.below t → motive t) → motive t :=
-fun {α} {motive} t (F_1 : (t : List α) → List.below t → motive t) => (
-  @List.rec α (fun t => PProd (motive t) (@List.below α motive t))
-    ⟨F_1 [] PUnit.unit, PUnit.unit⟩
-    (fun head tail tail_ih => ⟨F_1 (head :: tail) ⟨tail_ih, PUnit.unit⟩, ⟨tail_ih, PUnit.unit⟩⟩)
-    t
-  ).1
-```
-and
-```
-@[reducible] protected def List.binductionOn.{u} : ∀ {α : Type u} {motive : List α → Prop}
-  (t : List α), (∀ (t : List α), List.ibelow t → motive t) → motive t :=
-fun {α} {motive} t F_1 => (
-  @List.rec α (fun t => And (motive t) (@List.ibelow α motive t))
-    ⟨F_1 [] True.intro, True.intro⟩
-    (fun head tail tail_ih => ⟨F_1 (head :: tail) ⟨tail_ih, True.intro⟩, ⟨tail_ih, True.intro⟩⟩)
-    t
-  ).1
-```
--/
-def mkBRecOnOrBInductionOn (indName : Name) (ind : Bool) : MetaM Unit := do
-  let .inductInfo indVal ← getConstInfo indName | return
-  unless indVal.isRec do return
-  if ← isPropFormerType indVal.type then return
-  let recName := mkRecName indName
-  let .recInfo recVal ← getConstInfo recName | return
-  unless recVal.numMotives = indVal.all.length do
-    /-
-    The mutual declaration containing `declName` contains nested inductive datatypes.
-    We don't support this kind of declaration here yet. We probably never will :)
-    To support it, we will need to generate an auxiliary `below` for each nested inductive
-    type since their default `below` is not good here. For example, at
-    ```
-    inductive Term
-    | var : String -> Term
-    | app : String -> List Term -> Term
-    ```
-    The `List.below` is not useful since it will not allow us to recurse over the nested terms.
-    We need to generate another one using the auxiliary recursor `Term.rec_1` for `List Term`.
-    -/
-    return
-
-  let lvl::lvls := recVal.levelParams.map (Level.param ·)
-    | throwError "recursor {recName} has no levelParams"
-  let lvlParam := recVal.levelParams.head!
-  -- universe parameter names of brecOn/binductionOn
-  let blps := if ind then recVal.levelParams.tail!  else recVal.levelParams
-  -- universe arguments of below/ibelow
-  let blvls := if ind then lvls else lvl::lvls
-
-  let .some ⟨idx, _⟩ := indVal.all.toArray.indexOf? indName
-    | throwError m!"Did not find {indName} in {indVal.all}"
-
-  let .some ilvl ← typeFormerTypeLevel indVal.type
-    | throwError "type {indVal.type} of inductive {indVal.name} not a type former?"
-  -- universe level of the resultant type
-  let rlvl : Level :=
-    if ind then
-      0
-    else if indVal.isReflexive then
-      if let .max 1 lvl := ilvl then
-        mkLevelMax' (.succ lvl) lvl
-      else
-        mkLevelMax' (.succ lvl) ilvl
-    else
-      mkLevelMax' 1 lvl
-
-  let refType :=
-    if ind then
-      recVal.type.instantiateLevelParams [lvlParam] [0]
-    else if indVal.isReflexive then
-      recVal.type.instantiateLevelParams [lvlParam] [lvl.succ]
-    else
-      recVal.type
-
-  let decl ← forallTelescope refType fun refArgs _ => do
-    assert! refArgs.size == indVal.numParams + recVal.numMotives + recVal.numMinors + indVal.numIndices + 1
-    let params      : Array Expr := refArgs[:indVal.numParams]
-    let typeFormers : Array Expr := refArgs[indVal.numParams:indVal.numParams + recVal.numMotives]
-    let minors      : Array Expr := refArgs[indVal.numParams + recVal.numMotives:indVal.numParams + recVal.numMotives + recVal.numMinors]
-    let remaining   : Array Expr := refArgs[indVal.numParams + recVal.numMotives + recVal.numMinors:]
-
-    -- One `below` for each type former (same parameters)
-    let belows := indVal.all.toArray.map fun n =>
-      let belowName := if ind then mkIBelowName n else mkBelowName n
-      mkAppN (.const belowName blvls) (params ++ typeFormers)
-
-    -- create types of functionals (one for each type former)
-    --   (F_1 : (t : List α) → (f : List.below t) → motive t)
-    -- and bring parameters of that type into scope
-    let mut fDecls : Array (Name × (Array Expr -> MetaM Expr)) := #[]
-    for typeFormer in typeFormers, below in belows, i in [:typeFormers.size] do
-      let fType ← forallTelescope (← inferType typeFormer) fun targs _ => do
-        withLocalDeclD `f (mkAppN below targs) fun f =>
-          mkForallFVars (targs.push f) (mkAppN typeFormer targs)
-      let fName := .mkSimple s!"F_{i + 1}"
-      fDecls := fDecls.push (fName, fun _ => pure fType)
-    withLocalDeclsD fDecls fun fs => do
-      let mut val := .const recName (rlvl :: lvls)
-      -- add parameters
-      val := mkAppN val params
-      -- add type formers
-      for typeFormer in typeFormers, below in belows do
-        -- example: (motive := fun t => PProd (motive t) (@List.below α motive t))
-        let arg ← forallTelescope (← inferType typeFormer) fun targs _ => do
-          let cType := mkAppN typeFormer targs
-          let belowType := mkAppN below targs
-          let arg ← mkPProd cType belowType
-          mkLambdaFVars targs arg
-        val := .app val arg
-      -- add minor premises
-      for minor in minors do
-        let arg ← buildBRecOnMinorPremise rlvl typeFormers belows fs (← inferType minor)
-        val := .app val arg
-      -- add indices and major premise
-      val := mkAppN val remaining
-      -- project out first component
-      val ← mkPProdFst val
-
-      -- All paramaters of `.rec` besides the `minors` become parameters of `.bRecOn`, and the `fs`
-      let below_params := params ++ typeFormers ++ remaining ++ fs
-      let type ← mkForallFVars below_params (mkAppN typeFormers[idx]! remaining)
-      val ← mkLambdaFVars below_params val
-
-      let name := if ind then mkBInductionOnName indName else mkBRecOnName indName
-      mkDefinitionValInferrringUnsafe name blps type val .abbrev
-
-  addDecl (.defnDecl decl)
-  setReducibleAttribute decl.name
-  modifyEnv fun env => markAuxRecursor env decl.name
-  modifyEnv fun env => addProtected env decl.name
-
-def mkBRecOn (declName : Name) : MetaM Unit := mkBRecOnOrBInductionOn declName false
-def mkBInductionOn (declName : Name) : MetaM Unit := mkBRecOnOrBInductionOn declName true

src/Lean/Meta/Constructions/RecOn.lean

@@ -1,35 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Joachim Breitner
--/
-prelude
-import Lean.Meta.InferType
-import Lean.AuxRecursor
-import Lean.AddDecl
-import Lean.Meta.CompletionName
-
-open Lean Meta
-
-def mkRecOn (n : Name) : MetaM Unit := do
-  let .recInfo recInfo ← getConstInfo (mkRecName n)
-    | throwError "{mkRecName n} not a recinfo"
-  let decl ← forallTelescope recInfo.type fun xs t => do
-    let e := .const recInfo.name (recInfo.levelParams.map (.param ·))
-    let e := mkAppN e xs
-    -- We reorder the parameters
-    -- before: As Cs minor_premises indices major-premise
-    -- fow:    As Cs indices major-premise minor-premises
-    let AC_size := xs.size - recInfo.numMinors - recInfo.numIndices - 1
-    let vs :=
-      xs[:AC_size] ++
-      xs[AC_size + recInfo.numMinors:AC_size + recInfo.numMinors + 1 + recInfo.numIndices] ++
-      xs[AC_size:AC_size + recInfo.numMinors]
-    let type ← mkForallFVars vs t
-    let value ← mkLambdaFVars vs e
-    mkDefinitionValInferrringUnsafe (mkRecOnName n) recInfo.levelParams type value .abbrev
-
-  addDecl (.defnDecl decl)
-  setReducibleAttribute decl.name
-  modifyEnv fun env => markAuxRecursor env decl.name
-  modifyEnv fun env => addProtected env decl.name

src/Lean/Meta/IndPredBelow.lean

@@ -434,7 +434,7 @@ partial def mkBelowMatcher
   withExistingLocalDecls (lhss.foldl (init := []) fun s v => s ++ v.fvarDecls) do
     for lhs in lhss do
       trace[Meta.IndPredBelow.match] "{lhs.patterns.map (·.toMessageData)}"
-  let res ← Match.mkMatcher (exceptionIfContainsSorry := true) { matcherName, matchType, discrInfos := mkArray (mkMatcherInput.numDiscrs + 1) {}, lhss }
+  let res ← Match.mkMatcher { matcherName, matchType, discrInfos := mkArray (mkMatcherInput.numDiscrs + 1) {}, lhss }
   res.addMatcher
   -- if a wrong index is picked, the resulting matcher can be type-incorrect.
   -- we check here, so that errors can propagate higher up the call stack.

src/Lean/Meta/Match/Match.lean

@@ -830,12 +830,8 @@ Each `AltLHS` has a list of local declarations and a list of patterns.
 The number of patterns must be the same in each `AltLHS`.
 The generated matcher has the structure described at `MatcherInfo`. The motive argument is of the form
 `(motive : (a_1 : A_1) -> (a_2 : A_2[a_1]) -> ... -> (a_n : A_n[a_1, a_2, ... a_{n-1}]) -> Sort v)`
-where `v` is a universe parameter or 0 if `B[a_1, ..., a_n]` is a proposition.
-
-If `exceptionIfContainsSorry := true`, then `mkMatcher` throws an exception if the auxiliary
-declarations contains a `sorry`. We use this argument to workaround a bug at `IndPredBelow.mkBelowMatcher`.
--/
-def mkMatcher (input : MkMatcherInput) (exceptionIfContainsSorry := false) : MetaM MatcherResult := withCleanLCtxFor input do
+where `v` is a universe parameter or 0 if `B[a_1, ..., a_n]` is a proposition. -/
+def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := withCleanLCtxFor input do
   let ⟨matcherName, matchType, discrInfos, lhss⟩ := input
   let numDiscrs := discrInfos.size
   let numEqs := getNumEqsFromDiscrInfos discrInfos
@@ -848,11 +844,6 @@ def mkMatcher (input : MkMatcherInput) (exceptionIfContainsSorry := false) : Met
   let uElim ← getLevel matchTypeBody
   let uElimGen ← if uElim == levelZero then pure levelZero else mkFreshLevelMVar
   let mkMatcher (type val : Expr) (minors : Array (Expr × Nat)) (s : State) : MetaM MatcherResult := do
-    let val ← instantiateMVars val
-    let type ← instantiateMVars type
-    if exceptionIfContainsSorry then
-      if type.hasSorry || val.hasSorry then
-        throwError "failed to create auxiliary match declaration `{matcherName}`, it contains `sorry`"
     trace[Meta.Match.debug] "matcher value: {val}\ntype: {type}"
     trace[Meta.Match.debug] "minors num params: {minors.map (·.2)}"
     /- The option `bootstrap.gen_matcher_code` is a helper hack. It is useful, for example,
@@ -866,6 +857,7 @@ def mkMatcher (input : MkMatcherInput) (exceptionIfContainsSorry := false) : Met
        | negSucc n => succ n
        ```
        which is defined **before** `Int.decLt` -/
+
     let (matcher, addMatcher) ← mkMatcherAuxDefinition matcherName type val
     trace[Meta.Match.debug] "matcher levels: {matcher.getAppFn.constLevels!}, uElim: {uElimGen}"
     let uElimPos? ← getUElimPos? matcher.getAppFn.constLevels! uElimGen

src/Lean/Meta/SynthInstance.lean

@@ -698,83 +698,6 @@ private def preprocessOutParam (type : Expr) : MetaM Expr :=
   Remark: we use a different option for controlling the maximum result size for coercions.
 -/
 
-private def assignOutParams (type : Expr) (result : Expr) : MetaM Bool := do
-  let resultType ← inferType result
-  /- Output parameters of local instances may be marked as `syntheticOpaque` by the application-elaborator.
-      We use `withAssignableSyntheticOpaque` to make sure this kind of parameter can be assigned by the following `isDefEq`.
-      TODO: rewrite this check to avoid `withAssignableSyntheticOpaque`. -/
-  let defEq ← withDefault <| withAssignableSyntheticOpaque <| isDefEq type resultType
-  unless defEq do
-    trace[Meta.synthInstance] "{crossEmoji} result type{indentExpr resultType}\nis not definitionally equal to{indentExpr type}"
-  return defEq
-
-/--
-Auxiliary function for converting the `AbstractMVarsResult` returned by `SynthIntance.main` into an `Expr`.
--/
-private def applyAbstractResult? (type : Expr) (abstResult? : Option AbstractMVarsResult) : MetaM (Option Expr) := do
-  let some abstResult := abstResult? | return none
-  let (_, _, result) ← openAbstractMVarsResult abstResult
-  unless (← assignOutParams type result) do return none
-  let result ← instantiateMVars result
-  /- We use `check` to propagate universe constraints implied by the `result`.
-      Recall that we use `allowLevelAssignments := true` which allows universe metavariables in the current depth to be assigned,
-      but these assignments are discarded by `withNewMCtxDepth`.
-
-      TODO: If this `check` is a performance bottleneck, we can improve performance by tracking whether
-            a universe metavariable from previous universe levels have been assigned or not during TC resolution.
-            We only need to perform the `check` if this kind of assignment have been performed.
-
-      The example in the issue #796 exposed this issue.
-      ```
-      structure A
-      class B (a : outParam A) (α : Sort u)
-      class C {a : A} (α : Sort u) [B a α]
-      class D {a : A} (α : Sort u) [B a α] [c : C α]
-      class E (a : A) where [c (α : Sort u) [B a α] : C α]
-      instance c {a : A} [e : E a] (α : Sort u) [B a α] : C α := e.c α
-
-      def d {a : A} [e : E a] (α : Sort u) [b : B a α] : D α := ⟨⟩
-      ```
-      The term `D α` has two instance implicit arguments. The second one has type `C α`, and TC
-      resolution produces the result `@c.{u} a e α b`.
-      Note that the `e` has type `E.{?v} a`, and `E` is universe polymorphic,
-      but the universe does not occur in the parameter `a`. We have that `?v := u` is implied by `@c.{u} a e α b`,
-      but this assignment is lost.
-  -/
-  check result
-  return some result
-
-/--
-Auxiliary function for converting a cached `AbstractMVarsResult` returned by `SynthIntance.main` into an `Expr`.
-This function tries to avoid the potentially expensive `check` at `applyCachedAbstractResult?`.
--/
-private def applyCachedAbstractResult? (type : Expr) (abstResult? : Option AbstractMVarsResult) : MetaM (Option Expr) := do
-  let some abstResult := abstResult? | return none
-  if abstResult.numMVars == 0 && abstResult.paramNames.isEmpty then
-    /-
-    Result does not instroduce new metavariables, thus we don't need to perform (again)
-    the `check` at `applyAbstractResult?`.
-    This is an optimization.
-    -/
-    unless (← assignOutParams type abstResult.expr) do
-      return none
-    return some abstResult.expr
-  else
-    applyAbstractResult? type abstResult?
-
-/-- Helper function for caching synthesized type class instances. -/
-private def cacheResult (cacheKey : SynthInstanceCacheKey) (abstResult? : Option AbstractMVarsResult) (result? : Option Expr) : MetaM Unit := do
-  match result? with
-  | none => modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey none }
-  | some result =>
-    let some abstResult := abstResult? | return ()
-    if abstResult.numMVars == 0 && abstResult.paramNames.isEmpty then
-      -- See `applyCachedAbstractResult?` If new metavariables have **not** been introduced,
-      -- we don't need to perform extra checks again when reusing result.
-      modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey (some { expr := result, paramNames := #[], numMVars := 0 }) }
-    else
-      modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey (some abstResult) }
-
 def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do profileitM Exception "typeclass inference" (← getOptions) (decl := type.getAppFn.constName?.getD .anonymous) do
   let opts ← getOptions
   let maxResultSize := maxResultSize?.getD (synthInstance.maxSize.get opts)
@@ -786,20 +709,66 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
     let localInsts ← getLocalInstances
     let type ← instantiateMVars type
     let type ← preprocess type
+    let s ← get
+    let rec assignOutParams (result : Expr) : MetaM Bool := do
+      let resultType ← inferType result
+      /- Output parameters of local instances may be marked as `syntheticOpaque` by the application-elaborator.
+         We use `withAssignableSyntheticOpaque` to make sure this kind of parameter can be assigned by the following `isDefEq`.
+         TODO: rewrite this check to avoid `withAssignableSyntheticOpaque`. -/
+      let defEq ← withDefault <| withAssignableSyntheticOpaque <| isDefEq type resultType
+      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 (← get).cache.synthInstance.find? cacheKey with
-    | some abstResult? =>
-      let result? ← applyCachedAbstractResult? type abstResult?
-      trace[Meta.synthInstance] "result {result?} (cached)"
-      return result?
-    | none =>
-      let abstResult? ← withNewMCtxDepth (allowLevelAssignments := true) do
+    match s.cache.synthInstance.find? cacheKey with
+    | some result =>
+      trace[Meta.synthInstance] "result {result} (cached)"
+      if let some inst := result then
+        unless (← assignOutParams inst) do
+          return none
+      pure result
+    | none        =>
+      let result? ← withNewMCtxDepth (allowLevelAssignments := true) do
         let normType ← preprocessOutParam type
         SynthInstance.main normType maxResultSize
-      let result? ← applyAbstractResult? type abstResult?
-      trace[Meta.synthInstance] "result {result?}"
-      cacheResult cacheKey abstResult? result?
-      return result?
+      let result? ← match result? with
+        | none        => pure none
+        | some result => do
+          let (_, _, result) ← openAbstractMVarsResult result
+          trace[Meta.synthInstance] "result {result}"
+          if (← assignOutParams result) then
+            let result ← instantiateMVars result
+            /- We use `check` to propagate universe constraints implied by the `result`.
+               Recall that we use `allowLevelAssignments := true` which allows universe metavariables in the current depth to be assigned,
+               but these assignments are discarded by `withNewMCtxDepth`.
+
+               TODO: If this `check` is a performance bottleneck, we can improve performance by tracking whether
+                     a universe metavariable from previous universe levels have been assigned or not during TC resolution.
+                     We only need to perform the `check` if this kind of assignment have been performed.
+
+               The example in the issue #796 exposed this issue.
+               ```
+                structure A
+                class B (a : outParam A) (α : Sort u)
+                class C {a : A} (α : Sort u) [B a α]
+                class D {a : A} (α : Sort u) [B a α] [c : C α]
+                class E (a : A) where [c (α : Sort u) [B a α] : C α]
+                instance c {a : A} [e : E a] (α : Sort u) [B a α] : C α := e.c α
+
+                def d {a : A} [e : E a] (α : Sort u) [b : B a α] : D α := ⟨⟩
+               ```
+               The term `D α` has two instance implicit arguments. The second one has type `C α`, and TC
+               resolution produces the result `@c.{u} a e α b`.
+               Note that the `e` has type `E.{?v} a`, and `E` is universe polymorphic,
+               but the universe does not occur in the parameter `a`. We have that `?v := u` is implied by `@c.{u} a e α b`,
+               but this assignment is lost.
+            -/
+            check result
+            pure (some result)
+          else
+            pure none
+      modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey result? }
+      pure result?
 
 /--
   Return `LOption.some r` if succeeded, `LOption.none` if it failed, and `LOption.undef` if

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

@@ -123,14 +123,7 @@ private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInf
           return none
         pure <| some proof
       let rhs := (← instantiateMVars type).appArg!
-      /-
-      We used to use `e == rhs` in the following test.
-      However, it include unnecessary proof steps when `e` and `rhs`
-      are equal after metavariables are instantiated.
-      We are hoping the following `instantiateMVars` should not be too expensive since
-      we seldom have assigned metavariables in goals.
-      -/
-      if (← instantiateMVars e) == rhs then
+      if e == rhs then
         return none
       if thm.perm then
         /-

src/Lean/Parser.lean

@@ -12,7 +12,6 @@ import Lean.Parser.Command
 import Lean.Parser.Module
 import Lean.Parser.Syntax
 import Lean.Parser.Do
-import Lean.Parser.Tactic.Doc
 
 namespace Lean
 namespace Parser

src/Lean/Parser/Attr.lean

@@ -50,24 +50,6 @@ def externEntry := leading_parser
 @[builtin_attr_parser] def extern     := leading_parser
   nonReservedSymbol "extern" >> optional (ppSpace >> numLit) >> many (ppSpace >> externEntry)
 
-/--
-Declare this tactic to be an alias or alternative form of an existing tactic.
-
-This has the following effects:
- * The alias relationship is saved
- * The docstring is taken from the original tactic, if present
--/
-@[builtin_attr_parser] def «tactic_alt» := leading_parser
-  "tactic_alt" >> ppSpace >> ident
-
-/--
-Add one or more tags to a tactic.
-
-Tags should be applied to the canonical names for tactics.
--/
-@[builtin_attr_parser] def «tactic_tag» := leading_parser
-  "tactic_tag" >> many1 (ppSpace >> ident)
-
 end Attr
 
 end Lean.Parser

src/Lean/Parser/Command.lean

@@ -447,11 +447,6 @@ structure Pair (α : Type u) (β : Type v) : Type (max u v) where
   "#print " >> nonReservedSymbol "axioms " >> ident
 @[builtin_command_parser] def printEqns      := leading_parser
   "#print " >> (nonReservedSymbol "equations " <|> nonReservedSymbol "eqns ") >> ident
-/--
-Displays all available tactic tags, with documentation.
--/
-@[builtin_command_parser] def printTacTags   := leading_parser
-  "#print " >> nonReservedSymbol "tactic " >> nonReservedSymbol "tags"
 @[builtin_command_parser] def «init_quot»    := leading_parser
   "init_quot"
 def optionValue := nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit
@@ -674,26 +669,6 @@ Documentation can only be added to declarations in the same module.
 @[builtin_command_parser] def addDocString := leading_parser
   docComment >> "add_decl_doc " >> ident
 
-/--
-Register a tactic tag, saving its user-facing name and docstring.
-
-Tactic tags can be used by documentation generation tools to classify related tactics.
--/
-@[builtin_command_parser] def «register_tactic_tag» := leading_parser
-  optional (docComment >> ppLine) >>
-  "register_tactic_tag " >> ident >> strLit
-
-/--
-Add more documentation as an extension of the documentation for a given tactic.
-
-The extended documentation is placed in the command's docstring. It is shown as part of a bulleted
-list, so it should be brief.
--/
-@[builtin_command_parser] def «tactic_extension» := leading_parser
-  optional (docComment >> ppLine) >>
-  "tactic_extension " >> ident
-
-
 /--
   This is an auxiliary command for generation constructor injectivity theorems for
   inductive types defined at `Prelude.lean`.

src/Lean/Parser/Tactic.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import Lean.Parser.Term
-import Lean.Parser.Tactic.Doc
 
 namespace Lean
 namespace Parser

src/Lean/Parser/Tactic/Doc.lean

@@ -1,290 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: David Thrane Christiansen
--/
-prelude
-import Lean.Attributes
-import Lean.DocString.Extension
-import Lean.Elab.InfoTree.Main
-import Lean.Parser.Attr
-import Lean.Parser.Extension
-
-set_option linter.missingDocs true
-
-namespace Lean.Parser.Tactic.Doc
-
-open Lean.Parser (registerParserAttributeHook)
-open Lean.Parser.Attr
-
-/-- Check whether a name is a tactic syntax kind -/
-def isTactic (env : Environment) (kind : Name) : Bool := Id.run do
-  let some tactics := (Lean.Parser.parserExtension.getState env).categories.find? `tactic
-    | return false
-  for (tac, _) in tactics.kinds do
-    if kind == tac then return true
-  return false
-
-/--
-Stores a collection of *tactic alternatives*, to track which new syntax rules represent new forms of
-existing tactics.
--/
-builtin_initialize tacticAlternativeExt
-    : PersistentEnvExtension (Name × Name) (Name × Name) (NameMap Name) ←
-  registerPersistentEnvExtension {
-    mkInitial := pure {},
-    addImportedFn := fun _ => pure {},
-    addEntryFn := fun as (src, tgt) => as.insert src tgt,
-    exportEntriesFn := fun es =>
-      es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
-  }
-
-/--
-If `tac` is registered as the alternative form of another tactic, then return the canonical name for
-it.
--/
-def alternativeOfTactic (env : Environment) (tac : Name) : Option Name :=
-  match env.getModuleIdxFor? tac with
-  | some modIdx =>
-    match (tacticAlternativeExt.getModuleEntries env modIdx).binSearch (tac, .anonymous) (Name.quickLt ·.1 ·.1) with
-    | some (_, val) => some val
-    | none => none
-  | none => tacticAlternativeExt.getState env |>.find? tac
-
-/--
-Find all alternatives for a given canonical tactic name.
--/
-def aliases [Monad m] [MonadEnv m] (tac : Name) : m NameSet := do
-  let env ← getEnv
-  let mut found := {}
-  for (src, tgt) in tacticAlternativeExt.getState env do
-    if tgt == tac then found := found.insert src
-  for arr in tacticAlternativeExt.toEnvExtension.getState env |>.importedEntries do
-    for (src, tgt) in arr do
-      if tgt == tac then found := found.insert src
-  pure found
-
-builtin_initialize
-  let name := `tactic_alt
-  registerBuiltinAttribute {
-    name := name,
-    ref := by exact decl_name%,
-    add := fun decl stx kind => do
-      unless kind == AttributeKind.global do throwError "invalid attribute '{name}', must be global"
-      unless ((← getEnv).getModuleIdxFor? decl).isNone do
-        throwError "invalid attribute '{name}', declaration is in an imported module"
-      let `(«tactic_alt»|tactic_alt $tgt) := stx
-        | throwError "invalid syntax for '{name}' attribute"
-
-      let tgtName ← Lean.Elab.realizeGlobalConstNoOverloadWithInfo tgt
-
-      if !(isTactic (← getEnv) tgtName) then throwErrorAt tgt "'{tgtName}' is not a tactic"
-      -- If this condition is true, then we're in an `attribute` command and can validate here.
-      if (← getEnv).find? decl |>.isSome then
-        if !(isTactic (← getEnv) decl) then throwError "'{decl}' is not a tactic"
-
-      if let some tgt' := alternativeOfTactic (← getEnv) tgtName then
-        throwError "'{tgtName}' is itself an alternative for '{tgt'}'"
-      modifyEnv fun env => tacticAlternativeExt.addEntry env (decl, tgtName)
-      if (← findSimpleDocString? (← getEnv) decl).isSome then
-        logWarningAt stx m!"Docstring for '{decl}' will be ignored because it is an alternative"
-
-    descr :=
-      "Register a tactic parser as an alternative form of an existing tactic, so they " ++
-      "can be grouped together in documentation.",
-    -- This runs prior to elaboration because it allows a check for whether the decl is present
-    -- in the environment to determine whether we can see if it's a tactic name. This is useful
-    -- when the attribute is applied after definition, using an `attribute` command (error checking
-    -- for the `@[tactic_alt TAC]` syntax is performed by the parser attribute hook). If this
-    -- attribute ran later, then the decl would already be present.
-    applicationTime := .beforeElaboration
-  }
-
-
-/--
-The known tactic tags that allow tactics to be grouped by purpose.
--/
-builtin_initialize knownTacticTagExt
-    : PersistentEnvExtension
-        (Name × String × Option String)
-        (Name × String × Option String)
-        (NameMap (String × Option String)) ←
-  registerPersistentEnvExtension {
-    mkInitial := pure {},
-    addImportedFn := fun _ => pure {},
-    addEntryFn := fun as (src, tgt) => as.insert src tgt,
-    exportEntriesFn := fun es =>
-      es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
-  }
-
-/--
-Get the user-facing name and docstring for a tactic tag.
--/
-def tagInfo [Monad m] [MonadEnv m] (tag : Name) : m (Option (String × Option String)) := do
-  let env ← getEnv
-  match env.getModuleIdxFor? tag with
-  | some modIdx =>
-    match (knownTacticTagExt.getModuleEntries env modIdx).binSearch (tag, default) (Name.quickLt ·.1 ·.1) with
-    | some (_, val) => pure (some val)
-    | none => pure none
-  | none => pure (knownTacticTagExt.getState env |>.find? tag)
-
-/-- Enumerate the tactic tags that are available -/
-def allTags [Monad m] [MonadEnv m] : m (List Name) := do
-  let env ← getEnv
-  let mut found : NameSet := {}
-  for (tag, _) in knownTacticTagExt.getState env do
-    found := found.insert tag
-  for arr in knownTacticTagExt.toEnvExtension.getState env |>.importedEntries do
-    for (tag, _) in arr do
-      found := found.insert tag
-  pure (found.toArray.qsort (·.toString < ·.toString) |>.toList)
-
-/-- Enumerate the tactic tags that are available, with their user-facing name and docstring -/
-def allTagsWithInfo [Monad m] [MonadEnv m] : m (List (Name × String × Option String)) := do
-  let env ← getEnv
-  let mut found : NameMap (String × Option String) := {}
-  for (tag, info) in knownTacticTagExt.getState env do
-    found := found.insert tag info
-  for arr in knownTacticTagExt.toEnvExtension.getState env |>.importedEntries do
-    for (tag, info) in arr do
-      found := found.insert tag info
-  let arr := found.fold (init := #[]) (fun arr k v => arr.push (k, v))
-  pure (arr.qsort (·.1.toString < ·.1.toString) |>.toList)
-
-/--
-The mapping between tags and tactics. Tags may be applied in any module, not just the defining
-module for the tactic.
-
-Because this is expected to be augmented regularly, but queried rarely (only when generating
-documentation indices), it is just stored as flat unsorted arrays of pairs. Before it is used for
-some other purpose, consider a new representation.
-
-The first projection in each pair is the tactic name, and the second is the tag name.
--/
-builtin_initialize tacticTagExt
-    : PersistentEnvExtension (Name × Name) (Name × Name) (NameMap NameSet) ←
-  registerPersistentEnvExtension {
-    mkInitial := pure {},
-    addImportedFn := fun _ => pure {},
-    addEntryFn := fun tags (decl, newTag) => tags.insert decl (tags.findD decl {} |>.insert newTag)
-    exportEntriesFn := fun tags => Id.run do
-      let mut exported := #[]
-      for (decl, dTags) in tags do
-        for t in dTags do
-          exported := exported.push (decl, t)
-      exported
-  }
-
-builtin_initialize
-  let name := `tactic_tag
-  registerBuiltinAttribute {
-    name := name,
-    ref := by exact decl_name%,
-    add := fun decl stx kind => do
-      unless kind == AttributeKind.global do throwError "invalid attribute '{name}', must be global"
-      let `(«tactic_tag»|tactic_tag $tags*) := stx
-        | throwError "invalid '{name}' attribute"
-      if (← getEnv).find? decl |>.isSome then
-        if !(isTactic (← getEnv) decl) then
-          throwErrorAt stx "'{decl}' is not a tactic"
-
-      if let some tgt' := alternativeOfTactic (← getEnv) decl then
-        throwErrorAt stx "'{decl}' is an alternative form of '{tgt'}'"
-
-      for t in tags do
-        let tagName := t.getId
-        if let some _ ← tagInfo tagName then
-          modifyEnv (tacticTagExt.addEntry · (decl, tagName))
-        else
-          let all ← allTags
-          let extra : MessageData :=
-              let count := all.length
-              let name := (m!"'{·}'")
-              let suggestions :=
-                if count == 0 then m!"(no tags defined)"
-                else if count == 1 then
-                  MessageData.joinSep (all.map name) ", "
-                else if count < 10 then
-                  m!"one of " ++ MessageData.joinSep (all.map name) ", "
-                else
-                  m!"one of " ++
-                  MessageData.joinSep (all.take 10 |>.map name) ", " ++ ", ..."
-              m!"(expected {suggestions})"
-
-          throwErrorAt t (m!"unknown tag '{tagName}' " ++ extra)
-    descr := "Register a tactic parser as an alternative of an existing tactic, so they can be " ++
-      "grouped together in documentation.",
-    -- This runs prior to elaboration because it allows a check for whether the decl is present
-    -- in the environment to determine whether we can see if it's a tactic name. This is useful
-    -- when the attribute is applied after definition, using an `attribute` command (error checking
-    -- for the `@[tactic_tag ...]` syntax is performed by the parser attribute hook). If this
-    -- attribute ran later, then the decl would already be present.
-    applicationTime := .beforeElaboration
-  }
-
-/--
-Extensions to tactic documentation.
-
-This provides a structured way to indicate that an extensible tactic has been extended (for
-instance, new cases tried by `trivial`).
--/
-builtin_initialize tacticDocExtExt
-    : PersistentEnvExtension (Name × Array String) (Name × String) (NameMap (Array String)) ←
-  registerPersistentEnvExtension {
-    mkInitial := pure {},
-    addImportedFn := fun _ => pure {},
-    addEntryFn := fun es (x, ext) => es.insert x (es.findD x #[] |>.push ext),
-    exportEntriesFn := fun es =>
-      es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
-  }
-
-/-- Gets the extensions declared for the documentation for the given canonical tactic name -/
-def getTacticExtensions (env : Environment) (tactic : Name) : Array String := Id.run do
-  let mut extensions := #[]
-  -- Extensions may be declared in any module, so they must all be searched
-  for modArr in tacticDocExtExt.toEnvExtension.getState env |>.importedEntries do
-    if let some (_, strs) := modArr.binSearch (tactic, #[]) (Name.quickLt ·.1 ·.1) then
-      extensions := extensions ++ strs
-  if let some strs := tacticDocExtExt.getState env |>.find? tactic then
-    extensions := extensions ++ strs
-  pure extensions
-
-/-- Gets the rendered extensions for the given canonical tactic name -/
-def getTacticExtensionString (env : Environment) (tactic : Name) : String := Id.run do
-  let exts := getTacticExtensions env tactic
-  if exts.size == 0 then ""
-  else "\n\nExtensions:\n\n" ++ String.join (exts.toList.map bullet) |>.trimRight
-where
-  indentLine (str: String) : String :=
-    (if str.all (·.isWhitespace) then str else "   " ++ str) ++ "\n"
-  bullet (str : String) : String :=
-    let lines := str.splitOn "\n"
-    match lines with
-    | [] => ""
-    | [l] => " * " ++ l ++ "\n\n"
-    | l::ls => " * " ++ l ++ "\n" ++ String.join (ls.map indentLine) ++ "\n\n"
-
-
--- Note: this error handler doesn't prevent all cases of non-tactics being added to the data
--- structure. But the module will throw errors during elaboration, and there doesn't seem to be
--- another way to implement this, because the category parser extension attribute runs *after* the
--- attributes specified before a `syntax` command.
-/--
-Validates that a tactic alternative is actually a tactic and that syntax tagged as tactics are
-tactics.
--/
-def tacticDocsOnTactics : ParserAttributeHook where
-  postAdd (catName declName : Name) (_builtIn : Bool) := do
-    if catName == `tactic then
-      return
-    if alternativeOfTactic (← getEnv) declName |>.isSome then
-      throwError m!"'{declName}' is not a tactic"
-    -- It's sufficient to look in the state (and not the imported entries) because this validation
-    -- only needs to check tags added in the current module
-    if let some tags := tacticTagExt.getState (← getEnv) |>.find? declName then
-      if !tags.isEmpty then
-        throwError m!"'{declName}' is not a tactic"
-
-builtin_initialize
-  registerParserAttributeHook tacticDocsOnTactics

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -45,8 +45,6 @@ structure Context where
   depth          : Nat := 0
 
 structure State where
-  /-- The number of `delab` steps so far. Used by `pp.maxSteps` to stop delaboration. -/
-  steps : Nat := 0
   /-- We attach `Elab.Info` at various locations in the `Syntax` output in order to convey
   its semantics. While the elaborator emits `InfoTree`s, here we have no real text location tree
   to traverse, so we use a flattened map. -/
@@ -264,12 +262,10 @@ def withBindingBodyUnusedName {α} (d : Syntax → DelabM α) : DelabM α := do
 inductive OmissionReason
   | deep
   | proof
-  | maxSteps
 
 def OmissionReason.toString : OmissionReason → String
   | deep => "Term omitted due to its depth (see option `pp.deepTerms`)."
   | proof => "Proof omitted (see option `pp.proofs`)."
-  | maxSteps => "Term omitted due to reaching the maximum number of steps allowed for pretty printing this expression (see option `pp.maxSteps`)."
 
 def addOmissionInfo (pos : Pos) (stx : Syntax) (e : Expr) (reason : OmissionReason) : DelabM Unit := do
   let info := Info.ofOmissionInfo <| ← mkOmissionInfo stx e
@@ -365,11 +361,6 @@ partial def delabFor : Name → Delab
 
 partial def delab : Delab := do
   checkSystem "delab"
-
-  if (← get).steps ≥ (← getPPOption getPPMaxSteps) then
-    return ← omission .maxSteps
-  modify fun s => {s with steps := s.steps + 1}
-
   let e ← getExpr
 
   if ← shouldOmitExpr e then

src/Lean/PrettyPrinter/Delaborator/Options.lean

@@ -8,11 +8,6 @@ import Lean.Data.Options
 
 namespace Lean
 
-register_builtin_option pp.maxSteps : Nat := {
-  defValue := 5000
-  group    := "pp"
-  descr    := "(pretty printer) maximum number of expressions to visit, after which terms will pretty print as `⋯`"
-}
 register_builtin_option pp.all : Bool := {
   defValue := false
   group    := "pp"
@@ -167,12 +162,12 @@ register_builtin_option pp.instanceTypes : Bool := {
   descr    := "(pretty printer) when printing explicit applications, show the types of inst-implicit arguments"
 }
 register_builtin_option pp.deepTerms : Bool := {
-  defValue := false
+  defValue := true
   group    := "pp"
   descr    := "(pretty printer) display deeply nested terms, replacing them with `⋯` if set to false"
 }
 register_builtin_option pp.deepTerms.threshold : Nat := {
-  defValue := 50
+  defValue := 20
   group    := "pp"
   descr    := "(pretty printer) when `pp.deepTerms` is false, the depth at which terms start being replaced with `⋯`"
 }
@@ -193,6 +188,16 @@ register_builtin_option pp.motives.all : Bool := {
 }
 -- TODO:
 /-
+register_builtin_option g_pp_max_depth : Nat := {
+  defValue := false
+  group    := "pp"
+  descr    := "(pretty printer) maximum expression depth, after that it will use ellipsis"
+}
+register_builtin_option g_pp_max_steps : Nat := {
+  defValue := false
+  group    := "pp"
+  descr    := "(pretty printer) maximum number of visited expressions, after that it will use ellipsis"
+}
 register_builtin_option g_pp_locals_full_names : Bool := {
   defValue := false
   group    := "pp"
@@ -220,7 +225,6 @@ register_builtin_option g_pp_compact_let : Bool := {
 }
 -/
 
-def getPPMaxSteps (o : Options) : Nat := o.get pp.maxSteps.name pp.maxSteps.defValue
 def getPPAll (o : Options) : Bool := o.get pp.all.name false
 def getPPFunBinderTypes (o : Options) : Bool := o.get pp.funBinderTypes.name (getPPAll o)
 def getPPPiBinderTypes (o : Options) : Bool := o.get pp.piBinderTypes.name pp.piBinderTypes.defValue

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -10,8 +10,6 @@ import Lean.DeclarationRange
 import Lean.Data.Json
 import Lean.Data.Lsp
 
-import Lean.Parser.Tactic.Doc
-
 import Lean.Server.FileWorker.Utils
 import Lean.Server.Requests
 import Lean.Server.Completion
@@ -26,8 +24,6 @@ open Lsp
 open RequestM
 open Snapshots
 
-open Lean.Parser.Tactic.Doc (alternativeOfTactic getTacticExtensionString)
-
 def handleCompletion (p : CompletionParams)
     : RequestM (RequestTask CompletionList) := do
   let doc ← readDoc
@@ -89,8 +85,7 @@ def handleHover (p : HoverParams)
       let stxDoc? ← match stack? with
         | some stack => stack.findSomeM? fun (stx, _) => do
           let .node _ kind _ := stx | pure none
-          let docStr ← findDocString? snap.env kind
-          return docStr.map (·, stx.getRange?.get!)
+          return (← findDocString? snap.env kind).map (·, stx.getRange?.get!)
         | none => pure none
 
       -- now try info tree

src/Lean/Server/InfoUtils.lean

@@ -5,14 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Wojciech Nawrocki
 -/
 prelude
-import Lean.DocString
 import Lean.PrettyPrinter
-import Lean.Parser.Tactic.Doc
 
 namespace Lean.Elab
 
-open Lean.Parser.Tactic.Doc (alternativeOfTactic getTacticExtensionString)
-
 /-- Elaborator information with elaborator context.
 
 It can be thought of as a "thunked" elaboration computation that allows us
@@ -248,7 +244,7 @@ def Info.docString? (i : Info) : MetaM (Option String) := do
   match i with
   | .ofTermInfo ti =>
     if let some n := ti.expr.constName? then
-      return (← findDocString? env n)
+      return ← findDocString? env n
   | .ofFieldInfo fi => return ← findDocString? env fi.projName
   | .ofOptionInfo oi =>
     if let some doc ← findDocString? env oi.declName then
@@ -262,7 +258,6 @@ def Info.docString? (i : Info) : MetaM (Option String) := do
     return ← findDocString? env ei.stx.getKind <||> findDocString? env ei.elaborator
   return none
 
-
 /-- Construct a hover popup, if any, from an info node in a context.-/
 def Info.fmtHover? (ci : ContextInfo) (i : Info) : IO (Option FormatWithInfos) := do
   ci.runMetaM i.lctx do

src/Leanc.lean

@@ -8,15 +8,10 @@ import Lean.Compiler.FFI
 open Lean.Compiler.FFI
 
 def main (args : List String) : IO UInt32 := do
-  let root ← match (← IO.getEnv "LEAN_SYSROOT") with
-    | some root => pure <| System.FilePath.mk root
-    | none      => pure <| (← IO.appDir).parent.get!
-  let mut cc := "@LEANC_CC@".replace "ROOT" root.toString
-
   if args.isEmpty then
-    IO.println s!"Lean C compiler
+    IO.println "Lean C compiler
 
-A simple wrapper around a C compiler. Defaults to `{cc}`,
+A simple wrapper around a C compiler. Defaults to `@LEANC_CC@`,
 which can be overridden with the environment variable `LEAN_CC`. All parameters are passed
 as-is to the wrapped compiler.
 
@@ -25,6 +20,11 @@ Interesting options:
 * `--print-ldflags`: print C compiler flags necessary for statically linking against the Lean library and exit"
     return 1
 
+  let root ← match (← IO.getEnv "LEAN_SYSROOT") with
+    | some root => pure <| System.FilePath.mk root
+    | none      => pure <| (← IO.appDir).parent.get!
+  let rootify s := s.replace "ROOT" root.toString
+
   -- It is difficult to identify the correct minor version here, leading to linking warnings like:
   -- `ld64.lld: warning: /usr/lib/system/libsystem_kernel.dylib has version 13.5.0, which is newer than target minimum of 13.0.0`
   -- In order to suppress these we set the MACOSX_DEPLOYMENT_TARGET variable into the far future.
@@ -38,27 +38,29 @@ Interesting options:
 
   -- We assume that the CMake variables do not contain escaped spaces
   let cflags := getCFlags root
-  let mut cflagsInternal := getInternalCFlags root
-  let mut ldflagsInternal := getInternalLinkerFlags root
+  let mut cflagsInternal := "@LEANC_INTERNAL_FLAGS@".trim.splitOn
+  let mut ldflagsInternal := "@LEANC_INTERNAL_LINKER_FLAGS@".trim.splitOn
   let ldflags := getLinkerFlags root linkStatic
 
   for arg in args do
     match arg with
     | "--print-cflags" =>
-      IO.println <| " ".intercalate cflags.toList
+      IO.println <| " ".intercalate (cflags.map rootify |>.toList)
       return 0
     | "--print-ldflags" =>
-      IO.println <| " ".intercalate (cflags ++ ldflags).toList
+      IO.println <| " ".intercalate ((cflags ++ ldflags).map rootify |>.toList)
       return 0
     | _ => pure ()
 
+  let mut cc := "@LEANC_CC@"
   if let some cc' ← IO.getEnv "LEAN_CC" then
     cc := cc'
     -- these are intended for the bundled compiler only
-    cflagsInternal := #[]
-    ldflagsInternal := #[]
+    cflagsInternal := []
+    ldflagsInternal := []
+  cc := rootify cc
   let args := cflags ++ cflagsInternal ++ args ++ ldflagsInternal ++ ldflags ++ ["-Wno-unused-command-line-argument"]
-  let args := args.filter (!·.isEmpty)
+  let args := args.filter (!·.isEmpty) |>.map rootify
   if args.contains "-v" then
     IO.eprintln s!"{cc} {" ".intercalate args.toList}"
   let child ← IO.Process.spawn { cmd := cc, args, env }

src/kernel/environment.cpp

@@ -299,12 +299,6 @@ extern "C" LEAN_EXPORT object * lean_add_decl(object * env, size_t max_heartbeat
         });
 }
 
-extern "C" LEAN_EXPORT object * lean_add_decl_without_checking(object * env, object * decl) {
-    return catch_kernel_exceptions<environment>([&]() {
-            return environment(env).add(declaration(decl, true), false);
-        });
-}
-
 void environment::for_each_constant(std::function<void(constant_info const & d)> const & f) const {
     smap_foreach(cnstr_get(raw(), 1), [&](object *, object * v) {
             constant_info cinfo(v, true);

src/lake/Lake/Build/Executable.lean

@@ -13,18 +13,10 @@ The build function definition for a Lean executable.
 
 def LeanExe.recBuildExe (self : LeanExe) : FetchM (BuildJob FilePath) :=
   withRegisterJob s!"{self.name}" do
-  /-
-  Remark: We must build the root before we fetch the transitive imports
-  so that errors in the import block of transitive imports will not kill this
-  job before the root is built.
-  -/
-  let mut linkJobs := #[]
-  for facet in self.root.nativeFacets self.supportInterpreter do
-    linkJobs := linkJobs.push <| ← fetch <| self.root.facet facet.name
   let imports ← self.root.transImports.fetch
-  for mod in imports do
-    for facet in mod.nativeFacets self.supportInterpreter do
-      linkJobs := linkJobs.push <| ← fetch <| mod.facet facet.name
+  let mut linkJobs := #[← self.root.o.fetch]
+  for mod in imports do for facet in mod.nativeFacets self.supportInterpreter do
+    linkJobs := linkJobs.push <| ← fetch <| mod.facet facet.name
   let deps := (← fetch <| self.pkg.facet `deps).push self.pkg
   for dep in deps do for lib in dep.externLibs do
     linkJobs := linkJobs.push <| ← lib.static.fetch

src/lake/Lake/Build/Module.lean

@@ -94,7 +94,7 @@ Recursively build a module's dependencies, including:
 * Shared libraries (e.g., `extern_lib` targets or precompiled modules)
 * `extraDepTargets` of its library
 -/
-def Module.recBuildDeps (mod : Module) : FetchM (BuildJob (SearchPath × Array FilePath)) := ensureJob do
+def Module.recBuildDeps (mod : Module) : FetchM (BuildJob (SearchPath × Array FilePath)) := do
   let extraDepJob ← mod.lib.extraDep.fetch
 
   /-
@@ -102,29 +102,30 @@ def Module.recBuildDeps (mod : Module) : FetchM (BuildJob (SearchPath × Array F
   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 ← mod.imports.fetch
+  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 ← if mod.shouldPrecompile then
-    mod.transImports.fetch else mod.precompileImports.fetch
-  let modLibJobs ← precompileImports.mapM (·.dynlib.fetch)
-  let pkgs := precompileImports.foldl (·.insert ·.pkg) OrdPackageSet.empty
-  let pkgs := if mod.shouldPrecompile then pkgs.insert mod.pkg else pkgs
-  let (externJobs, libDirs) ← recBuildExternDynlibs pkgs.toArray
+  let precompileImports ← try mod.precompileImports.fetch
+    catch errPos => return Job.error (← takeLogFrom errPos)
+  let modJobs ← precompileImports.mapM (·.dynlib.fetch)
+  let pkgs := precompileImports.foldl (·.insert ·.pkg)
+    OrdPackageSet.empty |>.insert mod.pkg |>.toArray
+  let (externJobs, libDirs) ← recBuildExternDynlibs pkgs
   let externDynlibsJob ← BuildJob.collectArray externJobs
-  let modDynlibsJob ← BuildJob.collectArray modLibJobs
+  let modDynlibsJob ← BuildJob.collectArray modJobs
 
   extraDepJob.bindAsync fun _ extraDepTrace => do
   importJob.bindAsync fun _ importTrace => do
-  modDynlibsJob.bindAsync fun modDynlibs modLibTrace => do
+  modDynlibsJob.bindAsync fun modDynlibs modTrace => do
   return externDynlibsJob.mapWithTrace fun externDynlibs externTrace =>
-    let depTrace := extraDepTrace.mix <| importTrace
+    let depTrace := extraDepTrace.mix <| importTrace.mix <| modTrace
     let depTrace :=
       match mod.platformIndependent with
-      | none => depTrace.mix <| modLibTrace.mix <| externTrace
-      | some false => depTrace.mix <| modLibTrace.mix <| externTrace.mix <| platformTrace
+      | none => depTrace.mix <| externTrace
+      | some false => depTrace.mix <| externTrace.mix <| platformTrace
       | some true => depTrace
     /-
     Requirements:

src/lake/Lake/CLI/Main.lean

@@ -201,12 +201,12 @@ def verifyInstall (opts : LakeOptions) : ExceptT CliError MainM PUnit := do
 def parseScriptSpec (ws : Workspace) (spec : String) : Except CliError Script :=
   match spec.splitOn "/" with
   | [scriptName] =>
-    match ws.findScript? (stringToLegalOrSimpleName scriptName) with
+    match ws.findScript? scriptName.toName with
     | some script => return script
     | none => throw <| CliError.unknownScript spec
   | [pkg, scriptName] => do
     let pkg ← parsePackageSpec ws pkg
-    match pkg.scripts.find? (stringToLegalOrSimpleName scriptName) with
+    match pkg.scripts.find? scriptName.toName with
     | some script => return script
     | none => throw <| CliError.unknownScript spec
   | _ => throw <| CliError.invalidScriptSpec spec

src/lake/Lake/DSL/Script.lean

@@ -15,7 +15,7 @@ namespace Lake.DSL
 open Lean Parser Command
 
 syntax scriptDeclSpec :=
-  identOrStr (ppSpace simpleBinder)? (declValSimple <|> declValDo)
+  ident (ppSpace simpleBinder)? (declValSimple <|> declValDo)
 
 /--
 Define a new Lake script for the package.
@@ -37,10 +37,9 @@ scoped syntax (name := scriptDecl)
 
 @[macro scriptDecl]
 def expandScriptDecl : Macro
-| `($[$doc?]? $[$attrs?]? script%$kw $name $[$args?]? do $seq $[$wds?:whereDecls]?) => do
-  `($[$doc?]? $[$attrs?]? script%$kw $name $[$args?]? := do $seq $[$wds?:whereDecls]?)
-| `($[$doc?]? $[$attrs?]? script%$kw $name $[$args?]? := $defn $[$wds?:whereDecls]?) => withRef kw do
-  let id := expandIdentOrStrAsIdent name
+| `($[$doc?]? $[$attrs?]? script%$kw $id:ident $[$args?]? do $seq $[$wds?:whereDecls]?) => do
+  `($[$doc?]? $[$attrs?]? script%$kw  $id:ident $[$args?]? := do $seq $[$wds?:whereDecls]?)
+| `($[$doc?]? $[$attrs?]? script%$kw  $id:ident $[$args?]? := $defn $[$wds?:whereDecls]?) => withRef kw do
   let args ← expandOptSimpleBinder args?
   let attrs := #[← `(Term.attrInstance| «script»)] ++ expandAttrs attrs?
   `($[$doc?]? @[$attrs,*] def $id : ScriptFn := fun $args => $defn $[$wds?:whereDecls]?)

src/lake/Lake/Load/Lean/Eval.lean

@@ -5,7 +5,6 @@ Authors: Mac Malone
 -/
 import Lake.DSL.Attributes
 import Lake.Config.Workspace
-import Lean.DocString
 
 /-! # Lean Configuration Evaluator
 

src/lake/examples/ffi/app/lakefile.lean

@@ -9,5 +9,4 @@ require ffi from ".."/"lib"
 lean_exe app where
   root := `Main
 
-lean_lib Test where
-  precompileModules := true
+lean_lib Test

src/lake/examples/ffi/lib/lakefile.lean

@@ -1,13 +1,14 @@
 import Lake
 open System Lake DSL
 
-package ffi where
+package ffi {
   srcDir := "lean"
+  precompileModules := true
+}
 
 lean_lib FFI
 
-@[default_target]
-lean_exe test where
+@[default_target] lean_exe test where
   root := `Main
 
 target ffi.o pkg : FilePath := do

src/lake/examples/ffi/package.sh

@@ -0,0 +1,10 @@
+set -ex
+
+cd app
+${LAKE:-../../../.lake/build/bin/lake} build -v -U
+cd ..
+
+
+cd lib
+${LAKE:-../../../.lake/build/bin/lake} build -v
+cd ..

src/lake/examples/ffi/test.sh

@@ -1,18 +1,8 @@
-#!/usr/bin/env bash
-set -euxo pipefail
-
-LAKE=${LAKE:-../../.lake/build/bin/lake}
+set -ex
 
 ./clean.sh
-
-# Tests that a non-precmpiled build does not load anything as a dynlib
-# https://github.com/leanprover/lean4/issues/4565
-$LAKE -d app build -v | (grep --color load-dynlib && exit 1 || true)
-$LAKE -d lib build -v | (grep --color load-dynlib && exit 1 || true)
-
+./package.sh
 ./app/.lake/build/bin/app
 ./lib/.lake/build/bin/test
 
-# Tests the successful precompilation of an `extern_lib`
-# Also tests a module with `precompileModules` always precompiles its imports
-$LAKE -d app build Test
+${LAKE:-../../.lake/build/bin/lake} -d app build -v Test

src/lake/examples/precompile/test.sh

@@ -4,9 +4,7 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 
 ./clean.sh
 $LAKE -d bar update
-# test that build a module w/o precompile modules still precompiles deps
-# https://github.com/leanprover/lake/issues/83
-$LAKE -d bar build
+$LAKE -d bar build # tests lake#83
 $LAKE -d foo build
 
 ./clean.sh

src/lake/examples/scripts/expected.out

@@ -1,5 +1,5 @@
 dep/hello
-scripts/say-goodbye
+scripts/dismiss
 scripts/greet
 Hello, world!
 Hello, me!
@@ -13,11 +13,10 @@ Greet the entity with the given name. Otherwise, greet the whole world.
 
 Hello from Dep!
 Hello from Dep!
-Goodbye!
 error: unknown script nonexistant
 error: unknown script nonexistant
 dep/hello
-scripts/say-goodbye
+scripts/dismiss
 scripts/greet
 Hello, world!
 Goodbye!

src/lake/examples/scripts/lakefile.lean

@@ -21,6 +21,6 @@ script greet (args) do
   return 0
 
 @[default_script]
-script "say-goodbye" do
+script dismiss do
   IO.println "Goodbye!"
   return 0

src/lake/examples/scripts/test.sh

@@ -15,11 +15,8 @@ $LAKE script run greet --me | tee -a produced.out
 $LAKE script doc greet | tee -a produced.out
 $LAKE script run hello | tee -a produced.out
 $LAKE script run dep/hello | tee -a produced.out
-# Test that non-indentifier names work
-# https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Running.20.60lake.60.20scripts.20from.20the.20command.20line/near/446944450
-$LAKE script run say-goodbye | tee -a produced.out
-($LAKE script run nonexistant 2>&1 | tee -a produced.out) && exit 1 || true
-($LAKE script doc nonexistant 2>&1 | tee -a produced.out) && exit 1 || true
+($LAKE script run nonexistant 2>&1 | tee -a produced.out) && false || true
+($LAKE script doc nonexistant 2>&1 | tee -a produced.out) && false || true
 $LAKE scripts | tee -a produced.out
 $LAKE run | tee -a produced.out
 

src/lake/tests/badImport/.gitignore

@@ -1 +1 @@
-Lib/Bogus.lean
+Lib/Y.lean

src/lake/tests/badImport/Etc.lean

@@ -1,2 +0,0 @@
--- Module used to test that a build continues after an import error
-import Bogus

src/lake/tests/badImport/Lib/A.lean

@@ -0,0 +1 @@
+import Lib.A

src/lake/tests/badImport/Lib/B.lean

@@ -1,2 +1 @@
--- Import a missing module within a Lake library
-import Lib.Bogus
+import Lib.Y

src/lake/tests/badImport/Lib/B1.lean

@@ -1,2 +0,0 @@
--- Import a module with a bad import
-import Lib.B

src/lake/tests/badImport/Lib/C.lean

@@ -0,0 +1 @@
+import Lib.A

src/lake/tests/badImport/Lib/S.lean

@@ -1,2 +0,0 @@
--- Module which imports itself
-import Lib.S

src/lake/tests/badImport/Lib/U.lean

@@ -1,2 +0,0 @@
--- Import a missing module outside any package known to Lake
-import Bogus

src/lake/tests/badImport/X.lean

@@ -1,2 +1 @@
--- From an executable, import a missing module within a Lake library
-import Lib.Bogus
+import Y

src/lake/tests/badImport/X1.lean

@@ -1,2 +0,0 @@
--- From an executable, import a module which contains a bad import
-import Lib.B

src/lake/tests/badImport/clean.sh

@@ -1 +1 @@
-rm -rf .lake lake-manifest.json Lib/Bogus.lean
+rm -rf .lake lake-manifest.json Lib/Y.lean

src/lake/tests/badImport/lakefile.lean

@@ -3,8 +3,5 @@ open Lake DSL
 
 package test
 
+lean_lib X
 lean_lib Lib
-lean_lib Etc
-
-lean_exe X
-lean_exe X1

src/lake/tests/badImport/test.sh

@@ -12,29 +12,22 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 # https://github.com/leanprover/lean4/issues/3351
 # https://github.com/leanprover/lean4/issues/3809
 
-# Test a module with a bad import does not kill the whole build
-($LAKE build Lib.U Etc 2>&1 && exit 1 || true) | grep --color -F "Building Etc"
 # Test importing a nmissing module from outside the workspace
-($LAKE build +Lib.U 2>&1 && exit 1 || true) | grep --color -F "U.lean:2:0: unknown module prefix 'Bogus'"
-$LAKE setup-file . Bogus # Lake ignores the file (the server will error)
+($LAKE build +X 2>&1 && exit 1 || true) | grep --color -F "X.lean:1:0: unknown module prefix 'Y'"
+$LAKE setup-file ./X.lean Y # Lake ignores the file (the server will error)
 # Test importing onself
-($LAKE build +Lib.S 2>&1 && exit 1 || true) | grep --color -F "S.lean: module imports itself"
-($LAKE setup-file ./Lib/S.lean Lib.S 2>&1 && exit 1 || true) | grep --color -F "S.lean: module imports itself"
+($LAKE build +Lib.A 2>&1 && exit 1 || true) | grep --color -F "A.lean: module imports itself"
+($LAKE setup-file ./Lib/A.lean Lib.A 2>&1 && exit 1 || true) | grep --color -F "A.lean: module imports itself"
 # Test importing a missing module from within the workspace
-($LAKE build +Lib.B 2>&1 && exit 1 || true) | grep --color -F "B.lean: bad import 'Lib.Bogus'"
-($LAKE setup-file ./Lib/B.lean Lib.Bogus 2>&1 && exit 1 || true) | grep --color "B.lean: bad import 'Lib.Bogus'"
+($LAKE build +Lib.B 2>&1 && exit 1 || true) | grep --color -F "B.lean: bad import 'Lib.Y'"
+($LAKE setup-file X.lean Lib.B 2>&1 && exit 1 || true) | grep --color "B.lean: bad import 'Lib.Y'"
 # Test a vanishing import within the workspace (lean4#3551)
-touch Lib/Bogus.lean
+touch Lib/Y.lean
 $LAKE build +Lib.B
-rm Lib/Bogus.lean
-($LAKE build +Lib.B 2>&1 && exit 1 || true) | grep --color -F "B.lean: bad import 'Lib.Bogus'"
-($LAKE setup-file . Lib.B 2>&1 && exit 1 || true) | grep --color "B.lean: bad import 'Lib.Bogus'"
-# Test a module which imports a module containing a bad import
-($LAKE build +Lib.B1 2>&1 && exit 1 || true) | grep --color -F "B1.lean: bad import 'Lib.B'"
-($LAKE setup-file ./Lib/B1.lean Lib.B 2>&1 && exit 1 || true) | grep --color -F "B1.lean: bad import 'Lib.B'"
-# Test an executable with a bad import does not kill the whole build
-($LAKE build X Etc 2>&1 && exit 1 || true) | grep --color -F "Building Etc"
-# Test an executable which imports a missing module from within the workspace
-($LAKE build X 2>&1 && exit 1 || true) | grep --color -F "X.lean: bad import 'Lib.Bogus'"
-# Test a executable which imports a module containing a bad import
-($LAKE build X1 2>&1 && exit 1 || true) | grep --color -F "B.lean: bad import 'Lib.Bogus'"
+rm Lib/Y.lean
+($LAKE build +Lib.B 2>&1 && exit 1 || true) | grep --color -F "B.lean: bad import 'Lib.Y'"
+($LAKE setup-file ./X.lean Lib.B 2>&1 && exit 1 || true) | grep --color "B.lean: bad import 'Lib.Y'"
+# Test a module C which imports another module A which contains a bad import
+($LAKE build +Lib.C 2>&1 && exit 1 || true) | grep --color -F "C.lean: bad import 'Lib.A'"
+($LAKE setup-file Lib/C.lean Lib.A 2>&1 && exit 1 || true) | grep --color -F "C.lean: bad import 'Lib.A'"
+

src/lake/tests/precompileArgs/lakefile.lean

@@ -6,5 +6,4 @@ package precompileArgs
 @[default_target]
 lean_lib Foo where
   precompileModules := true
-  platformIndependent := if get_config? platformIndependent |>.isSome then true else none
-  moreLinkArgs := if let some cfg := get_config? linkArgs then cfg.splitOn " " |>.toArray else #[]
+  moreLinkArgs := #["-lBaz"]

src/lake/tests/precompileArgs/test.sh

@@ -3,27 +3,7 @@ set -exo pipefail
 
 LAKE=${LAKE:-../../.lake/build/bin/lake}
 
-if [ "$OS" = Windows_NT ]; then
-LIB_PREFIX=
-SHARED_LIB_EXT=dll
-elif [ "`uname`" = Darwin ]; then
-LIB_PREFIX=lib
-SHARED_LIB_EXT=dylib
-else
-LIB_PREFIX=lib
-SHARED_LIB_EXT=so
-fi
-
 ./clean.sh
 
 # Test that `moreLinkArgs` are included when linking precompiled modules
-($LAKE build -KlinkArgs=-lBaz 2>&1 || true) | grep --color -- "-lBaz"
-
-# Test that dynlibs are part of the module trace unless `platformIndependent` is set
-$LAKE build -R
-echo foo > .lake/build/lib/${LIB_PREFIX}Foo-Bar-1.$SHARED_LIB_EXT
-($LAKE build 2>&1 --rehash && exit 1 || true) | grep --color "Building Foo"
-rm .lake/build/lib/${LIB_PREFIX}Foo-Bar-1.$SHARED_LIB_EXT
-$LAKE build -R -KplatformIndependent=true
-echo foo > .lake/build/lib/${LIB_PREFIX}Foo-Bar-1.$SHARED_LIB_EXT
-$LAKE build --rehash --no-build
+($LAKE build +Foo:dynlib 2>&1 || true) | grep --color -- "-lBaz"

src/library/constructions/CMakeLists.txt

@@ -1,3 +1,3 @@
-add_library(constructions OBJECT cases_on.cpp
-  no_confusion.cpp projection.cpp init_module.cpp
+add_library(constructions OBJECT rec_on.cpp cases_on.cpp
+  no_confusion.cpp projection.cpp brec_on.cpp init_module.cpp
   util.cpp)

src/library/constructions/brec_on.cpp

@@ -0,0 +1,318 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "runtime/sstream.h"
+#include "kernel/kernel_exception.h"
+#include "kernel/environment.h"
+#include "kernel/instantiate.h"
+#include "kernel/abstract.h"
+#include "kernel/type_checker.h"
+#include "kernel/inductive.h"
+#include "library/reducible.h"
+#include "library/bin_app.h"
+#include "library/suffixes.h"
+#include "library/util.h"
+#include "library/aux_recursors.h"
+#include "library/constructions/util.h"
+
+namespace lean {
+static optional<unsigned> is_typeformer_app(buffer<name> const & typeformer_names, expr const & e) {
+    expr const & fn = get_app_fn(e);
+    if (!is_fvar(fn))
+        return optional<unsigned>();
+    unsigned r = 0;
+    for (name const & n : typeformer_names) {
+        if (fvar_name(fn) == n)
+            return optional<unsigned>(r);
+        r++;
+    }
+    return optional<unsigned>();
+}
+
+static declaration mk_below(environment const & env, name const & n, bool ibelow) {
+    local_ctx lctx;
+    constant_info ind_info = env.get(n);
+    inductive_val ind_val  = ind_info.to_inductive_val();
+    name_generator ngen    = mk_constructions_name_generator();
+    unsigned nparams       = ind_val.get_nparams();
+    constant_info rec_info = env.get(mk_rec_name(n));
+    recursor_val rec_val   = rec_info.to_recursor_val();
+    unsigned nminors       = rec_val.get_nminors();
+    unsigned ntypeformers  = rec_val.get_nmotives();
+    names lps              = rec_info.get_lparams();
+    bool is_reflexive      = ind_val.is_reflexive();
+    level  lvl             = mk_univ_param(head(lps));
+    levels lvls            = lparams_to_levels(tail(lps));
+    names blvls;           // universe parameter names of ibelow/below
+    level  rlvl;           // universe level of the resultant type
+    // The arguments of below (ibelow) are the ones in the recursor - minor premises.
+    // The universe we map to is also different (l+1 for below of reflexive types) and (0 fo ibelow).
+    expr ref_type;
+    expr Type_result;
+    if (ibelow) {
+        // we are eliminating to Prop
+        blvls      = tail(lps);
+        rlvl       = mk_level_zero();
+        ref_type   = instantiate_lparam(rec_info.get_type(), param_id(lvl), mk_level_zero());
+    } else if (is_reflexive) {
+        blvls = lps;
+        rlvl  = get_datatype_level(env, ind_info.get_type());
+        // if rlvl is of the form (max 1 l), then rlvl <- l
+        if (is_max(rlvl) && is_one(max_lhs(rlvl)))
+            rlvl = max_rhs(rlvl);
+        rlvl       = mk_max(mk_succ(lvl), rlvl);
+        ref_type   = instantiate_lparam(rec_info.get_type(), param_id(lvl), mk_succ(lvl));
+    } else {
+        // we can simplify the universe levels for non-reflexive datatypes
+        blvls       = lps;
+        rlvl        = mk_max(mk_level_one(), lvl);
+        ref_type    = rec_info.get_type();
+    }
+    Type_result        = mk_sort(rlvl);
+    buffer<expr> ref_args;
+    to_telescope(lctx, ngen, ref_type, ref_args);
+    lean_assert(ref_args.size() == nparams + ntypeformers + nminors + ind_val.get_nindices() + 1);
+
+    // args contains the below/ibelow arguments
+    buffer<expr> args;
+    buffer<name> typeformer_names;
+    // add parameters and typeformers
+    for (unsigned i = 0; i < nparams; i++)
+        args.push_back(ref_args[i]);
+    for (unsigned i = nparams; i < nparams + ntypeformers; i++) {
+        args.push_back(ref_args[i]);
+        typeformer_names.push_back(fvar_name(ref_args[i]));
+    }
+    // we ignore minor premises in below/ibelow
+    for (unsigned i = nparams + ntypeformers + nminors; i < ref_args.size(); i++)
+        args.push_back(ref_args[i]);
+
+    // We define below/ibelow using the recursor for this type
+    levels rec_lvls       = cons(mk_succ(rlvl), lvls);
+    expr rec              = mk_constant(rec_info.get_name(), rec_lvls);
+    for (unsigned i = 0; i < nparams; i++)
+        rec = mk_app(rec, args[i]);
+    // add type formers
+    for (unsigned i = nparams; i < nparams + ntypeformers; i++) {
+        buffer<expr> targs;
+        to_telescope(lctx, ngen, lctx.get_type(args[i]), targs);
+        rec = mk_app(rec, lctx.mk_lambda(targs, Type_result));
+    }
+    // add minor premises
+    for (unsigned i = nparams + ntypeformers; i < nparams + ntypeformers + nminors; i++) {
+        expr minor = ref_args[i];
+        expr minor_type = lctx.get_type(minor);
+        buffer<expr> minor_args;
+        minor_type = to_telescope(lctx, ngen, minor_type, minor_args);
+        buffer<expr> prod_pairs;
+        for (expr & minor_arg : minor_args) {
+            buffer<expr> minor_arg_args;
+            expr minor_arg_type = to_telescope(env, lctx, ngen, lctx.get_type(minor_arg), minor_arg_args);
+            if (is_typeformer_app(typeformer_names, minor_arg_type)) {
+                expr fst  = lctx.get_type(minor_arg);
+                minor_arg = lctx.mk_local_decl(ngen, lctx.get_local_decl(minor_arg).get_user_name(), lctx.mk_pi(minor_arg_args, Type_result));
+                expr snd  = lctx.mk_pi(minor_arg_args, mk_app(minor_arg, minor_arg_args));
+                type_checker tc(env, lctx);
+                prod_pairs.push_back(mk_pprod(tc, fst, snd, ibelow));
+            }
+        }
+        type_checker tc(env, lctx);
+        expr new_arg = foldr([&](expr const & a, expr const & b) { return mk_pprod(tc, a, b, ibelow); },
+                             [&]() { return mk_unit(rlvl, ibelow); },
+                             prod_pairs.size(), prod_pairs.data());
+        rec = mk_app(rec, lctx.mk_lambda(minor_args, new_arg));
+    }
+
+    // add indices and major premise
+    for (unsigned i = nparams + ntypeformers; i < args.size(); i++) {
+        rec = mk_app(rec, args[i]);
+    }
+
+    name below_name  = ibelow ? name{n, "ibelow"} : name{n, "below"};
+    expr below_type  = lctx.mk_pi(args, Type_result);
+    expr below_value = lctx.mk_lambda(args, rec);
+
+    return mk_definition_inferring_unsafe(env, below_name, blvls, below_type, below_value,
+                                          reducibility_hints::mk_abbreviation());
+}
+
+static declaration mk_brec_on(environment const & env, name const & n, bool ind) {
+    local_ctx lctx;
+    constant_info ind_info = env.get(n);
+    inductive_val ind_val  = ind_info.to_inductive_val();
+    name_generator ngen    = mk_constructions_name_generator();
+    unsigned nparams       = ind_val.get_nparams();
+    constant_info rec_info = env.get(mk_rec_name(n));
+    recursor_val rec_val   = rec_info.to_recursor_val();
+    unsigned nminors       = rec_val.get_nminors();
+    unsigned ntypeformers  = rec_val.get_nmotives();
+    names lps              = rec_info.get_lparams();
+    bool is_reflexive      = ind_val.is_reflexive();
+    level  lvl             = mk_univ_param(head(lps));
+    levels lvls            = lparams_to_levels(tail(lps));
+    level rlvl;
+    names blps;
+    levels blvls; // universe level parameters of brec_on/binduction_on
+    // The arguments of brec_on (binduction_on) are the ones in the recursor - minor premises.
+    // The universe we map to is also different (l+1 for below of reflexive types) and (0 fo ibelow).
+    expr ref_type;
+    if (ind) {
+        // we are eliminating to Prop
+        blps       = tail(lps);
+        blvls      = lvls;
+        rlvl       = mk_level_zero();
+        ref_type   = instantiate_lparam(rec_info.get_type(), param_id(lvl), mk_level_zero());
+    } else if (is_reflexive) {
+        blps    = lps;
+        blvls   = cons(lvl, lvls);
+        rlvl    = get_datatype_level(env, ind_info.get_type());
+        // if rlvl is of the form (max 1 l), then rlvl <- l
+        if (is_max(rlvl) && is_one(max_lhs(rlvl)))
+            rlvl = max_rhs(rlvl);
+        rlvl       = mk_max(mk_succ(lvl), rlvl);
+        // inner_prod, inner_prod_intro, pr1, pr2 do not use the same universe levels for
+        // reflective datatypes.
+        ref_type   = instantiate_lparam(rec_info.get_type(), param_id(lvl), mk_succ(lvl));
+    } else {
+        // we can simplify the universe levels for non-reflexive datatypes
+        blps        = lps;
+        blvls       = cons(lvl, lvls);
+        rlvl        = mk_max(mk_level_one(), lvl);
+        ref_type    = rec_info.get_type();
+    }
+    buffer<expr> ref_args;
+    to_telescope(lctx, ngen, ref_type, ref_args);
+    lean_assert(ref_args.size() == nparams + ntypeformers + nminors + ind_val.get_nindices() + 1);
+
+    // args contains the brec_on/binduction_on arguments
+    buffer<expr> args;
+    buffer<name> typeformer_names;
+    // add parameters and typeformers
+    for (unsigned i = 0; i < nparams; i++)
+        args.push_back(ref_args[i]);
+    for (unsigned i = nparams; i < nparams + ntypeformers; i++) {
+        args.push_back(ref_args[i]);
+        typeformer_names.push_back(fvar_name(ref_args[i]));
+    }
+    // add indices and major premise
+    for (unsigned i = nparams + ntypeformers + nminors; i < ref_args.size(); i++)
+        args.push_back(ref_args[i]);
+    // create below terms (one per datatype)
+    //    (below.{lvls} params type-formers)
+    // Remark: it also creates the result type
+    buffer<expr> belows;
+    expr result_type;
+    unsigned k = 0;
+    for (name const & n1 : ind_val.get_all()) {
+        if (n1 == n) {
+            result_type = ref_args[nparams + k];
+            for (unsigned i = nparams + ntypeformers + nminors; i < ref_args.size(); i++)
+                result_type = mk_app(result_type, ref_args[i]);
+        }
+        k++;
+        name bname = name(n1, ind ? "ibelow" : "below");
+        expr below = mk_constant(bname, blvls);
+        for (unsigned i = 0; i < nparams; i++)
+            below = mk_app(below, ref_args[i]);
+        for (unsigned i = nparams; i < nparams + ntypeformers; i++)
+            below = mk_app(below, ref_args[i]);
+        belows.push_back(below);
+    }
+    // create functionals (one for each type former)
+    //     Pi idxs t, below idxs t -> C idxs t
+    buffer<expr> Fs;
+    name F_name("F");
+    for (unsigned i = nparams, j = 0; i < nparams + ntypeformers; i++, j++) {
+        expr const & C = ref_args[i];
+        buffer<expr> F_args;
+        to_telescope(lctx, ngen, lctx.get_type(C), F_args);
+        expr F_result = mk_app(C, F_args);
+        expr F_below  = mk_app(belows[j], F_args);
+        F_args.push_back(lctx.mk_local_decl(ngen, "f", F_below));
+        expr F_type   = lctx.mk_pi(F_args, F_result);
+        expr F        = lctx.mk_local_decl(ngen, F_name.append_after(j+1), F_type);
+        Fs.push_back(F);
+        args.push_back(F);
+    }
+
+    // We define brec_on/binduction_on using the recursor for this type
+    levels rec_lvls       = cons(rlvl, lvls);
+    expr rec              = mk_constant(rec_info.get_name(), rec_lvls);
+    // add parameters to rec
+    for (unsigned i = 0; i < nparams; i++)
+        rec = mk_app(rec, ref_args[i]);
+    // add type formers to rec
+    //     Pi indices t, prod (C ... t) (below ... t)
+    for (unsigned i = nparams, j = 0; i < nparams + ntypeformers; i++, j++) {
+        expr const & C = ref_args[i];
+        buffer<expr> C_args;
+        to_telescope(lctx, ngen, lctx.get_type(C), C_args);
+        expr C_t     = mk_app(C, C_args);
+        expr below_t = mk_app(belows[j], C_args);
+        type_checker tc(env, lctx);
+        expr prod    = mk_pprod(tc, C_t, below_t, ind);
+        rec = mk_app(rec, lctx.mk_lambda(C_args, prod));
+    }
+    // add minor premises to rec
+    for (unsigned i = nparams + ntypeformers, j = 0; i < nparams + ntypeformers + nminors; i++, j++) {
+        expr minor      = ref_args[i];
+        expr minor_type = lctx.get_type(minor);
+        buffer<expr> minor_args;
+        minor_type = to_telescope(lctx, ngen, minor_type, minor_args);
+        buffer<expr> pairs;
+        for (expr & minor_arg : minor_args) {
+            buffer<expr> minor_arg_args;
+            expr minor_arg_type = to_telescope(env, lctx, ngen, lctx.get_type(minor_arg), minor_arg_args);
+            if (auto k = is_typeformer_app(typeformer_names, minor_arg_type)) {
+                buffer<expr> C_args;
+                get_app_args(minor_arg_type, C_args);
+                type_checker tc(env, lctx);
+                expr new_minor_arg_type = mk_pprod(tc, minor_arg_type, mk_app(belows[*k], C_args), ind);
+                minor_arg = lctx.mk_local_decl(ngen, lctx.get_local_decl(minor_arg).get_user_name(), lctx.mk_pi(minor_arg_args, new_minor_arg_type));
+                if (minor_arg_args.empty()) {
+                    pairs.push_back(minor_arg);
+                } else {
+                    type_checker tc(env, lctx);
+                    expr r = mk_app(minor_arg, minor_arg_args);
+                    expr r_1 = lctx.mk_lambda(minor_arg_args, mk_pprod_fst(tc, r, ind));
+                    expr r_2 = lctx.mk_lambda(minor_arg_args, mk_pprod_snd(tc, r, ind));
+                    pairs.push_back(mk_pprod_mk(tc, r_1, r_2, ind));
+                }
+            }
+        }
+        type_checker tc(env, lctx);
+        expr b = foldr([&](expr const & a, expr const & b) { return mk_pprod_mk(tc, a, b, ind); },
+                       [&]() { return mk_unit_mk(rlvl, ind); },
+                       pairs.size(), pairs.data());
+        unsigned F_idx = *is_typeformer_app(typeformer_names, minor_type);
+        expr F = Fs[F_idx];
+        buffer<expr> F_args;
+        get_app_args(minor_type, F_args);
+        F_args.push_back(b);
+        expr new_arg = mk_pprod_mk(tc, mk_app(F, F_args), b, ind);
+        rec = mk_app(rec, lctx.mk_lambda(minor_args, new_arg));
+    }
+    // add indices and major to rec
+    for (unsigned i = nparams + ntypeformers + nminors; i < ref_args.size(); i++)
+        rec = mk_app(rec, ref_args[i]);
+
+    type_checker tc(env, lctx);
+    name brec_on_name  = name(n, ind ? g_binduction_on : g_brec_on);
+    expr brec_on_type  = lctx.mk_pi(args, result_type);
+    expr brec_on_value = lctx.mk_lambda(args, mk_pprod_fst(tc, rec, ind));
+
+    return mk_definition_inferring_unsafe(env, brec_on_name, blps, brec_on_type, brec_on_value,
+                                          reducibility_hints::mk_abbreviation());
+}
+
+extern "C" LEAN_EXPORT object * lean_mk_below(object * env, object * n, uint8 ibelow) {
+    return catch_kernel_exceptions<declaration>([&]() { return mk_below(environment(env), name(n, true), ibelow); });
+}
+
+extern "C" LEAN_EXPORT object * lean_mk_brec_on(object * env, object * n, uint8 ind) {
+    return catch_kernel_exceptions<declaration>([&]() { return mk_brec_on(environment(env), name(n, true), ind); });
+}
+}

src/library/constructions/brec_on.h

@@ -0,0 +1,22 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/environment.h"
+
+namespace lean {
+/** \brief Given an inductive datatype \c n in \c env, return declaration for
+    <tt>n.below</tt> or <tt>.nibelow</tt> auxiliary construction for <tt>n.brec_on</t>
+    (aka below recursion on).
+*/
+declaration mk_below(environment const & env, name const & n, bool ibelow);
+
+/** \brief Given an inductive datatype \c n in \c env, return declaration for
+    <tt>n.brec_on</tt> or <tt>n.binduction_on</tt>.
+*/
+declaration mk_brec_on(environment const & env, name const & n, bool ind);
+
+}

src/library/constructions/rec_on.cpp

@@ -0,0 +1,64 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "runtime/sstream.h"
+#include "kernel/kernel_exception.h"
+#include "kernel/environment.h"
+#include "kernel/instantiate.h"
+#include "kernel/abstract.h"
+#include "kernel/inductive.h"
+#include "library/reducible.h"
+#include "library/suffixes.h"
+#include "library/aux_recursors.h"
+#include "library/constructions/util.h"
+
+namespace lean {
+declaration mk_rec_on(environment const & env, name const & n) {
+    constant_info ind_info = env.get(n);
+    if (!ind_info.is_inductive())
+        throw exception(sstream() << "error in '" << g_rec_on << "' generation, '" << n << "' is not an inductive datatype");
+    name_generator ngen = mk_constructions_name_generator();
+    local_ctx lctx;
+    name rec_on_name(n, g_rec_on);
+    constant_info rec_info = env.get(mk_rec_name(n));
+    recursor_val  rec_val  = rec_info.to_recursor_val();
+    buffer<expr> locals;
+    expr rec_type = rec_info.get_type();
+    while (is_pi(rec_type)) {
+        expr local = lctx.mk_local_decl(ngen, binding_name(rec_type), binding_domain(rec_type), binding_info(rec_type));
+        rec_type   = instantiate(binding_body(rec_type), local);
+        locals.push_back(local);
+    }
+
+    // locals order
+    //   As Cs minor_premises indices major-premise
+
+    // new_locals order
+    //   As Cs indices major-premise minor-premises
+    buffer<expr> new_locals;
+    unsigned num_indices  = rec_val.get_nindices();
+    unsigned num_minors   = rec_val.get_nminors();
+    unsigned AC_sz        = locals.size() - num_minors - num_indices - 1;
+    for (unsigned i = 0; i < AC_sz; i++)
+        new_locals.push_back(locals[i]);
+    for (unsigned i = 0; i < num_indices + 1; i++)
+        new_locals.push_back(locals[AC_sz + num_minors + i]);
+    for (unsigned i = 0; i < num_minors; i++)
+        new_locals.push_back(locals[AC_sz + i]);
+    expr rec_on_type = lctx.mk_pi(new_locals, rec_type);
+
+    levels ls = lparams_to_levels(rec_info.get_lparams());
+    expr rec  = mk_constant(rec_info.get_name(), ls);
+    expr rec_on_val = lctx.mk_lambda(new_locals, mk_app(rec, locals));
+
+    return mk_definition_inferring_unsafe(env, rec_on_name, rec_info.get_lparams(),
+                                          rec_on_type, rec_on_val, reducibility_hints::mk_abbreviation());
+}
+
+extern "C" LEAN_EXPORT object * lean_mk_rec_on(object * env, object * n) {
+    return catch_kernel_exceptions<declaration>([&]() { return mk_rec_on(environment(env), name(n, true)); });
+}
+}

src/library/constructions/rec_on.h

@@ -0,0 +1,19 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/environment.h"
+
+namespace lean {
+/** \brief Given an inductive datatype \c n in \c env, returns
+    the declaration for <tt>n.rec_on</tt>.
+
+    \remark <tt>rec_on</tt> is based on <tt>n.rec</tt>
+
+    \remark Throws an exception if \c n is not an inductive datatype.
+*/
+declaration mk_rec_on(environment const & env, name const & n);
+}

src/library/constructions/util.cpp

@@ -12,6 +12,63 @@ Author: Leonardo de Moura
 namespace lean {
 static name * g_constructions_fresh = nullptr;
 
+static level get_level(type_checker & ctx, expr const & A) {
+    expr S = ctx.whnf(ctx.infer(A));
+    if (!is_sort(S))
+        throw exception("invalid expression, sort expected");
+    return sort_level(S);
+}
+
+expr mk_and_intro(type_checker & ctx, expr const & Ha, expr const & Hb) {
+    return mk_app(mk_constant(get_and_intro_name()), ctx.infer(Ha), ctx.infer(Hb), Ha, Hb);
+}
+
+expr mk_and_left(type_checker &, expr const & H) {
+    return mk_proj(get_and_name(), nat(0), H);
+}
+
+expr mk_and_right(type_checker &, expr const & H) {
+    return mk_proj(get_and_name(), nat(1), H);
+}
+
+expr mk_pprod(type_checker & ctx, expr const & A, expr const & B) {
+    level l1 = get_level(ctx, A);
+    level l2 = get_level(ctx, B);
+    return mk_app(mk_constant(get_pprod_name(), {l1, l2}), A, B);
+}
+
+expr mk_pprod_mk(type_checker & ctx, expr const & a, expr const & b) {
+    expr A = ctx.infer(a);
+    expr B = ctx.infer(b);
+    level l1 = get_level(ctx, A);
+    level l2 = get_level(ctx, B);
+    return mk_app(mk_constant(get_pprod_mk_name(), {l1, l2}), A, B, a, b);
+}
+
+expr mk_pprod_fst(type_checker &, expr const & p) {
+    return mk_proj(get_pprod_name(), nat(0), p);
+}
+
+expr mk_pprod_snd(type_checker &, expr const & p) {
+    return mk_proj(get_pprod_name(), nat(1), p);
+}
+
+expr mk_pprod(type_checker & ctx, expr const & a, expr const & b, bool prop) {
+    return prop ? mk_and(a, b) : mk_pprod(ctx, a, b);
+}
+
+expr mk_pprod_mk(type_checker & ctx, expr const & a, expr const & b, bool prop) {
+    return prop ? mk_and_intro(ctx, a, b) : mk_pprod_mk(ctx, a, b);
+}
+
+expr mk_pprod_fst(type_checker & ctx, expr const & p, bool prop) {
+    return prop ? mk_and_left(ctx, p) : mk_pprod_fst(ctx, p);
+}
+
+expr mk_pprod_snd(type_checker & ctx, expr const & p, bool prop) {
+    return prop ? mk_and_right(ctx, p) : mk_pprod_snd(ctx, p);
+}
+
 name_generator mk_constructions_name_generator() {
     return name_generator(*g_constructions_fresh);
 }

src/library/constructions/util.h

@@ -9,6 +9,13 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 
 namespace lean {
+environment completion_add_to_black_list(environment const & env, name const & decl_name);
+
+expr mk_pprod(type_checker & ctx, expr const & a, expr const & b, bool prop);
+expr mk_pprod_mk(type_checker & ctx, expr const & a, expr const & b, bool prop);
+expr mk_pprod_fst(type_checker & ctx, expr const & p, bool prop);
+expr mk_pprod_snd(type_checker & ctx, expr const & p, bool prop);
+
 name_generator mk_constructions_name_generator();
 void initialize_constructions_util();
 void finalize_constructions_util();

src/library/suffixes.h

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 constexpr char const * g_rec               = "rec";
+constexpr char const * g_rec_on            = "recOn";
 constexpr char const * g_brec_on           = "brecOn";
 constexpr char const * g_binduction_on     = "binductionOn";
 constexpr char const * g_cases_on          = "casesOn";

src/util/ffi.cpp

@@ -13,15 +13,7 @@ extern "C" object * lean_get_leanc_extra_flags(object *) {
     return lean_mk_string("@LEANC_EXTRA_FLAGS@");
 }
 
-extern "C" object * lean_get_leanc_internal_flags(object *) {
-    return lean_mk_string("@LEANC_INTERNAL_FLAGS@");
-}
-
 extern "C" object * lean_get_linker_flags(uint8 link_static) {
     return lean_mk_string(link_static ? "@LEANC_STATIC_LINKER_FLAGS@ @LEAN_EXTRA_LINKER_FLAGS@" : "@LEANC_SHARED_LINKER_FLAGS@ @LEAN_EXTRA_LINKER_FLAGS@");
 }
-
-extern "C" object * lean_get_internal_linker_flags(object *) {
-    return lean_mk_string("@LEANC_INTERNAL_LINKER_FLAGS@");
-}
 }