chore: fix apply? error reporting when out of heartbeats

src/Init/Data/Array/Basic.lean

@@ -613,15 +613,8 @@ def findIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option Nat :=
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   loop 0
 
-@[inline]
-def findFinIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option (Fin as.size) :=
-  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-  loop (j : Nat) :=
-    if h : j < as.size then
-      if p as[j] then some ⟨j, h⟩ else loop (j + 1)
-    else none
-    decreasing_by simp_wf; decreasing_trivial_pre_omega
-  loop 0
+def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
+  a.findIdx? fun a => a == v
 
 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size) :=
@@ -634,10 +627,6 @@ decreasing_by simp_wf; decreasing_trivial_pre_omega
 def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
   indexOfAux a v 0
 
-@[deprecated indexOf? (since := "2024-11-20")]
-def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
-  a.findIdx? fun a => a == v
-
 @[inline]
 def any (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool :=
   Id.run <| as.anyM p start stop
@@ -777,62 +766,48 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   go 0 #[]
 
-/--
-Remove the element at a given index from an array without a runtime bounds checks,
-using a `Nat` index and a tactic-provided bound.
+/-- Remove the element at a given index from an array without bounds checks, using a `Fin` index.
 
-This function takes worst case O(n) time because
-it has to backshift all elements at positions greater than `i`.-/
+  This function takes worst case O(n) time because
+  it has to backshift all elements at positions greater than `i`.-/
 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-def eraseIdx (a : Array α) (i : Nat) (h : i < a.size := by get_elem_tactic) : Array α :=
-  if h' : i + 1 < a.size then
-    let a' := a.swap ⟨i + 1, h'⟩ ⟨i, h⟩
-    a'.eraseIdx (i + 1) (by simp [a', h'])
+def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
+  if h : i.val + 1 < a.size then
+    let a' := a.swap ⟨i.val + 1, h⟩ i
+    let i' : Fin a'.size := ⟨i.val + 1, by simp [a', h]⟩
+    a'.feraseIdx i'
   else
     a.pop
-termination_by a.size - i
-decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ h
+termination_by a.size - i.val
+decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ i.isLt
 
 -- This is required in `Lean.Data.PersistentHashMap`.
-@[simp] theorem size_eraseIdx (a : Array α) (i : Nat) (h) : (a.eraseIdx i h).size = a.size - 1 := by
-  induction a, i, h using Array.eraseIdx.induct with
-  | @case1 a i h h' a' ih =>
-    unfold eraseIdx
-    simp [h', a', ih]
-  | case2 a i h h' =>
-    unfold eraseIdx
-    simp [h']
+@[simp] theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
+  induction a, i using Array.feraseIdx.induct with
+  | @case1 a i h a' _ ih =>
+    unfold feraseIdx
+    simp [h, a', ih]
+  | case2 a i h =>
+    unfold feraseIdx
+    simp [h]
 
 /-- Remove the element at a given index from an array, or do nothing if the index is out of bounds.
 
   This function takes worst case O(n) time because
   it has to backshift all elements at positions greater than `i`.-/
-def eraseIdxIfInBounds (a : Array α) (i : Nat) : Array α :=
-  if h : i < a.size then a.eraseIdx i h else a
-
-/-- Remove the element at a given index from an array, or panic if the index is out of bounds.
-
-This function takes worst case O(n) time because
-it has to backshift all elements at positions greater than `i`. -/
-def eraseIdx! (a : Array α) (i : Nat) : Array α :=
-  if h : i < a.size then a.eraseIdx i h else panic! "invalid index"
+def eraseIdx (a : Array α) (i : Nat) : Array α :=
+  if h : i < a.size then a.feraseIdx ⟨i, h⟩ else a
 
 def erase [BEq α] (as : Array α) (a : α) : Array α :=
   match as.indexOf? a with
   | none   => as
-  | some i => as.eraseIdx i
-
-/-- Erase the first element that satisfies the predicate `p`. -/
-def eraseP (as : Array α) (p : α → Bool) : Array α :=
-  match as.findIdx? p with
-  | none   => as
-  | some i => as.eraseIdxIfInBounds i
+  | some i => as.feraseIdx i
 
 /-- Insert element `a` at position `i`. -/
-@[inline] def insertIdx (as : Array α) (i : Nat) (a : α) (_ : i ≤ as.size := by get_elem_tactic) : Array α :=
+@[inline] def insertAt (as : Array α) (i : Fin (as.size + 1)) (a : α) : Array α :=
   let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
   loop (as : Array α) (j : Fin as.size) :=
-    if i < j then
+    if i.1 < j then
       let j' := ⟨j-1, Nat.lt_of_le_of_lt (Nat.pred_le _) j.2⟩
       let as := as.swap j' j
       loop as ⟨j', by rw [size_swap]; exact j'.2⟩
@@ -843,23 +818,12 @@ def eraseP (as : Array α) (p : α → Bool) : Array α :=
   let as := as.push a
   loop as ⟨j, size_push .. ▸ j.lt_succ_self⟩
 
-@[deprecated insertIdx (since := "2024-11-20")] abbrev insertAt := @insertIdx
-
 /-- Insert element `a` at position `i`. Panics if `i` is not `i ≤ as.size`. -/
-def insertIdx! (as : Array α) (i : Nat) (a : α) : Array α :=
+def insertAt! (as : Array α) (i : Nat) (a : α) : Array α :=
   if h : i ≤ as.size then
-    insertIdx as i a
+    insertAt as ⟨i, Nat.lt_succ_of_le h⟩ a
   else panic! "invalid index"
 
-@[deprecated insertIdx! (since := "2024-11-20")] abbrev insertAt! := @insertIdx!
-
-/-- Insert element `a` at position `i`, or do nothing if `as.size < i`. -/
-def insertIdxIfInBounds (as : Array α) (i : Nat) (a : α) : Array α :=
-  if h : i ≤ as.size then
-    insertIdx as i a
-  else
-    as
-
 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : Nat) : Bool :=
   if h : i < as.size then

src/Init/Data/Array/BinSearch.lean

@@ -52,7 +52,7 @@ namespace Array
     let mid    := (lo + hi)/2
     let midVal := as.get! mid
     if lt midVal k then
-      if mid == lo then do let v ← add (); pure <| as.insertIdx! (lo+1) v
+      if mid == lo then do let v ← add (); pure <| as.insertAt! (lo+1) v
       else binInsertAux lt merge add as k mid hi
     else if lt k midVal then
       binInsertAux lt merge add as k lo mid
@@ -67,7 +67,7 @@ namespace Array
     (k : α) : m (Array α) :=
   let _ := Inhabited.mk k
   if as.isEmpty then do let v ← add (); pure <| as.push v
-  else if lt k (as.get! 0) then do let v ← add (); pure <| as.insertIdx! 0 v
+  else if lt k (as.get! 0) then do let v ← add (); pure <| as.insertAt! 0 v
   else if !lt (as.get! 0) k then as.modifyM 0 <| merge
   else if lt as.back! k then do let v ← add (); pure <| as.push v
   else if !lt k as.back! then as.modifyM (as.size - 1) <| merge

src/Init/Data/Array/Lemmas.lean

@@ -1602,9 +1602,9 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
 
 /-! ### eraseIdx -/
 
-theorem eraseIdx_eq_eraseIdxIfInBounds {a : Array α} {i : Nat} (h : i < a.size) :
-    a.eraseIdx i h = a.eraseIdxIfInBounds i := by
-  simp [eraseIdxIfInBounds, h]
+theorem feraseIdx_eq_eraseIdx {a : Array α} {i : Fin a.size} :
+    a.feraseIdx i = a.eraseIdx i.1 := by
+  simp [eraseIdx]
 
 /-! ### isPrefixOf -/
 
@@ -1834,15 +1834,16 @@ theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
     l.toArray.takeWhile p = (l.takeWhile p).toArray := by
   simp [Array.takeWhile, takeWhile_go_toArray]
 
-@[simp] theorem eraseIdx_toArray (l : List α) (i : Nat) (h : i < l.toArray.size) :
-    l.toArray.eraseIdx i h = (l.eraseIdx i).toArray := by
-  rw [Array.eraseIdx]
-  split <;> rename_i h'
-  · rw [eraseIdx_toArray]
+@[simp] theorem feraseIdx_toArray (l : List α) (i : Fin l.toArray.size) :
+    l.toArray.feraseIdx i = (l.eraseIdx i).toArray := by
+  rw [feraseIdx]
+  split <;> rename_i h
+  · rw [feraseIdx_toArray]
     simp only [swap_toArray, Fin.getElem_fin, toList_toArray, mk.injEq]
     rw [eraseIdx_set_gt (by simp), eraseIdx_set_eq]
     simp
-  · simp at h h'
+  · rcases i with ⟨i, w⟩
+    simp at h w
     have t : i = l.length - 1 := by omega
     simp [t]
 termination_by l.length - i
@@ -1852,9 +1853,9 @@ decreasing_by
   simp
   omega
 
-@[simp] theorem eraseIdxIfInBounds_toArray (l : List α) (i : Nat) :
-    l.toArray.eraseIdxIfInBounds i = (l.eraseIdx i).toArray := by
-  rw [Array.eraseIdxIfInBounds]
+@[simp] theorem eraseIdx_toArray (l : List α) (i : Nat) :
+    l.toArray.eraseIdx i = (l.eraseIdx i).toArray := by
+  rw [Array.eraseIdx]
   split
   · simp
   · simp_all [eraseIdx_eq_self.2]
@@ -1873,13 +1874,13 @@ namespace Array
     (as.takeWhile p).toList = as.toList.takeWhile p := by
   induction as; simp
 
-@[simp] theorem toList_eraseIdx (as : Array α) (i : Nat) (h : i < as.size) :
-    (as.eraseIdx i h).toList = as.toList.eraseIdx i := by
+@[simp] theorem toList_feraseIdx (as : Array α) (i : Fin as.size) :
+    (as.feraseIdx i).toList = as.toList.eraseIdx i.1 := by
   induction as
   simp
 
-@[simp] theorem toList_eraseIdxIfInBounds (as : Array α) (i : Nat) :
-    (as.eraseIdxIfInBounds i).toList = as.toList.eraseIdx i := by
+@[simp] theorem toList_eraseIdx (as : Array α) (i : Nat) :
+    (as.eraseIdx i).toList = as.toList.eraseIdx i := by
   induction as
   simp
 

src/Init/Data/BitVec/Lemmas.lean

@@ -2611,7 +2611,7 @@ theorem getLsbD_rotateLeftAux_of_geq {x : BitVec w} {r : Nat} {i : Nat} (hi : i
   apply getLsbD_ge
   omega
 
-/-- When `r < w`, we give a formula for `(x.rotateLeft r).getLsbD i`. -/
+/-- When `r < w`, we give a formula for `(x.rotateRight r).getLsbD i`. -/
 theorem getLsbD_rotateLeft_of_le {x : BitVec w} {r i : Nat} (hr: r < w) :
     (x.rotateLeft r).getLsbD i =
       cond (i < r)
@@ -2638,56 +2638,6 @@ theorem getElem_rotateLeft {x : BitVec w} {r i : Nat} (h : i < w) :
       if h' : i < r % w then x[(w - (r % w) + i)] else x[i - (r % w)] := by
   simp [← BitVec.getLsbD_eq_getElem, h]
 
-/-- If `w ≤ x < 2 * w`, then `x % w = x - w` -/
-theorem mod_eq_sub_of_le_of_lt {x w : Nat} (x_le : w ≤ x) (x_lt : x < 2 * w) :
-    x % w = x - w := by
-  rw [Nat.mod_eq_sub_mod, Nat.mod_eq_of_lt (by omega)]
-  omega
-
-theorem getMsbD_rotateLeftAux_of_lt {x : BitVec w} {r : Nat} {i : Nat} (hi : i < w - r) :
-    (x.rotateLeftAux r).getMsbD i = x.getMsbD (r + i) := by
-  rw [rotateLeftAux, getMsbD_or]
-  simp [show i < w - r by omega, Nat.add_comm]
-
-theorem getMsbD_rotateLeftAux_of_ge {x : BitVec w} {r : Nat} {i : Nat} (hi : i ≥ w - r) :
-    (x.rotateLeftAux r).getMsbD i = (decide (i < w) && x.getMsbD (i - (w - r))) := by
-  simp [rotateLeftAux, getMsbD_or, show i + r ≥ w by omega, show ¬i < w - r by omega]
-
-/-- When `r < w`, we give a formula for `(x.rotateLeft r).getMsbD i`. -/
-theorem getMsbD_rotateLeft_of_lt {n w : Nat} {x : BitVec w} (hi : r < w):
-    (x.rotateLeft r).getMsbD n = (decide (n < w) && x.getMsbD ((r + n) % w)) := by
-  rcases w with rfl | w
-  · simp
-  · rw [BitVec.rotateLeft_eq_rotateLeftAux_of_lt (by omega)]
-    by_cases h : n < (w + 1) - r
-    · simp [getMsbD_rotateLeftAux_of_lt h, Nat.mod_eq_of_lt, show r + n < (w + 1) by omega, show n < w + 1 by omega]
-    · simp [getMsbD_rotateLeftAux_of_ge <| Nat.ge_of_not_lt h]
-      by_cases h₁ : n < w + 1
-      · simp only [h₁, decide_true, Bool.true_and]
-        have h₂ : (r + n) < 2 * (w + 1) := by omega
-        rw [mod_eq_sub_of_le_of_lt (by omega) (by omega)]
-        congr 1
-        omega
-      · simp [h₁]
-
-theorem getMsbD_rotateLeft {r n w : Nat} {x : BitVec w} :
-    (x.rotateLeft r).getMsbD n = (decide (n < w) && x.getMsbD ((r + n) % w)) := by
-  rcases w with rfl | w
-  · simp
-  · by_cases h : r < w
-    · rw [getMsbD_rotateLeft_of_lt (by omega)]
-    · rw [← rotateLeft_mod_eq_rotateLeft, getMsbD_rotateLeft_of_lt (by apply Nat.mod_lt; simp)]
-      simp
-
-@[simp]
-theorem msb_rotateLeft {m w : Nat} {x : BitVec w} :
-    (x.rotateLeft m).msb = x.getMsbD (m % w) := by
-  simp only [BitVec.msb, getMsbD_rotateLeft]
-  by_cases h : w = 0
-  · simp [h]
-  · simp
-    omega
-
 /-! ## Rotate Right -/
 
 /--
@@ -2749,7 +2699,7 @@ theorem rotateRight_mod_eq_rotateRight {x : BitVec w} {r : Nat} :
   simp only [rotateRight, Nat.mod_mod]
 
 /-- When `r < w`, we give a formula for `(x.rotateRight r).getLsb i`. -/
-theorem getLsbD_rotateRight_of_lt {x : BitVec w} {r i : Nat} (hr: r < w) :
+theorem getLsbD_rotateRight_of_le {x : BitVec w} {r i : Nat} (hr: r < w) :
     (x.rotateRight r).getLsbD i =
       cond (i < w - r)
       (x.getLsbD (r + i))
@@ -2767,7 +2717,7 @@ theorem getLsbD_rotateRight {x : BitVec w} {r i : Nat} :
       (decide (i < w) && x.getLsbD (i - (w - (r % w)))) := by
   rcases w with ⟨rfl, w⟩
   · simp
-  · rw [← rotateRight_mod_eq_rotateRight, getLsbD_rotateRight_of_lt (Nat.mod_lt _ (by omega))]
+  · rw [← rotateRight_mod_eq_rotateRight, getLsbD_rotateRight_of_le (Nat.mod_lt _ (by omega))]
 
 @[simp]
 theorem getElem_rotateRight {x : BitVec w} {r i : Nat} (h : i < w) :
@@ -2775,56 +2725,6 @@ theorem getElem_rotateRight {x : BitVec w} {r i : Nat} (h : i < w) :
   simp only [← BitVec.getLsbD_eq_getElem]
   simp [getLsbD_rotateRight, h]
 
-theorem getMsbD_rotateRightAux_of_lt {x : BitVec w} {r : Nat} {i : Nat} (hi : i < r) :
-    (x.rotateRightAux r).getMsbD i = x.getMsbD (i + (w - r)) := by
-  rw [rotateRightAux, getMsbD_or, getMsbD_ushiftRight]
-  simp [show i < r by omega]
-
-theorem getMsbD_rotateRightAux_of_ge {x : BitVec w} {r : Nat} {i : Nat} (hi : i ≥ r) :
-    (x.rotateRightAux r).getMsbD i = (decide (i < w) && x.getMsbD (i - r)) := by
-  simp [rotateRightAux, show ¬ i < r by omega, show i + (w - r) ≥ w by omega]
-
-/-- When `m < w`, we give a formula for `(x.rotateLeft m).getMsbD i`. -/
-@[simp]
-theorem getMsbD_rotateRight_of_lt {w n m : Nat} {x : BitVec w} (hr : m < w):
-    (x.rotateRight m).getMsbD n = (decide (n < w) && (if (n < m % w)
-    then x.getMsbD ((w + n - m % w) % w) else x.getMsbD (n - m % w))):= by
-  rcases w with rfl | w
-  · simp
-  · rw [rotateRight_eq_rotateRightAux_of_lt (by omega)]
-    by_cases h : n < m
-    · simp only [getMsbD_rotateRightAux_of_lt h, show n < w + 1 by omega, decide_true,
-        show m % (w + 1) = m by rw [Nat.mod_eq_of_lt hr], h, ↓reduceIte,
-        show (w + 1 + n - m) < (w + 1) by omega, Nat.mod_eq_of_lt, Bool.true_and]
-      congr 1
-      omega
-    · simp [h, getMsbD_rotateRightAux_of_ge <| Nat.ge_of_not_lt h]
-      by_cases h₁ : n < w + 1
-      · simp [h, h₁, decide_true, Bool.true_and, Nat.mod_eq_of_lt hr]
-      · simp [h₁]
-
-@[simp]
-theorem getMsbD_rotateRight {w n m : Nat} {x : BitVec w} :
-    (x.rotateRight m).getMsbD n = (decide (n < w) && (if (n < m % w)
-    then x.getMsbD ((w + n - m % w) % w) else x.getMsbD (n - m % w))):= by
-  rcases w with rfl | w
-  · simp
-  · by_cases h₀ : m < w
-    · rw [getMsbD_rotateRight_of_lt (by omega)]
-    · rw [← rotateRight_mod_eq_rotateRight, getMsbD_rotateRight_of_lt (by apply Nat.mod_lt; simp)]
-      simp
-
-@[simp]
-theorem msb_rotateRight {r w : Nat} {x : BitVec w} :
-    (x.rotateRight r).msb = x.getMsbD ((w - r % w) % w) := by
-  simp only [BitVec.msb, getMsbD_rotateRight]
-  by_cases h₀ : 0 < w
-  · simp only [h₀, decide_true, Nat.add_zero, Nat.zero_le, Nat.sub_eq_zero_of_le, Bool.true_and,
-    ite_eq_left_iff, Nat.not_lt, Nat.le_zero_eq]
-    intro h₁
-    simp [h₁]
-  · simp [show w = 0 by omega]
-
 /- ## twoPow -/
 
 theorem twoPow_eq (w : Nat) (i : Nat) : twoPow w i = 1#w <<< i := by

src/Init/Data/List/Attach.lean

@@ -238,7 +238,7 @@ theorem get_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h :
     (hn : n < (pmap f l h).length) :
     get (pmap f l h) ⟨n, hn⟩ =
       f (get l ⟨n, @length_pmap _ _ p f l h ▸ hn⟩)
-        (h _ (get_mem l ⟨n, @length_pmap _ _ p f l h ▸ hn⟩)) := by
+        (h _ (get_mem l n (@length_pmap _ _ p f l h ▸ hn))) := by
   simp only [get_eq_getElem]
   simp [getElem_pmap]
 

src/Init/Data/List/Lemmas.lean

@@ -503,9 +503,9 @@ theorem getElem?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n : Nat, l[n]? = s
 theorem get?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n, l.get? n = some a :=
   let ⟨⟨n, _⟩, e⟩ := get_of_mem h; ⟨n, e ▸ get?_eq_get _⟩
 
-theorem get_mem : ∀ (l : List α) n, get l n ∈ l
-  | _ :: _, ⟨0, _⟩ => .head ..
-  | _ :: l, ⟨_+1, _⟩ => .tail _ (get_mem l ..)
+theorem get_mem : ∀ (l : List α) n h, get l ⟨n, h⟩ ∈ l
+  | _ :: _, 0, _ => .head ..
+  | _ :: l, _+1, _ => .tail _ (get_mem l ..)
 
 theorem getElem?_mem {l : List α} {n : Nat} {a : α} (e : l[n]? = some a) : a ∈ l :=
   let ⟨_, e⟩ := getElem?_eq_some_iff.1 e; e ▸ getElem_mem ..
@@ -2415,7 +2415,7 @@ theorem forall_mem_replicate {p : α → Prop} {a : α} {n} :
 
 @[simp] theorem getElem_replicate (a : α) {n : Nat} {m} (h : m < (replicate n a).length) :
     (replicate n a)[m] = a :=
-  eq_of_mem_replicate (getElem_mem _)
+  eq_of_mem_replicate (get_mem _ _ _)
 
 @[deprecated getElem_replicate (since := "2024-06-12")]
 theorem get_replicate (a : α) {n : Nat} (m : Fin _) : (replicate n a).get m = a := by

src/Init/Data/Random.lean

@@ -113,10 +113,10 @@ initialize IO.stdGenRef : IO.Ref StdGen ←
   let seed := UInt64.toNat (ByteArray.toUInt64LE! (← IO.getRandomBytes 8))
   IO.mkRef (mkStdGen seed)
 
-def IO.setRandSeed (n : Nat) : BaseIO Unit :=
+def IO.setRandSeed (n : Nat) : IO Unit :=
   IO.stdGenRef.set (mkStdGen n)
 
-def IO.rand (lo hi : Nat) : BaseIO Nat := do
+def IO.rand (lo hi : Nat) : IO Nat := do
   let gen ← IO.stdGenRef.get
   let (r, gen) := randNat gen lo hi
   IO.stdGenRef.set gen

src/Init/Meta.lean

@@ -374,9 +374,6 @@ partial def structEq : Syntax → Syntax → Bool
 instance : BEq Lean.Syntax := ⟨structEq⟩
 instance : BEq (Lean.TSyntax k) := ⟨(·.raw == ·.raw)⟩
 
-/--
-Finds the first `SourceInfo` from the back of `stx` or `none` if no `SourceInfo` can be found.
--/
 partial def getTailInfo? : Syntax → Option SourceInfo
   | atom info _   => info
   | ident info .. => info
@@ -385,39 +382,14 @@ partial def getTailInfo? : Syntax → Option SourceInfo
   | node info _ _    => info
   | _             => none
 
-/--
-Finds the first `SourceInfo` from the back of `stx` or `SourceInfo.none`
-if no `SourceInfo` can be found.
--/
 def getTailInfo (stx : Syntax) : SourceInfo :=
   stx.getTailInfo?.getD SourceInfo.none
 
-/--
-Finds the trailing size of the first `SourceInfo` from the back of `stx`.
-If no `SourceInfo` can be found or the first `SourceInfo` from the back of `stx` contains no
-trailing whitespace, the result is `0`.
--/
 def getTrailingSize (stx : Syntax) : Nat :=
   match stx.getTailInfo? with
   | some (SourceInfo.original (trailing := trailing) ..) => trailing.bsize
   | _ => 0
 
-/--
-Finds the trailing whitespace substring of the first `SourceInfo` from the back of `stx`.
-If no `SourceInfo` can be found or the first `SourceInfo` from the back of `stx` contains
-no trailing whitespace, the result is `none`.
--/
-def getTrailing? (stx : Syntax) : Option Substring :=
-  stx.getTailInfo.getTrailing?
-
-/--
-Finds the tail position of the trailing whitespace of the first `SourceInfo` from the back of `stx`.
-If no `SourceInfo` can be found or the first `SourceInfo` from the back of `stx` contains
-no trailing whitespace and lacks a tail position, the result is `none`.
--/
-def getTrailingTailPos? (stx : Syntax) (canonicalOnly := false) : Option String.Pos :=
-  stx.getTailInfo.getTrailingTailPos? canonicalOnly
-
 /--
   Return substring of original input covering `stx`.
   Result is meaningful only if all involved `SourceInfo.original`s refer to the same string (as is the case after parsing). -/

src/Init/Prelude.lean

@@ -3654,8 +3654,7 @@ namespace SourceInfo
 
 /--
 Gets the position information from a `SourceInfo`, if available.
-If `canonicalOnly` is true, then `.synthetic` syntax with `canonical := false`
-will also return `none`.
+If `originalOnly` is true, then `.synthetic` syntax will also return `none`.
 -/
 def getPos? (info : SourceInfo) (canonicalOnly := false) : Option String.Pos :=
   match info, canonicalOnly with
@@ -3666,8 +3665,7 @@ def getPos? (info : SourceInfo) (canonicalOnly := false) : Option String.Pos :=
 
 /--
 Gets the end position information from a `SourceInfo`, if available.
-If `canonicalOnly` is true, then `.synthetic` syntax with `canonical := false`
-will also return `none`.
+If `originalOnly` is true, then `.synthetic` syntax will also return `none`.
 -/
 def getTailPos? (info : SourceInfo) (canonicalOnly := false) : Option String.Pos :=
   match info, canonicalOnly with
@@ -3676,24 +3674,6 @@ def getTailPos? (info : SourceInfo) (canonicalOnly := false) : Option String.Pos
   | synthetic (endPos := endPos) .., false => some endPos
   | _,                               _     => none
 
-/--
-Gets the substring representing the trailing whitespace of a `SourceInfo`, if available.
--/
-def getTrailing? (info : SourceInfo) : Option Substring :=
-  match info with
-  | original (trailing := trailing) .. => some trailing
-  | _                                  => none
-
-/--
-Gets the end position information of the trailing whitespace of a `SourceInfo`, if available.
-If `canonicalOnly` is true, then `.synthetic` syntax with `canonical := false`
-will also return `none`.
--/
-def getTrailingTailPos? (info : SourceInfo) (canonicalOnly := false) : Option String.Pos :=
-  match info.getTrailing? with
-  | some trailing => some trailing.stopPos
-  | none          => info.getTailPos? canonicalOnly
-
 end SourceInfo
 
 /--
@@ -3992,6 +3972,7 @@ position information.
 def getPos? (stx : Syntax) (canonicalOnly := false) : Option String.Pos :=
   stx.getHeadInfo.getPos? canonicalOnly
 
+
 /--
 Get the ending position of the syntax, if possible.
 If `canonicalOnly` is true, non-canonical `synthetic` nodes are treated as not carrying

src/Lean/Compiler/LCNF/Basic.lean

@@ -366,10 +366,10 @@ to be updated.
 @[implemented_by updateFunDeclCoreImp] opaque FunDeclCore.updateCore (decl: FunDecl) (type : Expr) (params : Array Param) (value : Code) : FunDecl
 
 def CasesCore.extractAlt! (cases : Cases) (ctorName : Name) : Alt × Cases :=
-  let found i := (cases.alts[i], { cases with alts := cases.alts.eraseIdx i })
-  if let some i := cases.alts.findFinIdx? fun | .alt ctorName' .. => ctorName == ctorName' | _ => false then
+  let found (i : Nat) := (cases.alts[i]!, { cases with alts := cases.alts.eraseIdx i })
+  if let some i := cases.alts.findIdx? fun | .alt ctorName' .. => ctorName == ctorName' | _ => false then
     found i
-  else if let some i := cases.alts.findFinIdx? fun | .default _ => true | _ => false then
+  else if let some i := cases.alts.findIdx? fun | .default _ => true | _ => false then
     found i
   else
     unreachable!

src/Lean/Compiler/LCNF/PassManager.lean

@@ -134,9 +134,9 @@ def withEachOccurrence (targetName : Name) (f : Nat → PassInstaller) : PassIns
 
 def installAfter (targetName : Name) (p : Pass → Pass) (occurrence : Nat := 0) : PassInstaller where
   install passes :=
-    if let some idx := passes.findFinIdx? (fun p => p.name == targetName && p.occurrence == occurrence) then
-      let passUnderTest := passes[idx]
-      return passes.insertIdx (idx + 1) (p passUnderTest)
+    if let some idx := passes.findIdx? (fun p => p.name == targetName && p.occurrence == occurrence) then
+      let passUnderTest := passes[idx]!
+      return passes.insertAt! (idx + 1) (p passUnderTest)
     else
       throwError s!"Tried to insert pass after {targetName}, occurrence {occurrence} but {targetName} is not in the pass list"
 
@@ -145,9 +145,9 @@ def installAfterEach (targetName : Name) (p : Pass → Pass) : PassInstaller :=
 
 def installBefore (targetName : Name) (p : Pass → Pass) (occurrence : Nat := 0): PassInstaller where
   install passes :=
-    if let some idx := passes.findFinIdx? (fun p => p.name == targetName && p.occurrence == occurrence) then
-      let passUnderTest := passes[idx]
-      return passes.insertIdx idx (p passUnderTest)
+    if let some idx := passes.findIdx? (fun p => p.name == targetName && p.occurrence == occurrence) then
+      let passUnderTest := passes[idx]!
+      return passes.insertAt! idx (p passUnderTest)
     else
       throwError s!"Tried to insert pass after {targetName}, occurrence {occurrence} but {targetName} is not in the pass list"
 

src/Lean/Compiler/Specialize.lean

@@ -32,7 +32,7 @@ private def elabSpecArgs (declName : Name) (args : Array Syntax) : MetaM (Array
         result := result.push idx
       else
         let argName := arg.getId
-        if let some idx := argNames.indexOf? argName then
+        if let some idx := argNames.getIdx? argName then
           if result.contains idx then throwErrorAt arg "invalid specialization argument name `{argName}`, it has already been specified as a specialization candidate"
           result := result.push idx
         else

src/Lean/Data/Lsp/Basic.lean

@@ -365,7 +365,6 @@ structure TextDocumentRegistrationOptions where
 
 inductive MarkupKind where
   | plaintext | markdown
-  deriving DecidableEq, Hashable
 
 instance : FromJson MarkupKind := ⟨fun
   | str "plaintext" => Except.ok MarkupKind.plaintext
@@ -379,7 +378,7 @@ instance : ToJson MarkupKind := ⟨fun
 structure MarkupContent where
   kind  : MarkupKind
   value : String
-  deriving ToJson, FromJson, DecidableEq, Hashable
+  deriving ToJson, FromJson
 
 /-- Reference to the progress of some in-flight piece of work.
 

src/Lean/Data/Lsp/LanguageFeatures.lean

@@ -25,7 +25,7 @@ inductive CompletionItemKind where
   | unit | value | enum | keyword | snippet
   | color | file | reference | folder | enumMember
   | constant | struct | event | operator | typeParameter
-  deriving Inhabited, DecidableEq, Repr, Hashable
+  deriving Inhabited, DecidableEq, Repr
 
 instance : ToJson CompletionItemKind where
   toJson a := toJson (a.toCtorIdx + 1)
@@ -39,11 +39,11 @@ structure InsertReplaceEdit where
   newText : String
   insert  : Range
   replace : Range
-  deriving FromJson, ToJson, BEq, Hashable
+  deriving FromJson, ToJson
 
 inductive CompletionItemTag where
   | deprecated
-  deriving Inhabited, DecidableEq, Repr, Hashable
+  deriving Inhabited, DecidableEq, Repr
 
 instance : ToJson CompletionItemTag where
   toJson t := toJson (t.toCtorIdx + 1)
@@ -73,7 +73,7 @@ structure CompletionItem where
   commitCharacters? : string[]
   command? : Command
   -/
-  deriving FromJson, ToJson, Inhabited, BEq, Hashable
+  deriving FromJson, ToJson, Inhabited
 
 structure CompletionList where
   isIncomplete : Bool

src/Lean/Data/PersistentHashMap.lean

@@ -233,10 +233,10 @@ partial def eraseAux [BEq α] : Node α β → USize → α → Node α β
   | n@(Node.collision keys vals heq), _, k =>
     match keys.indexOf? k with
     | some idx =>
-      let keys' := keys.eraseIdx idx
-      have keq := keys.size_eraseIdx idx _
-      let vals' := vals.eraseIdx (Eq.ndrec idx heq)
-      have veq := vals.size_eraseIdx (Eq.ndrec idx heq) _
+      let keys' := keys.feraseIdx idx
+      have keq := keys.size_feraseIdx idx
+      let vals' := vals.feraseIdx (Eq.ndrec idx heq)
+      have veq := vals.size_feraseIdx (Eq.ndrec idx heq)
       have : keys.size - 1 = vals.size - 1 := by rw [heq]
       Node.collision keys' vals' (keq.trans (this.trans veq.symm))
     | none     => n

src/Lean/Elab/App.lean

@@ -1347,7 +1347,7 @@ where
     let mut unusableNamedArgs := unusableNamedArgs
     for x in xs, bInfo in bInfos do
       let xDecl ← x.mvarId!.getDecl
-      if let some idx := remainingNamedArgs.findFinIdx? (·.name == xDecl.userName) then
+      if let some idx := remainingNamedArgs.findIdx? (·.name == xDecl.userName) then
         /- If there is named argument with name `xDecl.userName`, then it is accounted for and we can't make use of it. -/
         remainingNamedArgs := remainingNamedArgs.eraseIdx idx
       else
@@ -1355,9 +1355,9 @@ where
           /- We found a type of the form (baseName ...).
              First, we check if the current argument is an explicit one,
              and if the current explicit position "fits" at `args` (i.e., it must be ≤ arg.size) -/
-          if h : argIdx ≤ args.size ∧ bInfo.isExplicit then
+          if argIdx ≤ args.size && bInfo.isExplicit then
             /- We can insert `e` as an explicit argument -/
-            return (args.insertIdx argIdx (Arg.expr e), namedArgs)
+            return (args.insertAt! argIdx (Arg.expr e), namedArgs)
           else
             /- If we can't add `e` to `args`, we try to add it using a named argument, but this is only possible
                if there isn't an argument with the same name occurring before it. -/
@@ -1399,8 +1399,8 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
   let rec loop : Expr → List LVal → TermElabM Expr
   | f, []          => elabAppArgs f namedArgs args expectedType? explicit ellipsis
   | f, lval::lvals => do
-    if let LVal.fieldName (ref := ref) .. := lval then
-      addDotCompletionInfo ref f expectedType?
+    if let LVal.fieldName (fullRef := fullRef) .. := lval then
+      addDotCompletionInfo fullRef f expectedType?
     let hasArgs := !namedArgs.isEmpty || !args.isEmpty
     let (f, lvalRes) ← resolveLVal f lval hasArgs
     match lvalRes with
@@ -1650,14 +1650,6 @@ private def getSuccesses (candidates : Array (TermElabResult Expr)) : TermElabM
 -/
 private def mergeFailures (failures : Array (TermElabResult Expr)) : TermElabM α := do
   let exs := failures.map fun | .error ex _ => ex | _ => unreachable!
-  let trees := failures.map (fun | .error _ s => s.meta.core.infoState.trees | _ => unreachable!)
-    |>.filterMap (·[0]?)
-  -- Retain partial `InfoTree` subtrees in an `.ofChoiceInfo` node in case of multiple failures.
-  -- This ensures that the language server still has `Info` to work with when multiple overloaded
-  -- elaborators fail.
-  withInfoContext (mkInfo := pure <| .ofChoiceInfo { elaborator := .anonymous, stx := ← getRef }) do
-    for tree in trees do
-      pushInfoTree tree
   throwErrorWithNestedErrors "overloaded" exs
 
 private def elabAppAux (f : Syntax) (namedArgs : Array NamedArg) (args : Array Arg) (ellipsis : Bool) (expectedType? : Option Expr) : TermElabM Expr := do

src/Lean/Elab/BuiltinCommand.lean

@@ -211,7 +211,7 @@ private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBin
         else
           `(bracketedBinderF| {$id $[: $ty?]?})
       for id in ids.reverse do
-        if let some idx := binderIds.findFinIdx? fun binderId => binderId.raw.isIdent && binderId.raw.getId == id.raw.getId then
+        if let some idx := binderIds.findIdx? fun binderId => binderId.raw.isIdent && binderId.raw.getId == id.raw.getId then
           binderIds := binderIds.eraseIdx idx
           modifiedVarDecls := true
           varDeclsNew := varDeclsNew.push (← mkBinder id explicit)

src/Lean/Elab/BuiltinTerm.lean

@@ -42,15 +42,16 @@ private def elabOptLevel (stx : Syntax) : TermElabM Level :=
 @[builtin_term_elab «completion»] def elabCompletion : TermElab := fun stx expectedType? => do
   /- `ident.` is ambiguous in Lean, we may try to be completing a declaration name or access a "field". -/
   if stx[0].isIdent then
-    -- Add both an `id` and a `dot` `CompletionInfo` and have the language server figure out which
-    -- one to use.
-    addCompletionInfo <| CompletionInfo.id stx stx[0].getId (danglingDot := true) (← getLCtx) expectedType?
+    /- If we can elaborate the identifier successfully, we assume it is a dot-completion. Otherwise, we treat it as
+       identifier completion with a dangling `.`.
+       Recall that the server falls back to identifier completion when dot-completion fails. -/
     let s ← saveState
     try
       let e ← elabTerm stx[0] none
       addDotCompletionInfo stx e expectedType?
     catch _ =>
       s.restore
+      addCompletionInfo <| CompletionInfo.id stx stx[0].getId (danglingDot := true) (← getLCtx) expectedType?
     throwErrorAt stx[1] "invalid field notation, identifier or numeral expected"
   else
     elabPipeCompletion stx expectedType?
@@ -327,7 +328,7 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
 @[builtin_term_elab withAnnotateTerm] def elabWithAnnotateTerm : TermElab := fun stx expectedType? => do
   match stx with
   | `(with_annotate_term $stx $e) =>
-    withTermInfoContext' .anonymous stx (expectedType? := expectedType?) (elabTerm e expectedType?)
+    withInfoContext' stx (elabTerm e expectedType?) (mkTermInfo .anonymous (expectedType? := expectedType?) stx)
   | _ => throwUnsupportedSyntax
 
 private unsafe def evalFilePathUnsafe (stx : Syntax) : TermElabM System.FilePath :=

src/Lean/Elab/Do.lean

@@ -1518,7 +1518,7 @@ mutual
   -/
   partial def doForToCode (doFor : Syntax) (doElems : List Syntax) : M CodeBlock := do
     let doForDecls := doFor[1].getSepArgs
-    if h : doForDecls.size > 1 then
+    if doForDecls.size > 1 then
       /-
         Expand
         ```

src/Lean/Elab/Extra.lean

@@ -327,18 +327,15 @@ private def toExprCore (t : Tree) : TermElabM Expr := do
   | .term _ trees e =>
     modifyInfoState (fun s => { s with trees := s.trees ++ trees }); return e
   | .binop ref kind f lhs rhs =>
-    withRef ref <|
-      withTermInfoContext' .anonymous ref do
-        mkBinOp (kind == .lazy) f (← toExprCore lhs) (← toExprCore rhs)
+    withRef ref <| withInfoContext' ref (mkInfo := mkTermInfo .anonymous ref) do
+      mkBinOp (kind == .lazy) f (← toExprCore lhs) (← toExprCore rhs)
   | .unop ref f arg =>
-    withRef ref <|
-      withTermInfoContext' .anonymous ref do
-        mkUnOp f (← toExprCore arg)
+    withRef ref <| withInfoContext' ref (mkInfo := mkTermInfo .anonymous ref) do
+      mkUnOp f (← toExprCore arg)
   | .macroExpansion macroName stx stx' nested =>
-    withRef stx <|
-      withTermInfoContext' macroName stx <|
-        withMacroExpansion stx stx' <|
-          toExprCore nested
+    withRef stx <| withInfoContext' stx (mkInfo := mkTermInfo macroName stx) do
+      withMacroExpansion stx stx' do
+        toExprCore nested
 
 /--
   Auxiliary function to decide whether we should coerce `f`'s argument to `maxType` or not.

src/Lean/Elab/InfoTree/Main.lean

@@ -139,16 +139,12 @@ def TermInfo.runMetaM (info : TermInfo) (ctx : ContextInfo) (x : MetaM α) : IO
 
 def TermInfo.format (ctx : ContextInfo) (info : TermInfo) : IO Format := do
   info.runMetaM ctx do
-    let ty : Format ←
-      try
-        Meta.ppExpr (← Meta.inferType info.expr)
-      catch _ =>
-        pure "<failed-to-infer-type>"
+    let ty : Format ← try
+      Meta.ppExpr (← Meta.inferType info.expr)
+    catch _ =>
+      pure "<failed-to-infer-type>"
     return f!"{← Meta.ppExpr info.expr} {if info.isBinder then "(isBinder := true) " else ""}: {ty} @ {formatElabInfo ctx info.toElabInfo}"
 
-def PartialTermInfo.format (ctx : ContextInfo) (info : PartialTermInfo) : Format :=
-  f!"Partial term @ {formatElabInfo ctx info.toElabInfo}"
-
 def CompletionInfo.format (ctx : ContextInfo) (info : CompletionInfo) : IO Format :=
   match info with
   | .dot i (expectedType? := expectedType?) .. => return f!"[.] {← i.format ctx} : {expectedType?}"
@@ -195,13 +191,9 @@ def FieldRedeclInfo.format (ctx : ContextInfo) (info : FieldRedeclInfo) : Format
 def OmissionInfo.format (ctx : ContextInfo) (info : OmissionInfo) : IO Format := do
   return f!"Omission @ {← TermInfo.format ctx info.toTermInfo}\nReason: {info.reason}"
 
-def ChoiceInfo.format (ctx : ContextInfo) (info : ChoiceInfo) : Format :=
-  f!"Choice @ {formatElabInfo ctx info.toElabInfo}"
-
 def Info.format (ctx : ContextInfo) : Info → IO Format
   | ofTacticInfo i         => i.format ctx
   | ofTermInfo i           => i.format ctx
-  | ofPartialTermInfo i    => pure <| i.format ctx
   | ofCommandInfo i        => i.format ctx
   | ofMacroExpansionInfo i => i.format ctx
   | ofOptionInfo i         => i.format ctx
@@ -212,12 +204,10 @@ def Info.format (ctx : ContextInfo) : Info → IO Format
   | ofFVarAliasInfo i      => pure <| i.format
   | ofFieldRedeclInfo i    => pure <| i.format ctx
   | ofOmissionInfo i       => i.format ctx
-  | ofChoiceInfo i         => pure <| i.format ctx
 
 def Info.toElabInfo? : Info → Option ElabInfo
   | ofTacticInfo i         => some i.toElabInfo
   | ofTermInfo i           => some i.toElabInfo
-  | ofPartialTermInfo i    => some i.toElabInfo
   | ofCommandInfo i        => some i.toElabInfo
   | ofMacroExpansionInfo _ => none
   | ofOptionInfo _         => none
@@ -228,7 +218,6 @@ def Info.toElabInfo? : Info → Option ElabInfo
   | ofFVarAliasInfo _      => none
   | ofFieldRedeclInfo _    => none
   | ofOmissionInfo i       => some i.toElabInfo
-  | ofChoiceInfo i         => some i.toElabInfo
 
 /--
   Helper function for propagating the tactic metavariable context to its children nodes.
@@ -322,36 +311,24 @@ def realizeGlobalNameWithInfos (ref : Syntax) (id : Name) : CoreM (List (Name ×
       addConstInfo ref n
   return ns
 
-/--
-Adds a node containing the `InfoTree`s generated by `x` to the `InfoTree`s in `m`.
+/-- Use this to descend a node on the infotree that is being built.
 
-If `x` succeeds and `mkInfo` yields an `Info`, the `InfoTree`s of `x` become subtrees of a node
-containing the `Info` produced by `mkInfo`, which is then added to the `InfoTree`s in `m`.
-If `x` succeeds and `mkInfo` yields an `MVarId`, the `InfoTree`s of `x` are discarded and a `hole`
-node is added to the `InfoTree`s in `m`.
-If `x` fails, the `InfoTree`s of `x` become subtrees of a node containing the `Info` produced by
-`mkInfoOnError`, which is then added to the `InfoTree`s in `m`.
-
-The `InfoTree`s in `m` are reset before `x` is executed and restored with the addition of a new tree
-after `x` is executed.
--/
-def withInfoContext'
-    [MonadFinally m]
-    (x : m α)
-    (mkInfo : α → m (Sum Info MVarId))
-    (mkInfoOnError : m Info) :
-    m α := do
+It saves the current list of trees `t₀` and resets it and then runs `x >>= mkInfo`, producing either an `i : Info` or a hole id.
+Running `x >>= mkInfo` will modify the trees state and produce a new list of trees `t₁`.
+In the `i : Info` case, `t₁` become the children of a node `node i t₁` that is appended to `t₀`.
+ -/
+def withInfoContext' [MonadFinally m] (x : m α) (mkInfo : α → m (Sum Info MVarId)) : m α := do
   if (← getInfoState).enabled then
     let treesSaved ← getResetInfoTrees
     Prod.fst <$> MonadFinally.tryFinally' x fun a? => do
-      let info ← do
-        match a? with
-        | none => pure <| .inl <| ← mkInfoOnError
-        | some a => mkInfo a
-      modifyInfoTrees fun trees =>
-        match info with
-        | Sum.inl info   => treesSaved.push <| InfoTree.node info trees
-        | Sum.inr mvarId => treesSaved.push <| InfoTree.hole mvarId
+      match a? with
+      | none   => modifyInfoTrees fun _ => treesSaved
+      | some a =>
+        let info ← mkInfo a
+        modifyInfoTrees fun trees =>
+          match info with
+          | Sum.inl info   => treesSaved.push <| InfoTree.node info trees
+          | Sum.inr mvarId => treesSaved.push <| InfoTree.hole mvarId
   else
     x
 

src/Lean/Elab/InfoTree/Types.lean

@@ -70,18 +70,6 @@ structure TermInfo extends ElabInfo where
   isBinder : Bool := false
   deriving Inhabited
 
-/--
-Used instead of `TermInfo` when a term couldn't successfully be elaborated,
-and so there is no complete expression available.
-
-The main purpose of `PartialTermInfo` is to ensure that the sub-`InfoTree`s of a failed elaborator
-are retained so that they can still be used in the language server.
--/
-structure PartialTermInfo extends ElabInfo where
-  lctx : LocalContext -- The local context when the term was elaborated.
-  expectedType? : Option Expr
-  deriving Inhabited
-
 structure CommandInfo extends ElabInfo where
   deriving Inhabited
 
@@ -91,7 +79,7 @@ inductive CompletionInfo where
   | dot (termInfo : TermInfo) (expectedType? : Option Expr)
   | id (stx : Syntax) (id : Name) (danglingDot : Bool) (lctx : LocalContext) (expectedType? : Option Expr)
   | dotId (stx : Syntax) (id : Name) (lctx : LocalContext) (expectedType? : Option Expr)
-  | fieldId (stx : Syntax) (id : Option Name) (lctx : LocalContext) (structName : Name)
+  | fieldId (stx : Syntax) (id : Name) (lctx : LocalContext) (structName : Name)
   | namespaceId (stx : Syntax)
   | option (stx : Syntax)
   | endSection (stx : Syntax) (scopeNames : List String)
@@ -177,18 +165,10 @@ regular delaboration settings.
 structure OmissionInfo extends TermInfo where
   reason : String
 
-/--
-Indicates that all overloaded elaborators failed. The subtrees of a `ChoiceInfo` node are the
-partial `InfoTree`s of those failed elaborators. Retaining these partial `InfoTree`s helps
-the language server provide interactivity even when all overloaded elaborators failed.
--/
-structure ChoiceInfo extends ElabInfo where
-
 /-- Header information for a node in `InfoTree`. -/
 inductive Info where
   | ofTacticInfo (i : TacticInfo)
   | ofTermInfo (i : TermInfo)
-  | ofPartialTermInfo (i : PartialTermInfo)
   | ofCommandInfo (i : CommandInfo)
   | ofMacroExpansionInfo (i : MacroExpansionInfo)
   | ofOptionInfo (i : OptionInfo)
@@ -199,7 +179,6 @@ inductive Info where
   | ofFVarAliasInfo (i : FVarAliasInfo)
   | ofFieldRedeclInfo (i : FieldRedeclInfo)
   | ofOmissionInfo (i : OmissionInfo)
-  | ofChoiceInfo (i : ChoiceInfo)
   deriving Inhabited
 
 /-- The InfoTree is a structure that is generated during elaboration and used

src/Lean/Elab/LetRec.lean

@@ -90,12 +90,9 @@ private def elabLetRecDeclValues (view : LetRecView) : TermElabM (Array Expr) :=
       for i in [0:view.binderIds.size] do
         addLocalVarInfo view.binderIds[i]! xs[i]!
       withDeclName view.declName do
-        withInfoContext' view.valStx
-          (mkInfo := (pure <| .inl <| mkBodyInfo view.valStx ·))
-          (mkInfoOnError := (pure <| mkBodyInfo view.valStx none))
-          do
-             let value ← elabTermEnsuringType view.valStx type
-             mkLambdaFVars xs value
+        withInfoContext' view.valStx (mkInfo := (pure <| .inl <| mkBodyInfo view.valStx ·)) do
+          let value ← elabTermEnsuringType view.valStx type
+          mkLambdaFVars xs value
 
 private def registerLetRecsToLift (views : Array LetRecDeclView) (fvars : Array Expr) (values : Array Expr) : TermElabM Unit := do
   let letRecsToLiftCurr := (← get).letRecsToLift

src/Lean/Elab/Match.lean

@@ -644,7 +644,7 @@ where
       if inaccessible? p |>.isSome then
         return mkMData k (← withReader (fun _ => true) (go b))
       else if let some (stx, p) := patternWithRef? p then
-        Elab.withInfoContext' (go p) (mkInfoOnError := mkPartialTermInfo .anonymous stx) fun p => do
+        Elab.withInfoContext' (go p) fun p => do
           /- If `p` is a free variable and we are not inside of an "inaccessible" pattern, this `p` is a binder. -/
           mkTermInfo Name.anonymous stx p (isBinder := p.isFVar && !(← read))
       else

src/Lean/Elab/MutualDef.lean

@@ -283,7 +283,7 @@ private partial def withFunLocalDecls {α} (headers : Array DefViewElabHeader) (
   loop 0 #[]
 
 private def expandWhereStructInst : Macro
-  | whereStx@`(Parser.Command.whereStructInst|where%$whereTk $[$decls:letDecl];* $[$whereDecls?:whereDecls]?) => do
+  | `(Parser.Command.whereStructInst|where $[$decls:letDecl];* $[$whereDecls?:whereDecls]?) => do
     let letIdDecls ← decls.mapM fun stx => match stx with
       | `(letDecl|$_decl:letPatDecl) => Macro.throwErrorAt stx "patterns are not allowed here"
       | `(letDecl|$decl:letEqnsDecl) => expandLetEqnsDecl decl (useExplicit := false)
@@ -300,30 +300,7 @@ private def expandWhereStructInst : Macro
         `(structInstField|$id:ident := $val)
       | stx@`(letIdDecl|_ $_* $[: $_]? := $_) => Macro.throwErrorAt stx "'_' is not allowed here"
       | _ => Macro.throwUnsupported
-
-    let startOfStructureTkInfo : SourceInfo :=
-      match whereTk.getPos? with
-      | some pos => .synthetic pos ⟨pos.byteIdx + 1⟩ true
-      | none => .none
-    -- Position the closing `}` at the end of the trailing whitespace of `where $[$_:letDecl];*`.
-    -- We need an accurate range of the generated structure instance in the generated `TermInfo`
-    -- so that we can determine the expected type in structure field completion.
-    let structureStxTailInfo :=
-      whereStx[1].getTailInfo?
-      <|> whereStx[0].getTailInfo?
-    let endOfStructureTkInfo : SourceInfo :=
-      match structureStxTailInfo with
-      | some (SourceInfo.original _ _ trailing _) =>
-        let tokenPos := trailing.str.prev trailing.stopPos
-        let tokenEndPos := trailing.stopPos
-        .synthetic tokenPos tokenEndPos true
-      | _ => .none
-
     let body ← `(structInst| { $structInstFields,* })
-    let body := body.raw.setInfo <|
-      match startOfStructureTkInfo.getPos?, endOfStructureTkInfo.getTailPos? with
-      | some startPos, some endPos => .synthetic startPos endPos true
-      | _, _ => .none
     match whereDecls? with
     | some whereDecls => expandWhereDecls whereDecls body
     | none => return body
@@ -440,15 +417,12 @@ private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr
           -- Store instantiated body in info tree for the benefit of the unused variables linter
           -- and other metaprograms that may want to inspect it without paying for the instantiation
           -- again
-          withInfoContext' valStx
-            (mkInfo := (pure <| .inl <| mkBodyInfo valStx ·))
-            (mkInfoOnError := (pure <| mkBodyInfo valStx none))
-            do
-              -- synthesize mvars here to force the top-level tactic block (if any) to run
-              let val ← elabTermEnsuringType valStx type <* synthesizeSyntheticMVarsNoPostponing
-              -- NOTE: without this `instantiatedMVars`, `mkLambdaFVars` may leave around a redex that
-              -- leads to more section variables being included than necessary
-              instantiateMVarsProfiling val
+          withInfoContext' valStx (mkInfo := (pure <| .inl <| mkBodyInfo valStx ·)) do
+            -- synthesize mvars here to force the top-level tactic block (if any) to run
+            let val ← elabTermEnsuringType valStx type <* synthesizeSyntheticMVarsNoPostponing
+            -- NOTE: without this `instantiatedMVars`, `mkLambdaFVars` may leave around a redex that
+            -- leads to more section variables being included than necessary
+            instantiateMVarsProfiling val
         let val ← mkLambdaFVars xs val
         if linter.unusedSectionVars.get (← getOptions) && !header.type.hasSorry && !val.hasSorry then
           let unusedVars ← vars.filterMapM fun var => do

src/Lean/Elab/PatternVar.lean

@@ -332,9 +332,9 @@ where
     else
       let accessible := isNextArgAccessible ctx
       let (d, ctx)   := getNextParam ctx
-      match ctx.namedArgs.findFinIdx? fun namedArg => namedArg.name == d.1 with
+      match ctx.namedArgs.findIdx? fun namedArg => namedArg.name == d.1 with
       | some idx =>
-        let arg := ctx.namedArgs[idx]
+        let arg := ctx.namedArgs[idx]!
         let ctx := { ctx with namedArgs := ctx.namedArgs.eraseIdx idx }
         let ctx ← pushNewArg accessible ctx arg.val
         processCtorAppContext ctx

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

@@ -292,9 +292,9 @@ def mkBrecOnApp (positions : Positions) (fnIdx : Nat) (brecOnConst : Nat → Exp
     let packedFTypes ← inferArgumentTypesN positions.size brecOn
     let packedFArgs ← positions.mapMwith PProdN.mkLambdas packedFTypes FArgs
     let brecOn := mkAppN brecOn packedFArgs
-    let some (size, idx) := positions.findSome? fun pos => (pos.size, ·) <$> pos.indexOf? fnIdx
+    let some poss := positions.find? (·.contains fnIdx)
       | throwError "mkBrecOnApp: Could not find {fnIdx} in {positions}"
-    let brecOn ← PProdN.proj size idx brecOn
+    let brecOn ← PProdN.proj poss.size (poss.getIdx? fnIdx).get! brecOn
     mkLambdaFVars ys (mkAppN brecOn otherArgs)
 
 end Lean.Elab.Structural

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

@@ -40,7 +40,7 @@ private partial def post (fixedPrefix : Nat) (argsPacker : ArgsPacker) (funNames
     return TransformStep.done e
   let declName := f.constName!
   let us       := f.constLevels!
-  if let some fidx := funNames.indexOf? declName then
+  if let some fidx := funNames.getIdx? declName then
     let arity := fixedPrefix + argsPacker.varNamess[fidx]!.size
     let e' ← withAppN arity e fun args => do
       let fixedArgs := args[:fixedPrefix]

src/Lean/Elab/Print.lean

@@ -22,7 +22,7 @@ private def levelParamsToMessageData (levelParams : List Name) : MessageData :=
       m := m ++ ", " ++ toMessageData u
     return m ++ "}"
 
-private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (safety : DefinitionSafety) (sig : Bool := true) : CommandElabM MessageData := do
+private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (safety : DefinitionSafety) : CommandElabM MessageData := do
   let m : MessageData :=
     match (← getReducibilityStatus id) with
     | ReducibilityStatus.irreducible => "@[irreducible] "
@@ -38,13 +38,11 @@ private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type
   let (m, id) := match privateToUserName? id with
     | some id => (m ++ "private ", id)
     | none    => (m, id)
-  if sig then
-    return m!"{m}{kind} {id}{levelParamsToMessageData levelParams} : {type}"
-  else
-    return m!"{m}{kind}"
+  let m := m ++ kind ++ " " ++ id ++ levelParamsToMessageData levelParams ++ " : " ++ type
+  pure m
 
-private def mkHeader' (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (isUnsafe : Bool) (sig : Bool := true) : CommandElabM MessageData :=
-  mkHeader kind id levelParams type (if isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe) (sig := sig)
+private def mkHeader' (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (isUnsafe : Bool) : CommandElabM MessageData :=
+  mkHeader kind id levelParams type (if isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe)
 
 private def printDefLike (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (value : Expr) (safety := DefinitionSafety.safe) : CommandElabM Unit := do
   let m ← mkHeader kind id levelParams type safety
@@ -67,63 +65,32 @@ private def printInduct (id : Name) (levelParams : List Name) (numParams : Nat)
     m := m ++ Format.line ++ ctor ++ " : " ++ cinfo.type
   logInfo m
 
-/--
-Computes the origin of a field. Returns its projection function at the origin.
-Multiple parents could be the origin of a field, but we say the first parent that provides it is the one that determines the origin.
--/
-private partial def getFieldOrigin (structName field : Name) : MetaM Name := do
-  let env ← getEnv
-  for parent in getStructureParentInfo env structName do
-    if (findField? env parent.structName field).isSome then
-      return ← getFieldOrigin parent.structName field
-  let some fi := getFieldInfo? env structName field
-    | throwError "no such field {field} in {structName}"
-  return fi.projFn
-
 open Meta in
 private def printStructure (id : Name) (levelParams : List Name) (numParams : Nat) (type : Expr)
-    (isUnsafe : Bool) : CommandElabM Unit := do
-  let env ← getEnv
-  let kind := if isClass env id then "class" else "structure"
-  let header ← mkHeader' kind id levelParams type isUnsafe (sig := false)
-  liftTermElabM <| forallTelescope (← getConstInfo id).type fun params _ =>
-    let s := Expr.const id (levelParams.map .param)
-    withLocalDeclD `self (mkAppN s params) fun self => do
-      let mut m : MessageData := header
-      -- Signature
-      m := m ++ " " ++ .ofFormatWithInfosM do
-        let (stx, infos) ← PrettyPrinter.delabCore s (delab := PrettyPrinter.Delaborator.delabConstWithSignature)
-        pure ⟨← PrettyPrinter.ppTerm ⟨stx⟩, infos⟩
-      m := m ++ Format.line ++ m!"number of parameters: {numParams}"
-      -- Parents
-      let parents := getStructureParentInfo env id
-      unless parents.isEmpty do
-        m := m ++ Format.line ++ "parents:"
-        for parent in parents do
-          let ptype ← inferType (mkApp (mkAppN (.const parent.projFn (levelParams.map .param)) params) self)
-          m := m ++ indentD m!"{.ofConstName parent.projFn (fullNames := true)} : {ptype}"
-      -- Fields
-      let fields := getStructureFieldsFlattened env id (includeSubobjectFields := false)
-      if fields.isEmpty then
-        m := m ++ Format.line ++ "fields: (none)"
-      else
-        m := m ++ Format.line ++ "fields:"
+    (ctor : Name) (fields : Array Name) (isUnsafe : Bool) (isClass : Bool) : CommandElabM Unit := do
+  let kind := if isClass then "class" else "structure"
+  let mut m ← mkHeader' kind id levelParams type isUnsafe
+  m := m ++ Format.line ++ "number of parameters: " ++ toString numParams
+  m := m ++ Format.line ++ "constructor:"
+  let cinfo ← getConstInfo ctor
+  m := m ++ Format.line ++ ctor ++ " : " ++ cinfo.type
+  m := m ++ Format.line ++ "fields:" ++ (← doFields)
+  logInfo m
+where
+  doFields := liftTermElabM do
+    forallTelescope (← getConstInfo id).type fun params _ =>
+      withLocalDeclD `self (mkAppN (Expr.const id (levelParams.map .param)) params) fun self => do
+        let params := params.push self
+        let mut m : MessageData := ""
         for field in fields do
-          let some source := findField? env id field | panic! "missing structure field info"
-          let proj ← getFieldOrigin source field
-          let modifier := if isPrivateName proj then "private " else ""
-          let ftype ← inferType (← mkProjection self field)
-          m := m ++ indentD (m!"{modifier}{.ofConstName proj (fullNames := true)} : {ftype}")
-      -- Constructor
-      let cinfo := getStructureCtor (← getEnv) id
-      let ctorModifier := if isPrivateName cinfo.name then "private " else ""
-      m := m ++ Format.line ++ "constructor:" ++ indentD (ctorModifier ++ .signature cinfo.name)
-      -- Resolution order
-      let resOrder ← getStructureResolutionOrder id
-      if resOrder.size > 1 then
-        m := m ++ Format.line ++ "resolution order:"
-          ++ indentD (MessageData.joinSep (resOrder.map (.ofConstName · (fullNames := true))).toList ", ")
-      logInfo m
+          match getProjFnForField? (← getEnv) id field with
+          | some proj =>
+            let field : Format := if isPrivateName proj then "private " ++ toString field else toString field
+            let cinfo ← getConstInfo proj
+            let ftype ← instantiateForall cinfo.type params
+            m := m ++ Format.line ++ field ++ " : " ++ ftype
+          | none => panic! "missing structure field info"
+        addMessageContext m
 
 private def printIdCore (id : Name) : CommandElabM Unit := do
   let env ← getEnv
@@ -136,10 +103,11 @@ private def printIdCore (id : Name) : CommandElabM Unit := do
   | ConstantInfo.ctorInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constructor" id us t u
   | ConstantInfo.recInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "recursor" id us t u
   | ConstantInfo.inductInfo { levelParams := us, numParams, type := t, ctors, isUnsafe := u, .. } =>
-    if isStructure env id then
-      printStructure id us numParams t u
-    else
-      printInduct id us numParams t ctors u
+    match getStructureInfo? env id with
+    | some { fieldNames, .. } =>
+      let [ctor] := ctors | panic! "structures have only one constructor"
+      printStructure id us numParams t ctor fieldNames u (isClass env id)
+    | none => printInduct id us numParams t ctors u
   | none => throwUnknownId id
 
 private def printId (id : Syntax) : CommandElabM Unit := do

src/Lean/Elab/Quotation.lean

@@ -58,7 +58,7 @@ partial def mkTuple : Array Syntax → TermElabM Syntax
   | #[]  => `(Unit.unit)
   | #[e] => return e
   | es   => do
-    let stx ← mkTuple (es.eraseIdxIfInBounds 0)
+    let stx ← mkTuple (es.eraseIdx 0)
     `(Prod.mk $(es[0]!) $stx)
 
 def resolveSectionVariable (sectionVars : NameMap Name) (id : Name) : List (Name × List String) :=

src/Lean/Elab/StructInst.lean

@@ -186,7 +186,7 @@ def structInstArrayRef := leading_parser "[" >> termParser >>"]"
 ```
 -/
 private def isModifyOp? (stx : Syntax) : TermElabM (Option Syntax) := do
-  let s? ← stx[2][0].getSepArgs.foldlM (init := none) fun s? arg => do
+  let s? ← stx[2].getSepArgs.foldlM (init := none) fun s? arg => do
     /- arg is of the form `structInstFieldAbbrev <|> structInstField` -/
     if arg.getKind == ``Lean.Parser.Term.structInstField then
       /- Remark: the syntax for `structInstField` is
@@ -245,7 +245,7 @@ private def elabModifyOp (stx modifyOp : Syntax) (sources : Array ExplicitSource
     let valField  := modifyOp.setArg 0 <| mkNode ``Parser.Term.structInstLVal #[valFirst, valRest]
     let valSource := mkSourcesWithSyntax #[s]
     let val       := stx.setArg 1 valSource
-    let val       := val.setArg 2 <| mkNode ``Parser.Term.structInstFields #[mkNullNode #[valField]]
+    let val       := val.setArg 2 <| mkNullNode #[valField]
     trace[Elab.struct.modifyOp] "{stx}\nval: {val}"
     cont val
 
@@ -440,7 +440,7 @@ private def mkStructView (stx : Syntax) (structName : Name) (sources : SourcesVi
   /- Recall that `stx` is of the form
      ```
      leading_parser "{" >> optional (atomic (sepBy1 termParser ", " >> " with "))
-                 >> structInstFields (sepByIndent (structInstFieldAbbrev <|> structInstField) ...)
+                 >> sepByIndent (structInstFieldAbbrev <|> structInstField) ...
                  >> optional ".."
                  >> optional (" : " >> termParser)
                  >> " }"
@@ -448,7 +448,7 @@ private def mkStructView (stx : Syntax) (structName : Name) (sources : SourcesVi
 
      This method assumes that `structInstFieldAbbrev` had already been expanded.
   -/
-  let fields ← stx[2][0].getSepArgs.toList.mapM fun fieldStx => do
+  let fields ← stx[2].getSepArgs.toList.mapM fun fieldStx => do
     let val      := fieldStx[2]
     let first    ← toFieldLHS fieldStx[0][0]
     let rest     ← fieldStx[0][1].getArgs.toList.mapM toFieldLHS
@@ -602,9 +602,7 @@ mutual
             let valStx := s.ref -- construct substructure syntax using s.ref as template
             let valStx := valStx.setArg 4 mkNullNode -- erase optional expected type
             let args   := substructFields.toArray.map (·.toSyntax)
-            let fieldsStx := mkNode ``Parser.Term.structInstFields
-              #[mkNullNode <| mkSepArray args (mkAtom ",")]
-            let valStx := valStx.setArg 2 fieldsStx
+            let valStx := valStx.setArg 2 (mkNullNode <| mkSepArray args (mkAtom ","))
             let valStx ← updateSource valStx
             return { field with lhs := [field.lhs.head!], val := FieldVal.term valStx }
   /--

src/Lean/Elab/Syntax.lean

@@ -142,7 +142,7 @@ where
     let args := stx.getArgs
     if (← checkLeftRec stx[0]) then
       if args.size == 1 then throwErrorAt stx "invalid atomic left recursive syntax"
-      let args := args.eraseIdxIfInBounds 0
+      let args := args.eraseIdx 0
       let args ← args.mapM fun arg => withNestedParser do process arg
       mkParserSeq args
     else

src/Lean/Elab/Tactic/Config.lean

@@ -114,13 +114,6 @@ private def elabConfig (recover : Bool) (structName : Name) (items : Array Confi
     let e ← Term.withSynthesize <| Term.elabTermEnsuringType stx (mkConst structName)
     instantiateMVars e
 
-section
--- We automatically disable the following option for `macro`s but the subsequent `def` both contains
--- a quotation and is called only by `macro`s, so we disable the option for it manually. Note that
--- we can't use `in` as it is parsed as a single command and so the option would not influence the
--- parser.
-set_option internal.parseQuotWithCurrentStage false
-
 private def mkConfigElaborator
     (doc? : Option (TSyntax ``Parser.Command.docComment)) (elabName type monadName : Ident)
     (adapt recover : Term) : MacroM (TSyntax `command) := do
@@ -155,8 +148,6 @@ private def mkConfigElaborator
             throwError msg
       go)
 
-end
-
 /-!
 `declare_config_elab elabName TypeName` declares a function `elabName : Syntax → TacticM TypeName`
 that elaborates a tactic configuration.

src/Lean/Elab/Tactic/Induction.lean

@@ -340,9 +340,9 @@ where
     for h : altStxIdx in [0:altStxs.size] do
       let altStx := altStxs[altStxIdx]
       let altName := getAltName altStx
-      if let some i := alts.findFinIdx? (·.1 == altName) then
+      if let some i := alts.findIdx? (·.1 == altName) then
         -- cover named alternative
-        applyAltStx tacSnaps altStxIdx altStx alts[i]
+        applyAltStx tacSnaps altStxIdx altStx alts[i]!
         alts := alts.eraseIdx i
       else if !alts.isEmpty && isWildcard altStx then
         -- cover all alternatives

src/Lean/Elab/Term.lean

@@ -1298,20 +1298,13 @@ def isTacticOrPostponedHole? (e : Expr) : TermElabM (Option MVarId) := do
     | _                                  => return none
   | _ => pure none
 
-def mkTermInfo (elaborator : Name) (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none)
-    (lctx? : Option LocalContext := none) (isBinder := false) :
-    TermElabM (Sum Info MVarId) := do
+def mkTermInfo (elaborator : Name) (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none) (lctx? : Option LocalContext := none) (isBinder := false) : TermElabM (Sum Info MVarId) := do
   match (← isTacticOrPostponedHole? e) with
   | some mvarId => return Sum.inr mvarId
   | none =>
     let e := removeSaveInfoAnnotation e
     return Sum.inl <| Info.ofTermInfo { elaborator, lctx := lctx?.getD (← getLCtx), expr := e, stx, expectedType?, isBinder }
 
-def mkPartialTermInfo (elaborator : Name) (stx : Syntax) (expectedType? : Option Expr := none)
-    (lctx? : Option LocalContext := none) :
-    TermElabM Info := do
-  return Info.ofPartialTermInfo { elaborator, lctx := lctx?.getD (← getLCtx), stx, expectedType? }
-
 /--
 Pushes a new leaf node to the info tree associating the expression `e` to the syntax `stx`.
 As a result, when the user hovers over `stx` they will see the type of `e`, and if `e`
@@ -1333,54 +1326,41 @@ def addTermInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none)
   if (← read).inPattern && !force then
     return mkPatternWithRef e stx
   else
-    discard <| withInfoContext'
-      (pure ())
-      (fun _ => mkTermInfo elaborator stx e expectedType? lctx? isBinder)
-      (mkPartialTermInfo elaborator stx expectedType? lctx?)
+    withInfoContext' (pure ()) (fun _ => mkTermInfo elaborator stx e expectedType? lctx? isBinder) |> discard
     return e
 
 def addTermInfo' (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none) (lctx? : Option LocalContext := none) (elaborator := Name.anonymous) (isBinder := false) : TermElabM Unit :=
   discard <| addTermInfo stx e expectedType? lctx? elaborator isBinder
 
-def withInfoContext' (stx : Syntax) (x : TermElabM Expr)
-    (mkInfo : Expr → TermElabM (Sum Info MVarId)) (mkInfoOnError : TermElabM Info) :
-    TermElabM Expr := do
+def withInfoContext' (stx : Syntax) (x : TermElabM Expr) (mkInfo : Expr → TermElabM (Sum Info MVarId)) : TermElabM Expr := do
   if (← read).inPattern then
     let e ← x
     return mkPatternWithRef e stx
   else
-    Elab.withInfoContext' x mkInfo mkInfoOnError
+    Elab.withInfoContext' x mkInfo
 
 /-- Info node capturing `def/let rec` bodies, used by the unused variables linter. -/
 structure BodyInfo where
-  /-- The body as a fully elaborated term. `none` if the body failed to elaborate. -/
-  value? : Option Expr
+  /-- The body as a fully elaborated term. -/
+  value : Expr
 deriving TypeName
 
 /-- Creates an `Info.ofCustomInfo` node backed by a `BodyInfo`. -/
-def mkBodyInfo (stx : Syntax) (value? : Option Expr) : Info :=
-  .ofCustomInfo { stx, value := .mk { value? : BodyInfo } }
+def mkBodyInfo (stx : Syntax) (value : Expr) : Info :=
+  .ofCustomInfo { stx, value := .mk { value : BodyInfo } }
 
 /-- Extracts a `BodyInfo` custom info. -/
 def getBodyInfo? : Info → Option BodyInfo
   | .ofCustomInfo { value, .. } => value.get? BodyInfo
   | _ => none
 
-def withTermInfoContext' (elaborator : Name) (stx : Syntax) (x : TermElabM Expr)
-    (expectedType? : Option Expr := none) (lctx? : Option LocalContext := none)
-    (isBinder : Bool := false) :
-    TermElabM Expr :=
-  withInfoContext' stx x
-    (mkTermInfo elaborator stx (expectedType? := expectedType?) (lctx? := lctx?) (isBinder := isBinder))
-    (mkPartialTermInfo elaborator stx (expectedType? := expectedType?) (lctx? := lctx?))
-
 /--
 Postpone the elaboration of `stx`, return a metavariable that acts as a placeholder, and
 ensures the info tree is updated and a hole id is introduced.
 When `stx` is elaborated, new info nodes are created and attached to the new hole id in the info tree.
 -/
 def postponeElabTerm (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
-  withTermInfoContext' .anonymous stx (expectedType? := expectedType?) do
+  withInfoContext' stx (mkInfo := mkTermInfo .anonymous (expectedType? := expectedType?) stx) do
     postponeElabTermCore stx expectedType?
 
 /--
@@ -1392,7 +1372,7 @@ private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? :
   | (elabFn::elabFns) =>
     try
       -- record elaborator in info tree, but only when not backtracking to other elaborators (outer `try`)
-      withTermInfoContext' elabFn.declName stx (expectedType? := expectedType?)
+      withInfoContext' stx (mkInfo := mkTermInfo elabFn.declName (expectedType? := expectedType?) stx)
         (try
           elabFn.value stx expectedType?
         catch ex => match ex with
@@ -1775,7 +1755,7 @@ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone :
     let result ← match (← liftMacroM (expandMacroImpl? env stx)) with
     | some (decl, stxNew?) =>
       let stxNew ← liftMacroM <| liftExcept stxNew?
-      withTermInfoContext' decl stx (expectedType? := expectedType?) <|
+      withInfoContext' stx (mkInfo := mkTermInfo decl (expectedType? := expectedType?) stx) <|
         withMacroExpansion stx stxNew <|
           withRef stxNew <|
             elabTermAux expectedType? catchExPostpone implicitLambda stxNew

src/Lean/Level.lean

@@ -599,20 +599,17 @@ def geq (u v : Level) : Bool :=
 where
   go (u v : Level) : Bool :=
     u == v ||
-    let k := fun () =>
-      match v with
-      | imax v₁ v₂ => go u v₁ && go u v₂
-      | _          =>
-        let v' := v.getLevelOffset
-        (u.getLevelOffset == v' || v'.isZero)
-        && u.getOffset ≥ v.getOffset
     match u, v with
-    | _,          zero      => true
-    | u,          max v₁ v₂ => go u v₁ && go u v₂
-    | max u₁ u₂,  v         => go u₁ v || go u₂ v || k ()
-    | imax _  u₂, v         => go u₂ v
-    | succ u,     succ v    => go u v
-    | _,          _         => k ()
+    | _,          zero       => true
+    | u,          max v₁ v₂  => go u v₁ && go u v₂
+    | max u₁ u₂,  v          => go u₁ v || go u₂ v
+    | u,          imax v₁ v₂ => go u v₁ && go u v₂
+    | imax _  u₂, v          => go u₂ v
+    | succ u,     succ v     => go u v
+    | _, _ =>
+      let v' := v.getLevelOffset
+      (u.getLevelOffset == v' || v'.isZero)
+      && u.getOffset ≥ v.getOffset
   termination_by (u, v)
 
 end Level

src/Lean/Linter/UnusedVariables.lean

@@ -393,17 +393,16 @@ where
         | .ofCustomInfo ti =>
           if !linter.unusedVariables.analyzeTactics.get ci.options then
             if let some bodyInfo := ti.value.get? Elab.Term.BodyInfo then
-              if let some value := bodyInfo.value? then
-                -- the body is the only `Expr` we will analyze in this case
-                -- NOTE: we include it even if no tactics are present as at least for parameters we want
-                -- to lint only truly unused binders
-                let (e, _) := instantiateMVarsCore ci.mctx value
-                modify fun s => { s with
-                  assignments := s.assignments.push (.insert {} ⟨.anonymous⟩ e) }
-                let tacticsPresent := children.any (·.findInfo? (· matches .ofTacticInfo ..) |>.isSome)
-                withReader (· || tacticsPresent) do
-                  go children.toArray ci
-                return false
+              -- the body is the only `Expr` we will analyze in this case
+              -- NOTE: we include it even if no tactics are present as at least for parameters we want
+              -- to lint only truly unused binders
+              let (e, _) := instantiateMVarsCore ci.mctx bodyInfo.value
+              modify fun s => { s with
+                assignments := s.assignments.push (.insert {} ⟨.anonymous⟩ e) }
+              let tacticsPresent := children.any (·.findInfo? (· matches .ofTacticInfo ..) |>.isSome)
+              withReader (· || tacticsPresent) do
+                go children.toArray ci
+              return false
         | .ofTermInfo ti =>
           if ignored then return true
           match ti.expr with

src/Lean/Meta/ExprDefEq.lean

@@ -1387,21 +1387,15 @@ private abbrev unfold (e : Expr) (failK : MetaM α) (successK : Expr → MetaM
 /-- Auxiliary method for isDefEqDelta -/
 private def unfoldBothDefEq (fn : Name) (t s : Expr) : MetaM LBool := do
   match t, s with
-  | .const _ ls₁, .const _ ls₂ =>
-    match (← isListLevelDefEq ls₁ ls₂) with
-    | .true => return .true
-    | _ =>
-    unfold t (pure .undef) fun t =>
-    unfold s (pure .undef) fun s =>
-      isDefEqLeftRight fn t s
-  | .app _ _,     .app _ _     =>
+  | Expr.const _ ls₁, Expr.const _ ls₂ => isListLevelDefEq ls₁ ls₂
+  | Expr.app _ _,     Expr.app _ _     =>
     if (← tryHeuristic t s) then
-      return .true
+      pure LBool.true
     else
       unfold t
-       (unfold s (pure .undef) fun s => isDefEqRight fn t s)
+       (unfold s (pure LBool.undef) (fun s => isDefEqRight fn t s))
        (fun t => unfold s (isDefEqLeft fn t s) (fun s => isDefEqLeftRight fn t s))
-  | _, _ => return .false
+  | _, _ => pure LBool.false
 
 private def sameHeadSymbol (t s : Expr) : Bool :=
   match t.getAppFn, s.getAppFn with
@@ -1680,12 +1674,11 @@ private partial def isDefEqQuick (t s : Expr) : MetaM LBool :=
   -- | Expr.mdata _ t _,    s                   => isDefEqQuick t s
   -- | t,                   Expr.mdata _ s _    => isDefEqQuick t s
   | .fvar fvarId₁, .fvar fvarId₂ => do
-    if fvarId₁ == fvarId₂ then
-      return .true
-    else if (← fvarId₁.isLetVar <||> fvarId₂.isLetVar) then
-      return .undef
+    if (← fvarId₁.isLetVar <||> fvarId₂.isLetVar) then
+      return LBool.undef
+    else if fvarId₁ == fvarId₂ then
+      return LBool.true
     else
-      -- If `t` and `s` are not proofs or let-variables, we still return `.undef` and let other rules (e.g., unit-like) kick in.
       isDefEqProofIrrel t s
   | t, s =>
     isDefEqQuickOther t s

src/Lean/Meta/IndPredBelow.lean

@@ -83,7 +83,7 @@ where
       forallTelescopeReducing t fun xs s => do
         let motiveType ← instantiateForall motive xs[:numParams]
         withLocalDecl motiveName BinderInfo.implicit motiveType fun motive => do
-          mkForallFVars (xs.insertIdxIfInBounds numParams motive) s)
+          mkForallFVars (xs.insertAt! numParams motive) s)
 
   motiveType (indVal : InductiveVal) : MetaM Expr :=
     forallTelescopeReducing indVal.type fun xs _ => do

src/Lean/Meta/Match/MatchEqs.lean

@@ -129,9 +129,9 @@ where
           let typeNew := b.instantiate1 y
           if let some (_, lhs, rhs) ← matchEq? d then
             if lhs.isFVar && ys.contains lhs && args.contains lhs && isNamedPatternProof typeNew y then
-               let some j  := ys.indexOf? lhs | unreachable!
+               let some j  := ys.getIdx? lhs | unreachable!
                let ys      := ys.eraseIdx j
-               let some k  := args.indexOf? lhs | unreachable!
+               let some k  := args.getIdx? lhs | unreachable!
                let mask    := mask.set! k false
                let args    := args.map fun arg => if arg == lhs then rhs else arg
                let arg     ← mkEqRefl rhs

src/Lean/Meta/RecursorInfo.lean

@@ -107,7 +107,7 @@ private def getMajorPosDepElim (declName : Name) (majorPos? : Option Nat) (xs :
     if motiveArgs.isEmpty then
       throwError "invalid user defined recursor, '{declName}' does not support dependent elimination, and position of the major premise was not specified (solution: set attribute '[recursor <pos>]', where <pos> is the position of the major premise)"
     let major := motiveArgs.back!
-    match xs.indexOf? major with
+    match xs.getIdx? major with
     | some majorPos => pure (major, majorPos, true)
     | none          => throwError "ill-formed recursor '{declName}'"
 

src/Lean/Meta/Tactic/Clear.lean

@@ -27,7 +27,7 @@ def _root_.Lean.MVarId.clear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId
       throwTacticEx `clear mvarId m!"target depends on '{mkFVar fvarId}'"
     let lctx := lctx.erase fvarId
     let localInsts ← getLocalInstances
-    let localInsts := match localInsts.findFinIdx? fun localInst => localInst.fvar.fvarId! == fvarId with
+    let localInsts := match localInsts.findIdx? fun localInst => localInst.fvar.fvarId! == fvarId with
       | none => localInsts
       | some idx => localInsts.eraseIdx idx
     let newMVar ← mkFreshExprMVarAt lctx localInsts mvarDecl.type MetavarKind.syntheticOpaque tag

src/Lean/Meta/Tactic/TryThis.lean

@@ -430,13 +430,11 @@ def addSuggestions (ref : Syntax) (suggestions : Array Suggestion)
   logInfoAt ref m!"{header}{msgs}"
   addSuggestionCore ref suggestions header (isInline := false) origSpan? style? codeActionPrefix?
 
-private def addExactSuggestionCore (addSubgoalsMsg : Bool) (e : Expr) : MetaM Suggestion :=
-  withOptions (pp.mvars.set · false) do
+private def addExactSuggestionCore (addSubgoalsMsg : Bool) (e : Expr) : MetaM Suggestion := do
   let stx ← delabToRefinableSyntax e
   let mvars ← getMVars e
   let suggestion ← if mvars.isEmpty then `(tactic| exact $stx) else `(tactic| refine $stx)
-  let pp ← ppExpr e
-  let messageData? := if mvars.isEmpty then m!"exact {pp}" else m!"refine {pp}"
+  let messageData? := if mvars.isEmpty then m!"exact {e}" else m!"refine {e}"
   let postInfo? ← if !addSubgoalsMsg || mvars.isEmpty then pure none else
     let mut str := "\nRemaining subgoals:"
     for g in mvars do

src/Lean/MetavarContext.lean

@@ -248,7 +248,9 @@ instance : Hashable LocalInstance where
 
 /-- Remove local instance with the given `fvarId`. Do nothing if `localInsts` does not contain any free variable with id `fvarId`. -/
 def LocalInstances.erase (localInsts : LocalInstances) (fvarId : FVarId) : LocalInstances :=
-  localInsts.eraseP (fun inst => inst.fvar.fvarId! == fvarId)
+  match localInsts.findIdx? (fun inst => inst.fvar.fvarId! == fvarId) with
+  | some idx => localInsts.eraseIdx idx
+  | _        => localInsts
 
 /-- A kind for the metavariable that determines its unification behaviour.
 For more information see the large comment at the beginning of this file. -/

src/Lean/Parser/Command.lean

@@ -137,7 +137,7 @@ def declValEqns      := leading_parser
 def whereStructField := leading_parser
   Term.letDecl
 def whereStructInst  := leading_parser
-  ppIndent ppSpace >> "where" >> Term.structInstFields (sepByIndent (ppGroup whereStructField) "; " (allowTrailingSep := true)) >>
+  ppIndent ppSpace >> "where" >> sepByIndent (ppGroup whereStructField) "; " (allowTrailingSep := true) >>
   optional Term.whereDecls
 /-- `declVal` matches the right-hand side of a declaration, one of:
 * `:= expr` (a "simple declaration")

src/Lean/Parser/Term.lean

@@ -281,12 +281,6 @@ def structInstFieldAbbrev := leading_parser
   atomic (ident >> notFollowedBy ("." <|> ":=" <|> symbol "[") "invalid field abbreviation")
 def optEllipsis      := leading_parser
   optional " .."
-/-
-Tags the structure instance field syntax with a `Lean.Parser.Term.structInstFields` syntax node.
-This node is used to enable structure instance field completion in the whitespace
-of a structure instance notation.
--/
-def structInstFields (p : Parser) : Parser := node `Lean.Parser.Term.structInstFields p
 /--
 Structure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be
 inherited. If `e` is itself a variable called `x`, it can be elided:
@@ -298,7 +292,7 @@ The structure type can be specified if not inferable:
 -/
 @[builtin_term_parser] def structInst := leading_parser
   "{ " >> withoutPosition (optional (atomic (sepBy1 termParser ", " >> " with "))
-    >> structInstFields (sepByIndent (structInstFieldAbbrev <|> structInstField) ", " (allowTrailingSep := true))
+    >> sepByIndent (structInstFieldAbbrev <|> structInstField) ", " (allowTrailingSep := true)
     >> optEllipsis
     >> optional (" : " >> termParser)) >> " }"
 def typeSpec := leading_parser " : " >> termParser
@@ -990,7 +984,6 @@ builtin_initialize
   register_parser_alias bracketedBinder
   register_parser_alias attrKind
   register_parser_alias optSemicolon
-  register_parser_alias structInstFields
 
 end Parser
 end Lean

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -91,32 +91,21 @@ Rather, it is called through the `app` delaborator.
 -/
 def delabConst : Delab := do
   let Expr.const c₀ ls ← getExpr | unreachable!
-  let mut c₀ := c₀
-  let mut c  := c₀
-  if let some n := privateToUserName? c₀ then
-    unless (← getPPOption getPPPrivateNames) do
-      if c₀ == mkPrivateName (← getEnv) n then
-        -- The name is defined in this module, so use `n` as the name and unresolve like any other name.
-        c₀ := n
-        c ← unresolveNameGlobal n (fullNames := ← getPPOption getPPFullNames)
+  let c₀ := if (← getPPOption getPPPrivateNames) then c₀ else (privateToUserName? c₀).getD c₀
+
+  let mut c ← unresolveNameGlobal c₀ (fullNames := ← getPPOption getPPFullNames)
+  let stx ← if ls.isEmpty || !(← getPPOption getPPUniverses) then
+    if (← getLCtx).usesUserName c then
+      -- `c` is also a local declaration
+      if c == c₀ && !(← read).inPattern then
+        -- `c` is the fully qualified named. So, we append the `_root_` prefix
+        c := `_root_ ++ c
       else
-        -- The name is not defined in this module, so make inaccessible. Unresolving does not make sense to do.
-        c ← withFreshMacroScope <| MonadQuotation.addMacroScope n
+        c := c₀
+    pure <| mkIdent c
   else
-    c ← unresolveNameGlobal c (fullNames := ← getPPOption getPPFullNames)
-  let stx ←
-    if ls.isEmpty || !(← getPPOption getPPUniverses) then
-      if (← getLCtx).usesUserName c then
-        -- `c` is also a local declaration
-        if c == c₀ && !(← read).inPattern then
-          -- `c` is the fully qualified named. So, we append the `_root_` prefix
-          c := `_root_ ++ c
-        else
-          c := c₀
-      pure <| mkIdent c
-    else
-      let mvars ← getPPOption getPPMVarsLevels
-      `($(mkIdent c).{$[$(ls.toArray.map (Level.quote · (prec := 0) (mvars := mvars)))],*})
+    let mvars ← getPPOption getPPMVarsLevels
+    `($(mkIdent c).{$[$(ls.toArray.map (Level.quote · (prec := 0) (mvars := mvars)))],*})
 
   let stx ← maybeAddBlockImplicit stx
   if (← getPPOption getPPTagAppFns) then
@@ -349,7 +338,7 @@ def delabAppExplicitCore (fieldNotation : Bool) (numArgs : Nat) (delabHead : (in
     if idx == 0 then
       -- If it's the first argument, then we can tag `obj.field` with the first app.
       head ← withBoundedAppFn (numArgs - 1) <| annotateTermInfo head
-    return Syntax.mkApp head (argStxs.eraseIdxIfInBounds idx)
+    return Syntax.mkApp head (argStxs.eraseIdx idx)
   else
     return Syntax.mkApp fnStx argStxs
 
@@ -876,7 +865,7 @@ def delabLam : Delab :=
           -- "default" binder group is the only one that expects binder names
           -- as a term, i.e. a single `Syntax.ident` or an application thereof
           let stxCurNames ←
-            if h : curNames.size > 1 then
+            if curNames.size > 1 then
               `($(curNames.get! 0) $(curNames.eraseIdx 0)*)
             else
               pure $ curNames.get! 0;

src/Lean/Server/Completion/CompletionCollectors.lean

@@ -1,610 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Marc Huisinga
--/
-prelude
-import Lean.Data.FuzzyMatching
-import Lean.Elab.Tactic.Doc
-import Lean.Server.Completion.CompletionResolution
-import Lean.Server.Completion.EligibleHeaderDecls
-
-namespace Lean.Server.Completion
-open Elab
-open Lean.Lsp
-open Meta
-open FuzzyMatching
-
-section Infrastructure
-
-  structure ScoredCompletionItem where
-    item  : CompletionItem
-    score : Float
-    deriving Inhabited
-
-  private structure Context where
-    params            : CompletionParams
-    completionInfoPos : Nat
-
-
-  /-- Intermediate state while completions are being computed. -/
-  private structure State where
-    /-- All completion items and their fuzzy match scores so far. -/
-    items  : Array ScoredCompletionItem := #[]
-
-  /--
-  Monad used for completion computation that allows modifying a completion `State` and reading
-  `CompletionParams`.
-  -/
-  private abbrev M := ReaderT Context $ StateRefT State MetaM
-
-  /-- Adds a new completion item to the state in `M`. -/
-  private def addItem
-      (item  : CompletionItem)
-      (score : Float)
-      (id?   : Option CompletionIdentifier := none)
-      : M Unit := do
-    let ctx ← read
-    let data := {
-      params := ctx.params,
-      cPos := ctx.completionInfoPos,
-      id?
-      : ResolvableCompletionItemData
-    }
-    let item := { item with data? := toJson data }
-    modify fun s => { s with items := s.items.push ⟨item, score⟩ }
-
-  /--
-  Adds a new completion item with the given `label`, `id`, `kind` and `score` to the state in `M`.
-  Computes the doc string from the environment if available.
-  -/
-  private def addUnresolvedCompletionItem
-      (label         : Name)
-      (id            : CompletionIdentifier)
-      (kind          : CompletionItemKind)
-      (score         : Float)
-      : M Unit := do
-    let env ← getEnv
-    let (docStringPrefix?, tags?) := Id.run do
-      let .const declName := id
-        | (none, none)
-      let some param := Linter.deprecatedAttr.getParam? env declName
-        | (none, none)
-      let docstringPrefix :=
-        if let some text := param.text? then
-          text
-        else if let some newName := param.newName? then
-          s!"`{declName}` has been deprecated, use `{newName}` instead."
-        else
-          s!"`{declName}` has been deprecated."
-      (some docstringPrefix, some #[CompletionItemTag.deprecated])
-    let docString? ← do
-      let .const declName := id
-        | pure none
-      findDocString? env declName
-    let doc? := do
-      let docValue ←
-        match docStringPrefix?, docString? with
-        | none,                 none           => none
-        | some docStringPrefix, none           => docStringPrefix
-        | none,                 docString      => docString
-        | some docStringPrefix, some docString => s!"{docStringPrefix}\n\n{docString}"
-      pure { value := docValue , kind := MarkupKind.markdown : MarkupContent }
-    let item := { label := label.toString, kind? := kind, documentation? := doc?, tags?}
-    addItem item score id
-
-  private def getCompletionKindForDecl (constInfo : ConstantInfo) : M CompletionItemKind := do
-    let env ← getEnv
-    if constInfo.isCtor then
-      return CompletionItemKind.constructor
-    else if constInfo.isInductive then
-      if isClass env constInfo.name then
-        return CompletionItemKind.class
-      else if (← isEnumType constInfo.name) then
-        return CompletionItemKind.enum
-      else
-        return CompletionItemKind.struct
-    else if constInfo.isTheorem then
-      return CompletionItemKind.event
-    else if (← isProjectionFn constInfo.name) then
-      return CompletionItemKind.field
-    else
-      let isFunction : Bool ← withTheReader Core.Context ({ · with maxHeartbeats := 0 }) do
-        return (← whnf constInfo.type).isForall
-      if isFunction then
-        return CompletionItemKind.function
-      else
-        return CompletionItemKind.constant
-
-  private def addUnresolvedCompletionItemForDecl (label : Name) (declName : Name) (score : Float) : M Unit := do
-    if let some c := (← getEnv).find? declName then
-      addUnresolvedCompletionItem label (.const declName) (← getCompletionKindForDecl c) score
-
-  private def addKeywordCompletionItem (keyword : String) (score : Float) : M Unit := do
-    let item := { label := keyword, detail? := "keyword", documentation? := none, kind? := CompletionItemKind.keyword }
-    addItem item score
-
-  private def addNamespaceCompletionItem (ns : Name) (score : Float) : M Unit := do
-    let item := { label := ns.toString, detail? := "namespace", documentation? := none, kind? := CompletionItemKind.module }
-    addItem item score
-
-  private def runM
-      (params            : CompletionParams)
-      (completionInfoPos : Nat)
-      (ctx               : ContextInfo)
-      (lctx              : LocalContext)
-      (x                 : M Unit)
-      : IO (Array ScoredCompletionItem) :=
-    ctx.runMetaM lctx do
-      let (_, s) ← x.run ⟨params, completionInfoPos⟩ |>.run {}
-      return s.items
-
-end Infrastructure
-
-section Utils
-
-  private def normPrivateName? (declName : Name) : MetaM (Option Name) := do
-    match privateToUserName? declName with
-    | none => return declName
-    | some userName =>
-      if mkPrivateName (← getEnv) userName == declName then
-        return userName
-      else
-        return none
-
-  /--
-    Return the auto-completion label if `id` can be auto completed using `declName` assuming namespace `ns` is open.
-    This function only succeeds with atomic labels. BTW, it seems most clients only use the last part.
-
-    Remark: `danglingDot == true` when the completion point is an identifier followed by `.`.
-  -/
-  private def matchDecl? (ns : Name) (id : Name) (danglingDot : Bool) (declName : Name) : MetaM (Option (Name × Float)) := do
-    let some declName ← normPrivateName? declName
-      | return none
-    if !ns.isPrefixOf declName then
-      return none
-    let declName := declName.replacePrefix ns Name.anonymous
-    if danglingDot then
-      -- If the input is `id.` and `declName` is of the form `id.atomic`, complete with `atomicName`
-      if id.isPrefixOf declName then
-        let declName := declName.replacePrefix id Name.anonymous
-        if declName.isAtomic && !declName.isAnonymous then
-          return some (declName, 1)
-    else if let (.str p₁ s₁, .str p₂ s₂) := (id, declName) then
-      if p₁ == p₂ then
-        -- If the namespaces agree, fuzzy-match on the trailing part
-        return fuzzyMatchScoreWithThreshold? s₁ s₂ |>.map (.mkSimple s₂, ·)
-      else if p₁.isAnonymous then
-        -- If `id` is namespace-less, also fuzzy-match declaration names in arbitrary namespaces
-        -- (but don't match the namespace itself).
-        -- Penalize score by component length of added namespace.
-        return fuzzyMatchScoreWithThreshold? s₁ s₂ |>.map (declName, · / (p₂.getNumParts + 1).toFloat)
-    return none
-
-end Utils
-
-section IdCompletionUtils
-
-  private def matchAtomic (id : Name) (declName : Name) (danglingDot : Bool) : Option Float := do
-    if danglingDot then
-      none
-    match id, declName with
-    | .str .anonymous s₁, .str .anonymous s₂ => fuzzyMatchScoreWithThreshold? s₁ s₂
-    | _, _ => none
-
-  /--
-  Truncate the given identifier and make sure it has length `≤ newLength`.
-  This function assumes `id` does not contain `Name.num` constructors.
-  -/
-  private partial def truncate (id : Name) (newLen : Nat) : Name :=
-    let rec go (id : Name) : Name × Nat :=
-      match id with
-      | Name.anonymous => (id, 0)
-      | Name.num ..    => unreachable!
-      | .str p s =>
-        let (p', len) := go p
-        if len + 1 >= newLen then
-          (p', len)
-        else
-          let optDot := if p.isAnonymous then 0 else 1
-          let len'   := len + optDot + s.length
-          if len' ≤ newLen then
-            (id, len')
-          else
-            (Name.mkStr p (s.extract 0 ⟨newLen - optDot - len⟩), newLen)
-    (go id).1
-
-  def matchNamespace (ns : Name) (nsFragment : Name) (danglingDot : Bool) : Option Float :=
-    if danglingDot then
-      if nsFragment != ns && nsFragment.isPrefixOf ns then
-        some 1
-      else
-        none
-    else
-      match ns, nsFragment with
-      | .str p₁ s₁, .str p₂ s₂ =>
-        if p₁ == p₂ then fuzzyMatchScoreWithThreshold? s₂ s₁ else none
-      | _, _ => none
-
-  def completeNamespaces (ctx : ContextInfo) (id : Name) (danglingDot : Bool) : M Unit := do
-    let env ← getEnv
-    let add (ns : Name) (ns' : Name) (score : Float) : M Unit :=
-      if danglingDot then
-        addNamespaceCompletionItem (ns.replacePrefix (ns' ++ id) Name.anonymous) score
-      else
-        addNamespaceCompletionItem (ns.replacePrefix ns' Name.anonymous) score
-    env.getNamespaceSet |>.forM fun ns => do
-      unless ns.isInternal || env.contains ns do -- Ignore internal and namespaces that are also declaration names
-        for openDecl in ctx.openDecls do
-          match openDecl with
-          | OpenDecl.simple ns' _      =>
-            if let some score := matchNamespace ns (ns' ++ id) danglingDot then
-              add ns ns' score
-              return ()
-          | _ => pure ()
-        -- use current namespace
-        let rec visitNamespaces (ns' : Name) : M Unit := do
-          if let some score := matchNamespace ns (ns' ++ id) danglingDot then
-            add ns ns' score
-          else
-            match ns' with
-            | Name.str p .. => visitNamespaces p
-            | _ => return ()
-        visitNamespaces ctx.currNamespace
-
-end IdCompletionUtils
-
-section DotCompletionUtils
-
-  private def unfoldeDefinitionGuarded? (e : Expr) : MetaM (Option Expr) :=
-    try unfoldDefinition? e catch _ => pure none
-
-  /-- Return `true` if `e` is a `declName`-application, or can be unfolded (delta-reduced) to one. -/
-  private partial def isDefEqToAppOf (e : Expr) (declName : Name) : MetaM Bool := do
-    let isConstOf := match e.getAppFn with
-      | .const name .. => (privateToUserName? name).getD name == declName
-      | _ => false
-    if isConstOf then
-      return true
-    let some e ← unfoldeDefinitionGuarded? e | return false
-    isDefEqToAppOf e declName
-
-  private def isDotCompletionMethod (typeName : Name) (info : ConstantInfo) : MetaM Bool :=
-    forallTelescopeReducing info.type fun xs _ => do
-      for x in xs do
-        let localDecl ← x.fvarId!.getDecl
-        let type := localDecl.type.consumeMData
-        if (← isDefEqToAppOf type typeName) then
-          return true
-      return false
-
-  /--
-  Checks whether the expected type of `info.type` can be reduced to an application of `typeName`.
-  -/
-  private def isDotIdCompletionMethod (typeName : Name) (info : ConstantInfo) : MetaM Bool := do
-    forallTelescopeReducing info.type fun _ type =>
-      isDefEqToAppOf type.consumeMData typeName
-
-  /--
-  Converts `n` to `Name.anonymous` if `n` is a private prefix (see `Lean.isPrivatePrefix`).
-  -/
-  private def stripPrivatePrefix (n : Name) : Name :=
-    match n with
-    | .num _ 0 => if isPrivatePrefix n then .anonymous else n
-    | _ => n
-
-  /--
-  Compares `n₁` and `n₂` modulo private prefixes. Similar to `Name.cmp` but ignores all
-  private prefixes in both names.
-  Necessary because the namespaces of private names do not contain private prefixes.
-  -/
-  private partial def cmpModPrivate (n₁ n₂ : Name) : Ordering :=
-    let n₁ := stripPrivatePrefix n₁
-    let n₂ := stripPrivatePrefix n₂
-    match n₁, n₂ with
-    | .anonymous, .anonymous => Ordering.eq
-    | .anonymous, _          => Ordering.lt
-    | _,          .anonymous => Ordering.gt
-    | .num p₁ i₁, .num p₂ i₂ =>
-      match compare i₁ i₂ with
-      | Ordering.eq => cmpModPrivate p₁ p₂
-      | ord         => ord
-    | .num _ _,   .str _ _   => Ordering.lt
-    | .str _ _,   .num _ _   => Ordering.gt
-    | .str p₁ n₁, .str p₂ n₂ =>
-      match compare n₁ n₂ with
-      | Ordering.eq => cmpModPrivate p₁ p₂
-      | ord         => ord
-
-  /--
-  `NameSet` where names are compared according to `cmpModPrivate`.
-  Helps speed up dot completion because it allows us to look up names without first having to
-  strip the private prefix from deep in the name, letting us reject most names without
-  having to scan the full name first.
-  -/
-  private def NameSetModPrivate := RBTree Name cmpModPrivate
-
-  /--
-    Given a type, try to extract relevant type names for dot notation field completion.
-    We extract the type name, parent struct names, and unfold the type.
-    The process mimics the dot notation elaboration procedure at `App.lean` -/
-  private partial def getDotCompletionTypeNames (type : Expr) : MetaM NameSetModPrivate :=
-    return (← visit type |>.run RBTree.empty).2
-  where
-    visit (type : Expr) : StateRefT NameSetModPrivate MetaM Unit := do
-      let .const typeName _ := type.getAppFn | return ()
-      modify fun s => s.insert typeName
-      if isStructure (← getEnv) typeName then
-        for parentName in (← getAllParentStructures typeName) do
-          modify fun s => s.insert parentName
-      let some type ← unfoldeDefinitionGuarded? type | return ()
-      visit type
-
-end DotCompletionUtils
-
-private def idCompletionCore
-    (ctx         : ContextInfo)
-    (stx         : Syntax)
-    (id          : Name)
-    (hoverInfo   : HoverInfo)
-    (danglingDot : Bool)
-    : M Unit := do
-  let mut id := id
-  if id.hasMacroScopes then
-    if stx.getHeadInfo matches .original .. then
-      id := id.eraseMacroScopes
-    else
-      -- Identifier is synthetic and has macro scopes => no completions
-      -- Erasing the macro scopes does not make sense in this case because the identifier name
-      -- is some random synthetic string.
-      return
-  let mut danglingDot := danglingDot
-  if let HoverInfo.inside delta := hoverInfo then
-    id := truncate id delta
-    danglingDot := false
-  if id.isAtomic then
-    -- search for matches in the local context
-    for localDecl in (← getLCtx) do
-      if let some score := matchAtomic id localDecl.userName danglingDot then
-        addUnresolvedCompletionItem localDecl.userName (.fvar localDecl.fvarId) (kind := CompletionItemKind.variable) score
-  -- search for matches in the environment
-  let env ← getEnv
-  forEligibleDeclsM fun declName c => do
-    let bestMatch? ← (·.2) <$> StateT.run (s := none) do
-      let matchUsingNamespace (ns : Name) : StateT (Option (Name × Float)) M Unit := do
-        let some (label, score) ← matchDecl? ns id danglingDot declName
-          | return
-        modify fun
-          | none =>
-            some (label, score)
-          | some (bestLabel, bestScore) =>
-            -- for open namespaces `A` and `A.B` and a decl `A.B.c`, pick the decl `c` over `B.c`
-            if label.isSuffixOf bestLabel then
-              some (label, score)
-            else
-              some (bestLabel, bestScore)
-      let rec visitNamespaces (ns : Name) : StateT (Option (Name × Float)) M Unit := do
-        let Name.str p .. := ns
-          | return ()
-        matchUsingNamespace ns
-        visitNamespaces p
-      -- use current namespace
-      visitNamespaces ctx.currNamespace
-      -- use open decls
-      for openDecl in ctx.openDecls do
-        let OpenDecl.simple ns exs := openDecl
-          | pure ()
-        if exs.contains declName then
-          continue
-        matchUsingNamespace ns
-      matchUsingNamespace Name.anonymous
-    if let some (bestLabel, bestScore) := bestMatch? then
-      addUnresolvedCompletionItem bestLabel (.const declName) (← getCompletionKindForDecl c) bestScore
-  let matchAlias (ns : Name) (alias : Name) : Option Float :=
-    -- Recall that aliases may not be atomic and include the namespace where they were created.
-    if ns.isPrefixOf alias then
-      let alias := alias.replacePrefix ns Name.anonymous
-      matchAtomic id alias danglingDot
-    else
-      none
-  let eligibleHeaderDecls ← getEligibleHeaderDecls env
-  -- Auxiliary function for `alias`
-  let addAlias (alias : Name) (declNames : List Name) (score : Float) : M Unit := do
-    declNames.forM fun declName => do
-      if allowCompletion eligibleHeaderDecls env declName then
-        addUnresolvedCompletionItemForDecl (.mkSimple alias.getString!) declName score
-  -- search explicitly open `ids`
-  for openDecl in ctx.openDecls do
-    match openDecl with
-    | OpenDecl.explicit openedId resolvedId =>
-      if allowCompletion eligibleHeaderDecls env resolvedId then
-        if let some score := matchAtomic id openedId danglingDot then
-          addUnresolvedCompletionItemForDecl (.mkSimple openedId.getString!) resolvedId score
-    | OpenDecl.simple ns _      =>
-      getAliasState env |>.forM fun alias declNames => do
-        if let some score := matchAlias ns alias then
-          addAlias alias declNames score
-  -- search for aliases
-  getAliasState env |>.forM fun alias declNames => do
-    -- use current namespace
-    let rec searchAlias (ns : Name) : M Unit := do
-      if let some score := matchAlias ns alias then
-        addAlias alias declNames score
-      else
-        match ns with
-        | Name.str p ..  => searchAlias p
-        | _ => return ()
-    searchAlias ctx.currNamespace
-  -- Search keywords
-  if !danglingDot then
-    if let .str .anonymous s := id then
-      let keywords := Parser.getTokenTable env
-      for keyword in keywords.findPrefix s do
-        if let some score := fuzzyMatchScoreWithThreshold? s keyword then
-          addKeywordCompletionItem keyword score
-  -- Search namespaces
-  completeNamespaces ctx id danglingDot
-
-def idCompletion
-    (params            : CompletionParams)
-    (completionInfoPos : Nat)
-    (ctx               : ContextInfo)
-    (lctx              : LocalContext)
-    (stx               : Syntax)
-    (id                : Name)
-    (hoverInfo         : HoverInfo)
-    (danglingDot       : Bool)
-    : IO (Array ScoredCompletionItem) :=
-  runM params completionInfoPos ctx lctx do
-    idCompletionCore ctx stx id hoverInfo danglingDot
-
-def dotCompletion
-    (params            : CompletionParams)
-    (completionInfoPos : Nat)
-    (ctx               : ContextInfo)
-    (info              : TermInfo)
-    : IO (Array ScoredCompletionItem) :=
-  runM params completionInfoPos ctx info.lctx do
-    let nameSet ← try
-      getDotCompletionTypeNames (← instantiateMVars (← inferType info.expr))
-    catch _ =>
-      pure RBTree.empty
-    if nameSet.isEmpty then
-      return
-
-    forEligibleDeclsM fun declName c => do
-      let unnormedTypeName := declName.getPrefix
-      if ! nameSet.contains unnormedTypeName then
-        return
-      let some declName ← normPrivateName? declName
-        | return
-      let typeName := declName.getPrefix
-      if ! (← isDotCompletionMethod typeName c) then
-        return
-      let completionKind ← getCompletionKindForDecl c
-      addUnresolvedCompletionItem (.mkSimple c.name.getString!) (.const c.name) (kind := completionKind) 1
-
-def dotIdCompletion
-    (params            : CompletionParams)
-    (completionInfoPos : Nat)
-    (ctx               : ContextInfo)
-    (lctx              : LocalContext)
-    (id                : Name)
-    (expectedType?     : Option Expr)
-    : IO (Array ScoredCompletionItem) :=
-  runM params completionInfoPos ctx lctx do
-    let some expectedType := expectedType?
-      | return ()
-
-    let resultTypeFn := (← instantiateMVars expectedType).cleanupAnnotations.getAppFn.cleanupAnnotations
-    let .const .. := resultTypeFn
-      | return ()
-
-    let nameSet ← try
-      getDotCompletionTypeNames resultTypeFn
-    catch _ =>
-      pure RBTree.empty
-
-    forEligibleDeclsM fun declName c => do
-      let unnormedTypeName := declName.getPrefix
-      if ! nameSet.contains unnormedTypeName then
-        return
-
-      let some declName ← normPrivateName? declName
-        | return
-
-      let typeName := declName.getPrefix
-      if ! (← isDotIdCompletionMethod typeName c) then
-        return
-
-      let completionKind ← getCompletionKindForDecl c
-      if id.isAnonymous then
-        -- We're completing a lone dot => offer all decls of the type
-        addUnresolvedCompletionItem (.mkSimple c.name.getString!) (.const c.name) completionKind 1
-        return
-
-      let some (label, score) ← matchDecl? typeName id (danglingDot := false) declName | pure ()
-      addUnresolvedCompletionItem label (.const c.name) completionKind score
-
-def fieldIdCompletion
-    (params            : CompletionParams)
-    (completionInfoPos : Nat)
-    (ctx               : ContextInfo)
-    (lctx              : LocalContext)
-    (id                : Option Name)
-    (structName        : Name)
-    : IO (Array ScoredCompletionItem) :=
-  runM params completionInfoPos ctx lctx do
-    let idStr := id.map (·.toString) |>.getD ""
-    let fieldNames := getStructureFieldsFlattened (← getEnv) structName (includeSubobjectFields := false)
-    for fieldName in fieldNames do
-      let .str _ fieldName := fieldName | continue
-      let some score := fuzzyMatchScoreWithThreshold? idStr fieldName | continue
-      let item := { label := fieldName, detail? := "field", documentation? := none, kind? := CompletionItemKind.field }
-      addItem item score
-
-def optionCompletion
-    (params            : CompletionParams)
-    (completionInfoPos : Nat)
-    (ctx               : ContextInfo)
-    (stx               : Syntax)
-    (caps              : ClientCapabilities)
-    : IO (Array ScoredCompletionItem) :=
-  ctx.runMetaM {} do
-    let (partialName, trailingDot) :=
-      -- `stx` is from `"set_option" >> ident`
-      match stx[1].getSubstring? (withLeading := false) (withTrailing := false) with
-      | none => ("", false)  -- the `ident` is `missing`, list all options
-      | some ss =>
-        if !ss.str.atEnd ss.stopPos && ss.str.get ss.stopPos == '.' then
-          -- include trailing dot, which is not parsed by `ident`
-          (ss.toString ++ ".", true)
-        else
-          (ss.toString, false)
-    -- HACK(WN): unfold the type so ForIn works
-    let (decls : RBMap _ _ _) ← getOptionDecls
-    let opts ← getOptions
-    let mut items := #[]
-    for ⟨name, decl⟩ in decls do
-      if let some score := fuzzyMatchScoreWithThreshold? partialName name.toString then
-        let textEdit :=
-          if !caps.textDocument?.any (·.completion?.any (·.completionItem?.any (·.insertReplaceSupport?.any (·)))) then
-            none -- InsertReplaceEdit not supported by client
-          else if let some ⟨start, stop⟩ := stx[1].getRange? then
-            let stop := if trailingDot then stop + ' ' else stop
-            let range := ⟨ctx.fileMap.utf8PosToLspPos start, ctx.fileMap.utf8PosToLspPos stop⟩
-            some { newText := name.toString, insert := range, replace := range : InsertReplaceEdit }
-          else
-            none
-        items := items.push ⟨{
-            label := name.toString
-            detail? := s!"({opts.get name decl.defValue}), {decl.descr}"
-            documentation? := none,
-            kind? := CompletionItemKind.property -- TODO: investigate whether this is the best kind for options.
-            textEdit? := textEdit
-            data? := toJson {
-              params,
-              cPos := completionInfoPos,
-              id? := none : ResolvableCompletionItemData
-            }
-          }, score⟩
-    return items
-
-def tacticCompletion
-    (params            : CompletionParams)
-    (completionInfoPos : Nat)
-    (ctx               : ContextInfo)
-    : IO (Array ScoredCompletionItem) := ctx.runMetaM .empty do
-  let allTacticDocs ← Tactic.Doc.allTacticDocs
-  let items : Array ScoredCompletionItem := allTacticDocs.map fun tacticDoc =>
-    ⟨{
-      label          := tacticDoc.userName
-      detail?        := none
-      documentation? := tacticDoc.docString.map fun docString =>
-        { value := docString, kind := MarkupKind.markdown : MarkupContent }
-      kind?          := CompletionItemKind.keyword
-      data?          := toJson { params, cPos := completionInfoPos, id? := none : ResolvableCompletionItemData }
-    }, 1⟩
-  return items
-
-end Lean.Server.Completion

src/Lean/Server/Completion/CompletionInfoSelection.lean

@@ -1,131 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Marc Huisinga
--/
-prelude
-import Lean.Server.Completion.SyntheticCompletion
-
-namespace Lean.Server.Completion
-open Elab
-
-private def filterDuplicateCompletionInfos
-    (infos : Array ContextualizedCompletionInfo)
-    : Array ContextualizedCompletionInfo := Id.run do
-  -- We don't expect there to be too many duplicate completion infos,
-  -- so it's fine if this is quadratic (we don't need to implement `Hashable` / `LT` this way).
-  let mut deduplicatedInfos : Array ContextualizedCompletionInfo := #[]
-  for i in infos do
-    if deduplicatedInfos.any (fun di => eq di.info i.info) then
-      continue
-    deduplicatedInfos := deduplicatedInfos.push i
-  deduplicatedInfos
-where
-  eq : CompletionInfo → CompletionInfo → Bool
-    | .dot ti₁ .., .dot ti₂ .. =>
-      ti₁.stx.eqWithInfo ti₂.stx && ti₁.expr == ti₂.expr
-    | .id stx₁ id₁ .., .id stx₂ id₂ .. =>
-      stx₁.eqWithInfo stx₂ && id₁ == id₂
-    | .dotId stx₁ id₁ .., .id stx₂ id₂ .. =>
-      stx₁.eqWithInfo stx₂ && id₁ == id₂
-    | .fieldId stx₁ id₁? _ structName₁, .fieldId stx₂ id₂? _ structName₂ =>
-      stx₁.eqWithInfo stx₂ && id₁? == id₂? && structName₁ == structName₂
-    | .namespaceId stx₁, .namespaceId stx₂ =>
-      stx₁.eqWithInfo stx₂
-    | .option stx₁, .option stx₂ =>
-      stx₁.eqWithInfo stx₂
-    | .endSection stx₁ scopeNames₁, .endSection stx₂ scopeNames₂ =>
-      stx₁.eqWithInfo stx₂ && scopeNames₁ == scopeNames₂
-    | .tactic stx₁, .tactic stx₂ =>
-      stx₁.eqWithInfo stx₂
-    | _, _ =>
-      false
-
-def findCompletionInfosAt
-    (fileMap  : FileMap)
-    (hoverPos : String.Pos)
-    (cmdStx   : Syntax)
-    (infoTree : InfoTree)
-    : Array ContextualizedCompletionInfo := Id.run do
-  let ⟨hoverLine, _⟩ := fileMap.toPosition hoverPos
-  let mut completionInfoCandidates := infoTree.foldInfo (init := #[]) (go hoverLine)
-  if completionInfoCandidates.isEmpty then
-    completionInfoCandidates := findSyntheticCompletions fileMap hoverPos cmdStx infoTree
-  return filterDuplicateCompletionInfos completionInfoCandidates
-where
-  go
-      (hoverLine : Nat)
-      (ctx       : ContextInfo)
-      (info      : Info)
-      (best     : Array ContextualizedCompletionInfo)
-      : Array ContextualizedCompletionInfo := Id.run do
-    let .ofCompletionInfo completionInfo := info
-      | return best
-    if ! info.occursInOrOnBoundary hoverPos then
-      return best
-    let headPos := info.pos?.get!
-    let tailPos := info.tailPos?.get!
-    let hoverInfo :=
-      if hoverPos < tailPos then
-        HoverInfo.inside (hoverPos - headPos).byteIdx
-      else
-        HoverInfo.after
-    let ⟨headPosLine, _⟩ := fileMap.toPosition headPos
-    let ⟨tailPosLine, _⟩ := fileMap.toPosition info.tailPos?.get!
-    if headPosLine != hoverLine || headPosLine != tailPosLine then
-      return best
-    return best.push { hoverInfo, ctx, info := completionInfo }
-
-private def computePrioritizedCompletionPartitions
-    (items : Array (ContextualizedCompletionInfo × Nat))
-    : Array (Array (ContextualizedCompletionInfo × Nat)) :=
-  let partitions := items.groupByKey fun (i, _) =>
-    let isId := i.info matches .id ..
-    let size? := Info.ofCompletionInfo i.info |>.size?
-    (isId, size?)
-  -- Sort partitions so that non-id completions infos come before id completion infos and
-  -- within those two groups, smaller sizes come before larger sizes.
-  let partitionsByPriority := partitions.toArray.qsort
-    fun ((isId₁, size₁?), _) ((isId₂, size₂?), _) =>
-      match size₁?, size₂? with
-      | some _, none   => true
-      | none,   some _ => false
-      | _, _ =>
-        match isId₁, isId₂ with
-        | false, true  => true
-        | true,  false => false
-        | _,     _     => Id.run do
-          let some size₁ := size₁?
-            | return false
-          let some size₂ := size₂?
-            | return false
-          return size₁ < size₂
-  partitionsByPriority.map (·.2)
-
-/--
-Finds all `CompletionInfo`s (both from the `InfoTree` and synthetic ones), prioritizes them,
-arranges them in partitions of `CompletionInfo`s with the same priority and sorts these partitions
-so that `CompletionInfo`s with the highest priority come first.
-The returned `CompletionInfo`s are also tagged with their index in `findCompletionInfosAt` so that
-when resolving a `CompletionItem`, we can reconstruct which `CompletionInfo` it was created from.
-
-In general, the `InfoTree` may contain multiple different `CompletionInfo`s covering `hoverPos`,
-and so we need to decide which of these `CompletionInfo`s we want to use to show completions to the
-user. We choose priorities by the following rules:
-- Synthetic completions have the lowest priority since they are only intended as a backup.
-- Non-identifier completions have the highest priority since they tend to be much more helpful than
-  identifier completions when available since there are typically way too many of the latter.
-- Within the three groups [non-id completions, id completions, synthetic completions],
-  `CompletionInfo`s with a smaller range are considered to be better.
--/
-def findPrioritizedCompletionPartitionsAt
-    (fileMap  : FileMap)
-    (hoverPos : String.Pos)
-    (cmdStx   : Syntax)
-    (infoTree : InfoTree)
-    : Array (Array (ContextualizedCompletionInfo × Nat)) :=
-  findCompletionInfosAt fileMap hoverPos cmdStx infoTree
-    |>.zipWithIndex
-    |> computePrioritizedCompletionPartitions
-
-end Lean.Server.Completion

src/Lean/Server/Completion/CompletionResolution.lean

@@ -1,91 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Marc Huisinga
--/
-prelude
-import Lean.Server.Completion.CompletionItemData
-import Lean.Server.Completion.CompletionInfoSelection
-
-namespace Lean.Lsp
-
-/--
-Identifier that is sent from the server to the client as part of the `CompletionItem.data?` field.
-Needed to resolve the `CompletionItem` when the client sends a `completionItem/resolve` request
-for that item, again containing the `data?` field provided by the server.
--/
-inductive CompletionIdentifier where
-  | const (declName : Name)
-  | fvar  (id       : FVarId)
-  deriving FromJson, ToJson
-
-/--
-`CompletionItemData` that contains additional information to identify the item
-in order to resolve it.
--/
-structure ResolvableCompletionItemData extends CompletionItemData where
-  /-- Position of the completion info that this completion item was created from. -/
-  cPos : Nat
-  id?  : Option CompletionIdentifier
-  deriving FromJson, ToJson
-
-private partial def consumeImplicitPrefix (e : Expr) (k : Expr → MetaM α) : MetaM α := do
-  match e with
-  | Expr.forallE n d b c =>
-    -- We do not consume instance implicit arguments because the user probably wants be aware of this dependency
-    if c == .implicit then
-      Meta.withLocalDecl n c d fun arg =>
-        consumeImplicitPrefix (b.instantiate1 arg) k
-    else
-      k e
-  | _ => k e
-
-/--
-Fills the `CompletionItem.detail?` field of `item` using the pretty-printed type identified by `id`.
--/
-def CompletionItem.resolve
-    (item : CompletionItem)
-    (id   : CompletionIdentifier)
-    : MetaM CompletionItem := do
-  let env ← getEnv
-  let lctx ← getLCtx
-  let mut item := item
-
-  if item.detail?.isNone then
-    let type? := match id with
-      | .const declName =>
-        env.find? declName |>.map ConstantInfo.type
-      | .fvar id =>
-        lctx.find? id |>.map LocalDecl.type
-    let detail? ← type?.mapM fun type =>
-      consumeImplicitPrefix type fun typeWithoutImplicits =>
-        return toString (← Meta.ppExpr typeWithoutImplicits)
-    item := { item with detail? := detail? }
-
-  return item
-
-end Lean.Lsp
-
-namespace Lean.Server.Completion
-open Lean.Lsp
-open Elab
-
-/--
-Fills the `CompletionItem.detail?` field of `item` using the pretty-printed type identified by `id`
-in the context found at `hoverPos` in `infoTree`.
--/
-def resolveCompletionItem?
-    (fileMap           : FileMap)
-    (hoverPos          : String.Pos)
-    (cmdStx            : Syntax)
-    (infoTree          : InfoTree)
-    (item              : CompletionItem)
-    (id                : CompletionIdentifier)
-    (completionInfoPos : Nat)
-    : IO CompletionItem := do
-  let completionInfos := findCompletionInfosAt fileMap hoverPos cmdStx infoTree
-  let some i := completionInfos.get? completionInfoPos
-    | return item
-  i.ctx.runMetaM i.info.lctx (item.resolve id)
-
-end Lean.Server.Completion

src/Lean/Server/Completion/CompletionUtils.lean

@@ -1,22 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Marc Huisinga
--/
-prelude
-import Init.Prelude
-import Lean.Elab.InfoTree.Types
-
-namespace Lean.Server.Completion
-open Elab
-
-inductive HoverInfo : Type where
-  | after
-  | inside (delta : Nat)
-
-structure ContextualizedCompletionInfo where
-  hoverInfo : HoverInfo
-  ctx       : ContextInfo
-  info      : CompletionInfo
-
-end Lean.Server.Completion

src/Lean/Server/Completion/EligibleHeaderDecls.lean

@@ -1,53 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Marc Huisinga
--/
-prelude
-import Lean.Meta.CompletionName
-
-namespace Lean.Server.Completion
-open Meta
-
-abbrev EligibleHeaderDecls := Std.HashMap Name ConstantInfo
-
-/-- Cached header declarations for which `allowCompletion headerEnv decl` is true. -/
-builtin_initialize eligibleHeaderDeclsRef : IO.Ref (Option EligibleHeaderDecls) ←
-  IO.mkRef none
-
-/--
-Returns the declarations in the header for which `allowCompletion env decl` is true, caching them
-if not already cached.
--/
-def getEligibleHeaderDecls (env : Environment) : IO EligibleHeaderDecls := do
-  eligibleHeaderDeclsRef.modifyGet fun
-    | some eligibleHeaderDecls => (eligibleHeaderDecls, some eligibleHeaderDecls)
-    | none =>
-      let (_, eligibleHeaderDecls) :=
-        StateT.run (m := Id) (s := {}) do
-          -- `map₁` are the header decls
-          env.constants.map₁.forM fun declName c => do
-            modify fun eligibleHeaderDecls =>
-              if allowCompletion env declName then
-                eligibleHeaderDecls.insert declName c
-              else
-                eligibleHeaderDecls
-      (eligibleHeaderDecls, some eligibleHeaderDecls)
-
-/-- Iterate over all declarations that are allowed in completion results. -/
-def forEligibleDeclsM [Monad m] [MonadEnv m] [MonadLiftT (ST IO.RealWorld) m]
-    [MonadLiftT IO m] (f : Name → ConstantInfo → m PUnit) : m PUnit := do
-  let env ← getEnv
-  (← getEligibleHeaderDecls env).forM f
-  -- map₂ are exactly the local decls
-  env.constants.map₂.forM fun name c => do
-    if allowCompletion env name then
-      f name c
-
-/-- Checks whether this declaration can appear in completion results. -/
-def allowCompletion (eligibleHeaderDecls : EligibleHeaderDecls) (env : Environment)
-    (declName : Name) : Bool :=
-  eligibleHeaderDecls.contains declName ||
-    env.constants.map₂.contains declName && Lean.Meta.allowCompletion env declName
-
-end Lean.Server.Completion

src/Lean/Server/Completion/SyntheticCompletion.lean

@@ -1,396 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Marc Huisinga
--/
-prelude
-import Lean.Server.InfoUtils
-import Lean.Server.Completion.CompletionUtils
-
-namespace Lean.Server.Completion
-open Elab
-
-private def findBest?
-    (infoTree : InfoTree)
-    (gt : α → α → Bool)
-    (f : ContextInfo → Info → PersistentArray InfoTree → Option α)
-    : Option α :=
-  infoTree.visitM (m := Id) (postNode := choose) |>.join
-where
-  choose
-      (ctx : ContextInfo)
-      (info : Info)
-      (cs : PersistentArray InfoTree)
-      (childValues : List (Option (Option α)))
-      : Option α :=
-    let bestChildValue := childValues.map (·.join) |>.foldl (init := none) fun v best =>
-      if isBetter v best then
-        v
-      else
-        best
-    if let some v := f ctx info cs then
-      if isBetter v bestChildValue then
-        v
-      else
-        bestChildValue
-    else
-      bestChildValue
-  isBetter (a b : Option α) : Bool :=
-    match a, b with
-    | none,   none   => false
-    | some _, none   => true
-    | none,   some _ => false
-    | some a, some b => gt a b
-
-/--
-If there are `Info`s that contain `hoverPos` and have a nonempty `LocalContext`,
-yields the closest one of those `Info`s.
-Otherwise, yields the closest `Info` that contains `hoverPos` and has an empty `LocalContext`.
--/
-private def findClosestInfoWithLocalContextAt?
-    (hoverPos : String.Pos)
-    (infoTree : InfoTree)
-    : Option (ContextInfo × Info) :=
-  findBest? infoTree isBetter fun ctx info _ =>
-    if info.occursInOrOnBoundary hoverPos then
-      (ctx, info)
-    else
-      none
-where
-  isBetter (a b : ContextInfo × Info) : Bool :=
-    let (_, ia) := a
-    let (_, ib) := b
-    if !ia.lctx.isEmpty && ib.lctx.isEmpty then
-      true
-    else if ia.lctx.isEmpty && !ib.lctx.isEmpty then
-      false
-    else if ia.isSmaller ib then
-      true
-    else if ib.isSmaller ia then
-      false
-    else
-      false
-
-private def findSyntheticIdentifierCompletion?
-    (hoverPos : String.Pos)
-    (infoTree : InfoTree)
-    : Option ContextualizedCompletionInfo := do
-  let some (ctx, info) := findClosestInfoWithLocalContextAt? hoverPos infoTree
-    | none
-  let some stack := info.stx.findStack? (·.getRange?.any (·.contains hoverPos (includeStop := true)))
-    | none
-  let stack := stack.dropWhile fun (stx, _) => !(stx matches `($_:ident) || stx matches `($_:ident.))
-  let some (stx, _) := stack.head?
-    | none
-  let isDotIdCompletion := stack.any fun (stx, _) => stx matches `(.$_:ident)
-  if isDotIdCompletion then
-    -- An identifier completion is never useful in a dotId completion context.
-    none
-  let some (id, danglingDot) :=
-      match stx with
-      | `($id:ident) => some (id.getId, false)
-      | `($id:ident.) => some (id.getId, true)
-      | _ => none
-    | none
-  let tailPos := stx.getTailPos?.get!
-  let hoverInfo :=
-    if hoverPos < tailPos then
-      HoverInfo.inside (tailPos - hoverPos).byteIdx
-    else
-      HoverInfo.after
-  some { hoverInfo, ctx, info := .id stx id danglingDot info.lctx none }
-
-private partial def getIndentationAmount (fileMap : FileMap) (line : Nat) : Nat := Id.run do
-  let lineStartPos := fileMap.lineStart line
-  let lineEndPos := fileMap.lineStart (line + 1)
-  let mut it : String.Iterator := ⟨fileMap.source, lineStartPos⟩
-  let mut indentationAmount := 0
-  while it.pos < lineEndPos do
-    let c := it.curr
-    if c = ' ' || c = '\t' then
-      indentationAmount := indentationAmount + 1
-    else
-      break
-    it := it.next
-  return indentationAmount
-
-private partial def isCursorOnWhitespace (fileMap : FileMap) (hoverPos : String.Pos) : Bool :=
-  fileMap.source.atEnd hoverPos || (fileMap.source.get hoverPos).isWhitespace
-
-private partial def isCursorInProperWhitespace (fileMap : FileMap) (hoverPos : String.Pos) : Bool :=
-  (fileMap.source.atEnd hoverPos || (fileMap.source.get hoverPos).isWhitespace)
-    && (fileMap.source.get (hoverPos - ⟨1⟩)).isWhitespace
-
-private partial def isSyntheticTacticCompletion
-    (fileMap  : FileMap)
-    (hoverPos : String.Pos)
-    (cmdStx   : Syntax)
-    : Bool := Id.run do
-  let hoverFilePos := fileMap.toPosition hoverPos
-  let mut hoverLineIndentation := getIndentationAmount fileMap hoverFilePos.line
-  if hoverFilePos.column < hoverLineIndentation then
-    -- Ignore trailing whitespace after the cursor
-    hoverLineIndentation := hoverFilePos.column
-  go hoverFilePos hoverLineIndentation cmdStx 0
-where
-  go
-      (hoverFilePos : Position)
-      (hoverLineIndentation : Nat)
-      (stx : Syntax)
-      (leadingWs : Nat)
-      : Bool := Id.run do
-    match stx.getPos?, stx.getTailPos? with
-    | some startPos, some endPos =>
-      let isCursorInCompletionRange :=
-        startPos.byteIdx - leadingWs <= hoverPos.byteIdx
-          && hoverPos.byteIdx <= endPos.byteIdx + stx.getTrailingSize
-      if ! isCursorInCompletionRange then
-        return false
-      let mut wsBeforeArg := leadingWs
-      for arg in stx.getArgs do
-        if go hoverFilePos hoverLineIndentation arg wsBeforeArg then
-          return true
-        -- We must account for the whitespace before an argument because the syntax nodes we use
-        -- to identify tactic blocks only start *after* the whitespace following a `by`, and we
-        -- want to provide tactic completions in that whitespace as well.
-        -- This method of computing whitespace assumes that there are no syntax nodes without tokens
-        -- after `by` and before the first proper tactic syntax.
-        wsBeforeArg := arg.getTrailingSize
-      return isCompletionInEmptyTacticBlock stx
-        || isCompletionAfterSemicolon stx
-        || isCompletionOnTacticBlockIndentation hoverFilePos hoverLineIndentation stx
-    | _, _ =>
-      -- Empty tactic blocks typically lack ranges since they do not contain any tokens.
-      -- We do not perform more precise range checking in this case because we assume that empty
-      -- tactic blocks always occur within other syntax with ranges that let us narrow down the
-      -- search to the degree that we can be sure that the cursor is indeed in this empty tactic
-      -- block.
-      return isCompletionInEmptyTacticBlock stx
-
-  isCompletionOnTacticBlockIndentation
-      (hoverFilePos : Position)
-      (hoverLineIndentation : Nat)
-      (stx : Syntax)
-      : Bool := Id.run do
-    let isCursorInIndentation := hoverFilePos.column <= hoverLineIndentation
-    if ! isCursorInIndentation then
-      -- Do not trigger tactic completion at the end of a properly indented tactic block line since
-      -- that line might already have entered term mode by that point.
-      return false
-    let some tacticsNode := getTacticsNode? stx
-      | return false
-    let some firstTacticPos := tacticsNode.getPos?
-      | return false
-    let firstTacticLine := fileMap.toPosition firstTacticPos |>.line
-    let firstTacticIndentation := getIndentationAmount fileMap firstTacticLine
-    -- This ensures that we do not accidentally provide tactic completions in a term mode proof -
-    -- tactic completions are only provided at the same indentation level as the other tactics in
-    -- that tactic block.
-    let isCursorInTacticBlock := hoverLineIndentation == firstTacticIndentation
-    return isCursorInProperWhitespace fileMap hoverPos && isCursorInTacticBlock
-
-  isCompletionAfterSemicolon (stx : Syntax) : Bool := Id.run do
-    let some tacticsNode := getTacticsNode? stx
-      | return false
-    let tactics := tacticsNode.getArgs
-    -- We want to provide completions in the case of `skip;<CURSOR>`, so the cursor must only be on
-    -- whitespace, not in proper whitespace.
-    return isCursorOnWhitespace fileMap hoverPos && tactics.any fun tactic => Id.run do
-      let some tailPos := tactic.getTailPos?
-        | return false
-      let isCursorAfterSemicolon :=
-        tactic.isToken ";"
-          && tailPos.byteIdx <= hoverPos.byteIdx
-          && hoverPos.byteIdx <= tailPos.byteIdx + tactic.getTrailingSize
-      return isCursorAfterSemicolon
-
-  getTacticsNode? (stx : Syntax) : Option Syntax :=
-    if stx.getKind == ``Parser.Tactic.tacticSeq1Indented then
-      some stx[0]
-    else if stx.getKind == ``Parser.Tactic.tacticSeqBracketed then
-      some stx[1]
-    else
-      none
-
-  isCompletionInEmptyTacticBlock (stx : Syntax) : Bool :=
-    isCursorInProperWhitespace fileMap hoverPos && isEmptyTacticBlock stx
-
-  isEmptyTacticBlock (stx : Syntax) : Bool :=
-    stx.getKind == ``Parser.Tactic.tacticSeq && isEmpty stx
-      || stx.getKind == ``Parser.Tactic.tacticSeq1Indented && isEmpty stx
-      || stx.getKind == ``Parser.Tactic.tacticSeqBracketed && isEmpty stx[1]
-
-  isEmpty : Syntax → Bool
-    | .missing       => true
-    | .ident ..      => false
-    | .atom ..       => false
-    | .node _ _ args => args.all isEmpty
-
-private partial def findOutermostContextInfo? (i : InfoTree) : Option ContextInfo :=
-  go i
-where
-  go (i : InfoTree) : Option ContextInfo := do
-    match i with
-  | .context ctx i =>
-    match ctx with
-    | .commandCtx ctxInfo =>
-      some { ctxInfo with }
-    | _ =>
-      -- This shouldn't happen (see the `PartialContextInfo` docstring),
-      -- but let's continue searching regardless
-      go i
-  | .node _ cs =>
-    cs.findSome? go
-  | .hole .. =>
-    none
-
-private def findSyntheticTacticCompletion?
-    (fileMap  : FileMap)
-    (hoverPos : String.Pos)
-    (cmdStx   : Syntax)
-    (infoTree : InfoTree)
-    : Option ContextualizedCompletionInfo := do
-  let ctx ← findOutermostContextInfo? infoTree
-  if ! isSyntheticTacticCompletion fileMap hoverPos cmdStx then
-    none
-  -- Neither `HoverInfo` nor the syntax in `.tactic` are important for tactic completion.
-  return { hoverInfo := HoverInfo.after, ctx, info := .tactic .missing }
-
-private def findExpectedTypeAt (infoTree : InfoTree) (hoverPos : String.Pos) : Option (ContextInfo × Expr) := do
-  let (ctx, .ofTermInfo i) ← infoTree.smallestInfo? fun i => Id.run do
-      let some pos := i.pos?
-        | return false
-      let some tailPos := i.tailPos?
-        | return false
-      let .ofTermInfo ti := i
-        | return false
-      return ti.expectedType?.isSome && pos <= hoverPos && hoverPos <= tailPos
-    | none
-  (ctx, i.expectedType?.get!)
-
-private partial def foldWithLeadingToken [Inhabited α]
-    (f    : α → Option Syntax → Syntax → α)
-    (init : α)
-    (stx  : Syntax)
-    : α :=
-  let (_, r) := go none init stx
-  r
-where
-  go [Inhabited α] (leadingToken? : Option Syntax) (acc : α) (stx : Syntax) : Option Syntax × α :=
-    let acc := f acc leadingToken? stx
-    match stx with
-    | .missing  => (none, acc)
-    | .atom ..  => (stx, acc)
-    | .ident .. => (stx, acc)
-    | .node _ _ args => Id.run do
-      let mut acc := acc
-      let mut lastToken? := none
-      for arg in args do
-        let (lastToken'?, acc') := go (lastToken? <|> leadingToken?) acc arg
-        lastToken? := lastToken'? <|> lastToken?
-        acc := acc'
-      return (lastToken?, acc)
-
-private def findWithLeadingToken?
-    (p : Option Syntax → Syntax → Bool)
-    (stx : Syntax)
-    : Option Syntax :=
-  foldWithLeadingToken (stx := stx) (init := none) fun foundStx? leadingToken? stx =>
-    match foundStx? with
-    | some foundStx => foundStx
-    | none =>
-      if p leadingToken? stx then
-        some stx
-      else
-        none
-
-private def isSyntheticStructFieldCompletion
-    (fileMap  : FileMap)
-    (hoverPos : String.Pos)
-    (cmdStx   : Syntax)
-    : Bool := Id.run do
-  let isCursorOnWhitespace := isCursorOnWhitespace fileMap hoverPos
-  let isCursorInProperWhitespace := isCursorInProperWhitespace fileMap hoverPos
-  if ! isCursorOnWhitespace then
-    return false
-
-  let hoverFilePos := fileMap.toPosition hoverPos
-  let mut hoverLineIndentation := getIndentationAmount fileMap hoverFilePos.line
-  if hoverFilePos.column < hoverLineIndentation then
-    -- Ignore trailing whitespace after the cursor
-    hoverLineIndentation := hoverFilePos.column
-
-  return Option.isSome <| findWithLeadingToken? (stx := cmdStx) fun leadingToken? stx => Id.run do
-    let some leadingToken := leadingToken?
-      | return false
-
-    if stx.getKind != ``Parser.Term.structInstFields then
-      return false
-
-    let fieldsAndSeps := stx[0].getArgs
-    let some outerBoundsStart := leadingToken.getTailPos? (canonicalOnly := true)
-      | return false
-    let some outerBoundsStop :=
-        stx.getTrailingTailPos? (canonicalOnly := true)
-          <|> leadingToken.getTrailingTailPos? (canonicalOnly := true)
-      | return false
-    let outerBounds : String.Range := ⟨outerBoundsStart, outerBoundsStop⟩
-
-    let isCompletionInEmptyBlock :=
-      fieldsAndSeps.isEmpty && outerBounds.contains hoverPos (includeStop := true)
-    if isCompletionInEmptyBlock then
-      return true
-
-    let isCompletionAfterSep := fieldsAndSeps.zipWithIndex.any fun (fieldOrSep, i) => Id.run do
-      if i % 2 == 0 || !fieldOrSep.isAtom then
-        return false
-      let sep := fieldOrSep
-      let some sepTailPos := sep.getTailPos?
-        | return false
-      return sepTailPos <= hoverPos
-        && hoverPos.byteIdx <= sepTailPos.byteIdx + sep.getTrailingSize
-    if isCompletionAfterSep then
-      return true
-
-    let isCompletionOnIndentation := Id.run do
-      if ! isCursorInProperWhitespace then
-        return false
-      let isCursorInIndentation := hoverFilePos.column <= hoverLineIndentation
-      if ! isCursorInIndentation then
-        return false
-      let some firstFieldPos := stx.getPos?
-        | return false
-      let firstFieldLine := fileMap.toPosition firstFieldPos |>.line
-      let firstFieldIndentation := getIndentationAmount fileMap firstFieldLine
-      let isCursorInBlock := hoverLineIndentation == firstFieldIndentation
-      return isCursorInBlock
-    return isCompletionOnIndentation
-
-private def findSyntheticFieldCompletion?
-  (fileMap  : FileMap)
-  (hoverPos : String.Pos)
-  (cmdStx   : Syntax)
-  (infoTree : InfoTree)
-  : Option ContextualizedCompletionInfo := do
-  if ! isSyntheticStructFieldCompletion fileMap hoverPos cmdStx then
-    none
-  let (ctx, expectedType) ← findExpectedTypeAt infoTree hoverPos
-  let .const typeName _ := expectedType.getAppFn
-    | none
-  if ! isStructure ctx.env typeName then
-    none
-  return { hoverInfo := HoverInfo.after, ctx, info := .fieldId .missing none .empty typeName }
-
-def findSyntheticCompletions
-    (fileMap  : FileMap)
-    (hoverPos : String.Pos)
-    (cmdStx   : Syntax)
-    (infoTree : InfoTree)
-    : Array ContextualizedCompletionInfo :=
-  let syntheticCompletionData? : Option ContextualizedCompletionInfo :=
-    findSyntheticTacticCompletion? fileMap hoverPos cmdStx infoTree <|>
-      findSyntheticFieldCompletion? fileMap hoverPos cmdStx infoTree <|>
-        findSyntheticIdentifierCompletion? hoverPos infoTree
-  syntheticCompletionData?.map (#[·]) |>.getD #[]
-
-end Lean.Server.Completion

src/Lean/Server/FileWorker.lean

@@ -28,7 +28,7 @@ import Lean.Server.FileWorker.WidgetRequests
 import Lean.Server.FileWorker.SetupFile
 import Lean.Server.Rpc.Basic
 import Lean.Widget.InteractiveDiagnostic
-import Lean.Server.Completion.ImportCompletion
+import Lean.Server.ImportCompletion
 
 /-!
 For general server architecture, see `README.md`. For details of IPC communication, see `Watchdog.lean`.

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -46,11 +46,10 @@ def handleCompletion (p : CompletionParams)
   mapTask (findCompletionCmdDataAtPos doc pos) fun cmdData? => do
     let some (cmdStx, infoTree) := cmdData?
       -- work around https://github.com/microsoft/vscode/issues/155738
-      | return {
-        items := #[{label := "-", data? := toJson { params := p : Lean.Lsp.CompletionItemData }}],
-        isIncomplete := true
-      }
-    Completion.find? p doc.meta.text pos cmdStx infoTree caps
+      | return { items := #[{label := "-"}], isIncomplete := true }
+    if let some r ← Completion.find? p doc.meta.text pos cmdStx infoTree caps then
+      return r
+    return { items := #[ ], isIncomplete := true }
 
 /--
 Handles `completionItem/resolve` requests that are sent by the client after the user selects
@@ -63,7 +62,7 @@ def handleCompletionItemResolve (item : CompletionItem)
     : RequestM (RequestTask CompletionItem) := do
   let doc ← readDoc
   let text := doc.meta.text
-  let some (data : ResolvableCompletionItemData) := item.data?.bind fun data => (fromJson? data).toOption
+  let some (data : CompletionItemDataWithId) := item.data?.bind fun data => (fromJson? data).toOption
     | return .pure item
   let some id := data.id?
     | return .pure item
@@ -71,7 +70,7 @@ def handleCompletionItemResolve (item : CompletionItem)
   mapTask (findCompletionCmdDataAtPos doc pos) fun cmdData? => do
     let some (cmdStx, infoTree) := cmdData?
       | return item
-    Completion.resolveCompletionItem? text pos cmdStx infoTree item id data.cPos
+    Completion.resolveCompletionItem? text pos cmdStx infoTree item id
 
 open Elab in
 def handleHover (p : HoverParams)

src/Lean/Server/ImportCompletion.lean

@@ -4,10 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Marc Huisinga
 -/
 prelude
+import Lean.Data.Name
 import Lean.Data.NameTrie
+import Lean.Data.Lsp.Utf16
+import Lean.Data.Lsp.LanguageFeatures
 import Lean.Util.Paths
 import Lean.Util.LakePath
-import Lean.Server.Completion.CompletionItemData
+import Lean.Server.CompletionItemData
 
 namespace ImportCompletion
 

src/Lean/Server/InfoUtils.lean

@@ -136,7 +136,6 @@ def InfoTree.getCompletionInfos (infoTree : InfoTree) : Array (ContextInfo × Co
 def Info.stx : Info → Syntax
   | ofTacticInfo i         => i.stx
   | ofTermInfo i           => i.stx
-  | ofPartialTermInfo i    => i.stx
   | ofCommandInfo i        => i.stx
   | ofMacroExpansionInfo i => i.stx
   | ofOptionInfo i         => i.stx
@@ -147,7 +146,6 @@ def Info.stx : Info → Syntax
   | ofFVarAliasInfo _      => .missing
   | ofFieldRedeclInfo i    => i.stx
   | ofOmissionInfo i       => i.stx
-  | ofChoiceInfo i         => i.stx
 
 def Info.lctx : Info → LocalContext
   | .ofTermInfo i           => i.lctx

src/Lean/Structure.lean

@@ -383,7 +383,7 @@ partial def computeStructureResolutionOrder [Monad m] [MonadEnv m]
   -- `resOrders` contains the resolution orders to merge.
   -- The parent list is inserted as a pseudo resolution order to ensure immediate parents come out in order,
   -- and it is added first to be the primary ordering constraint when there are ordering errors.
-  let mut resOrders := parentResOrders.insertIdx 0 parentNames |>.filter (!·.isEmpty)
+  let mut resOrders := parentResOrders.insertAt 0 parentNames |>.filter (!·.isEmpty)
 
   let mut resOrder : Array Name := #[structName]
   let mut defects : Array StructureResolutionOrderConflict := #[]

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean

@@ -815,7 +815,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
             have k'_in_bounds : k' < acc.2.1.length := by
               simp only [List.length_cons, Nat.succ_eq_add_one] at k'_succ_in_bounds
               exact Nat.lt_of_succ_lt_succ k'_succ_in_bounds
-            exact h2 (acc.2.1.get ⟨k', k'_in_bounds⟩) <| List.get_mem acc.snd.fst ⟨k', k'_in_bounds⟩
+            exact h2 (acc.2.1.get ⟨k', k'_in_bounds⟩) <| List.get_mem acc.snd.fst k' k'_in_bounds
     · next l_ne_i =>
       apply Or.inl
       constructor

src/include/lean/lean.h

@@ -406,13 +406,6 @@ static inline unsigned lean_ptr_other(lean_object * o) {
    small objects is a multiple of LEAN_OBJECT_SIZE_DELTA */
 LEAN_EXPORT size_t lean_object_byte_size(lean_object * o);
 
-/* Returns the size of the salient part of an object's storage,
-   i.e. the parts that contribute to the value representation;
-   padding or unused capacity is excluded. Operations that read
-   from an object's storage must only access these parts, since
-   the non-salient parts may not be initialized. */
-LEAN_EXPORT size_t lean_object_data_byte_size(lean_object * o);
-
 static inline bool lean_is_mt(lean_object * o) {
     return o->m_rc < 0;
 }
@@ -702,9 +695,6 @@ static inline size_t lean_array_capacity(b_lean_obj_arg o) { return lean_to_arra
 static inline size_t lean_array_byte_size(lean_object * o) {
     return sizeof(lean_array_object) + sizeof(void*)*lean_array_capacity(o);
 }
-static inline size_t lean_array_data_byte_size(lean_object * o) {
-    return sizeof(lean_array_object) + sizeof(void*)*lean_array_size(o);
-}
 static inline lean_object ** lean_array_cptr(lean_object * o) { return lean_to_array(o)->m_data; }
 static inline void lean_array_set_size(u_lean_obj_arg o, size_t sz) {
     assert(lean_is_array(o));
@@ -862,9 +852,6 @@ static inline size_t lean_sarray_byte_size(lean_object * o) {
     return sizeof(lean_sarray_object) + lean_sarray_elem_size(o)*lean_sarray_capacity(o);
 }
 static inline size_t lean_sarray_size(b_lean_obj_arg o) { return lean_to_sarray(o)->m_size; }
-static inline size_t lean_sarray_data_byte_size(lean_object * o) {
-    return sizeof(lean_sarray_object) + lean_sarray_elem_size(o)*lean_sarray_size(o);
-}
 static inline void lean_sarray_set_size(u_lean_obj_arg o, size_t sz) {
     assert(lean_is_exclusive(o));
     assert(sz <= lean_sarray_capacity(o));
@@ -1026,7 +1013,6 @@ static inline char const * lean_string_cstr(b_lean_obj_arg o) {
 }
 static inline size_t lean_string_size(b_lean_obj_arg o) { return lean_to_string(o)->m_size; }
 static inline size_t lean_string_len(b_lean_obj_arg o) { return lean_to_string(o)->m_length; }
-static inline size_t lean_string_data_byte_size(lean_object * o) { return sizeof(lean_string_object) + lean_string_size(o); }
 LEAN_EXPORT lean_obj_res lean_string_push(lean_obj_arg s, uint32_t c);
 LEAN_EXPORT lean_obj_res lean_string_append(lean_obj_arg s1, b_lean_obj_arg s2);
 static inline lean_obj_res lean_string_length(b_lean_obj_arg s) { return lean_box(lean_string_len(s)); }

src/runtime/object.cpp

@@ -172,28 +172,6 @@ extern "C" LEAN_EXPORT size_t lean_object_byte_size(lean_object * o) {
     }
 }
 
-extern "C" LEAN_EXPORT size_t lean_object_data_byte_size(lean_object * o) {
-    if (o->m_cs_sz == 0) {
-        /* Recall that multi-threaded, single-threaded and persistent objects are stored in the heap.
-           Persistent objects are multi-threaded and/or single-threaded that have been "promoted" to
-           a persistent status. */
-        switch (lean_ptr_tag(o)) {
-        case LeanArray:       return lean_array_data_byte_size(o);
-        case LeanScalarArray: return lean_sarray_data_byte_size(o);
-        case LeanString:      return lean_string_data_byte_size(o);
-        default:              return lean_small_object_size(o);
-        }
-    } else {
-        /* See comment at `lean_set_non_heap_header`, for small objects we store the object size in the RC field. */
-        switch (lean_ptr_tag(o)) {
-        case LeanArray:       return lean_array_data_byte_size(o);
-        case LeanScalarArray: return lean_sarray_data_byte_size(o);
-        case LeanString:      return lean_string_data_byte_size(o);
-        default:              return o->m_cs_sz;
-        }
-    }
-}
-
 static inline void lean_dealloc(lean_object * o, size_t sz) {
 #ifdef LEAN_SMALL_ALLOCATOR
     dealloc(o, sz);

src/runtime/sharecommon.cpp

@@ -13,8 +13,8 @@ namespace lean {
 extern "C" LEAN_EXPORT uint8 lean_sharecommon_eq(b_obj_arg o1, b_obj_arg o2) {
     lean_assert(!lean_is_scalar(o1));
     lean_assert(!lean_is_scalar(o2));
-    size_t sz1 = lean_object_data_byte_size(o1);
-    size_t sz2 = lean_object_data_byte_size(o2);
+    size_t sz1 = lean_object_byte_size(o1);
+    size_t sz2 = lean_object_byte_size(o2);
     if (sz1 != sz2) return false;
     // compare relevant parts of the header
     if (lean_ptr_tag(o1) != lean_ptr_tag(o2)) return false;
@@ -27,7 +27,7 @@ extern "C" LEAN_EXPORT uint8 lean_sharecommon_eq(b_obj_arg o1, b_obj_arg o2) {
 
 extern "C" LEAN_EXPORT uint64_t lean_sharecommon_hash(b_obj_arg o) {
     lean_assert(!lean_is_scalar(o));
-    size_t sz = lean_object_data_byte_size(o);
+    size_t sz = lean_object_byte_size(o);
     size_t header_sz = sizeof(lean_object);
     // hash relevant parts of the header
     unsigned init = hash(lean_ptr_tag(o), lean_ptr_other(o));