fix: broadcast test

This PR adds `suggest_for` annotations such that `Int*.toNatClamp` is
suggested for `Int*.toNat`.

script/Modulize.lean

@@ -29,7 +29,7 @@ def main (args : List String) : IO Unit := do
     if !msgs.toList.isEmpty then -- skip this file if there are parse errors
       msgs.forM fun msg => msg.toString >>= IO.println
       throw <| .userError "parse errors in file"
-    let `(header| $[module%$moduleTk?]? $imps:import*) := header
+    let `(header| $[module%$moduleTk?]? $[prelude%$preludeTk?]? $imps:import*) := header
       | throw <| .userError s!"unexpected header syntax of {path}"
     if moduleTk?.isSome then
       continue
@@ -38,11 +38,11 @@ def main (args : List String) : IO Unit := do
     let startPos := header.raw.getPos? |>.getD parserState.pos
 
     let dummyEnv ← mkEmptyEnvironment
-    let (initCmd, parserState', _) :=
+    let (initCmd, parserState', msgs') :=
       Parser.parseCommand inputCtx { env := dummyEnv, options := {} } parserState msgs
 
-    -- insert section if any trailing command
-    if !initCmd.isOfKind ``Parser.Command.eoi then
+    -- insert section if any trailing command (or error, which could be from an unknown command)
+    if !initCmd.isOfKind ``Parser.Command.eoi || msgs'.hasErrors then
       let insertPos? :=
           -- put below initial module docstring if any
           guard (initCmd.isOfKind ``Parser.Command.moduleDoc) *> initCmd.getTailPos? <|>
@@ -57,19 +57,21 @@ def main (args : List String) : IO Unit := do
         sec := "\n\n" ++ sec
       if insertPos?.isNone then
         sec := sec ++ "\n\n"
-      text := text.extract 0 insertPos ++ sec ++ text.extract insertPos text.rawEndPos
+      let insertPos := text.pos! insertPos
+      text := text.extract text.startPos insertPos ++ sec ++ text.extract insertPos text.endPos
 
     -- prepend each import with `public `
     for imp in imps.reverse do
       let insertPos := imp.raw.getPos?.get!
       let prfx := if doMeta then "public meta " else "public "
-      text := text.extract 0 insertPos ++ prfx ++ text.extract insertPos text.rawEndPos
+      let insertPos := text.pos! insertPos
+      text := text.extract text.startPos insertPos ++ prfx ++ text.extract insertPos text.endPos
 
     -- insert `module` header
-    let mut initText := text.extract 0 startPos
-    if !initText.trim.isEmpty then
+    let mut initText := text.extract text.startPos (text.pos! startPos)
+    if !initText.trimAscii.isEmpty then
       -- If there is a header comment, preserve it and put `module` in the line after
-      initText := initText.trimRight ++ "\n"
-    text := initText ++ "module\n\n" ++ text.extract startPos text.rawEndPos
+      initText := initText.trimAsciiEnd.toString ++ "\n"
+    text := initText ++ "module\n\n" ++ text.extract (text.pos! startPos) text.endPos
 
     IO.FS.writeFile path text

src/Init/Data/Char.lean

@@ -9,3 +9,4 @@ prelude
 public import Init.Data.Char.Basic
 public import Init.Data.Char.Lemmas
 public import Init.Data.Char.Order
+public import Init.Data.Char.Ordinal

src/Init/Data/Char/Ordinal.lean

@@ -0,0 +1,242 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.Fin.OverflowAware
+public import Init.Data.UInt.Basic
+public import Init.Data.Function
+import Init.Data.Char.Lemmas
+import Init.Data.Char.Order
+import Init.Grind
+
+/-!
+# Bijection between `Char` and `Fin Char.numCodePoints`
+
+In this file, we construct a bijection between `Char` and `Fin Char.numCodePoints` and show that
+it is compatible with various operations. Since `Fin` is simpler than `Char` due to being based
+on natural numbers instead of `UInt32` and not having a hole in the middle (surrogate code points),
+this is sometimes useful to simplify reasoning about `Char`.
+
+We use these declarations in the construction of `Char` ranges, see the module
+`Init.Data.Range.Polymorphic.Char`.
+-/
+
+set_option doc.verso true
+
+public section
+
+namespace Char
+
+/-- The number of surrogate code points. -/
+abbrev numSurrogates : Nat :=
+  -- 0xe000 - 0xd800
+  2048
+
+/-- The size of the {name}`Char` type. -/
+abbrev numCodePoints : Nat :=
+  -- 0x110000 - numSurrogates
+  1112064
+
+/--
+Packs {name}`Char` bijectively into {lean}`Fin Char.numCodePoints` by shifting code points which are
+greater than the surrogate code points by the number of surrogate code points.
+
+The inverse of this function is called {name (scope := "Init.Data.Char.Ordinal")}`Char.ofOrdinal`.
+-/
+def ordinal (c : Char) : Fin Char.numCodePoints :=
+  if h : c.val < 0xd800 then
+    ⟨c.val.toNat, by grind [UInt32.lt_iff_toNat_lt]⟩
+  else
+    ⟨c.val.toNat - Char.numSurrogates, by grind [UInt32.lt_iff_toNat_lt]⟩
+
+/--
+Unpacks {lean}`Fin Char.numCodePoints` bijectively to {name}`Char` by shifting code points which are
+greater than the surrogate code points by the number of surrogate code points.
+
+The inverse of this function is called {name}`Char.ordinal`.
+-/
+def ofOrdinal (f : Fin Char.numCodePoints) : Char :=
+  if h : (f : Nat) < 0xd800 then
+    ⟨UInt32.ofNatLT f (by grind), by grind [UInt32.toNat_ofNatLT]⟩
+  else
+    ⟨UInt32.ofNatLT (f + Char.numSurrogates) (by grind), by grind [UInt32.toNat_ofNatLT]⟩
+
+/--
+Computes the next {name}`Char`, skipping over surrogate code points (which are not valid
+{name}`Char`s) as necessary.
+
+This function is specified by its interaction with {name}`Char.ordinal`, see
+{name (scope := "Init.Data.Char.Ordinal")}`Char.succ?_eq`.
+-/
+def succ? (c : Char) : Option Char :=
+  if h₀ : c.val < 0xd7ff then
+    some ⟨c.val + 1, by grind [UInt32.lt_iff_toNat_lt, UInt32.toNat_add]⟩
+  else if h₁ : c.val = 0xd7ff then
+    some ⟨0xe000, by decide⟩
+  else if h₂ : c.val < 0x10ffff then
+    some ⟨c.val + 1, by
+      simp only [UInt32.lt_iff_toNat_lt, UInt32.reduceToNat, Nat.not_lt, ← UInt32.toNat_inj,
+        UInt32.isValidChar, Nat.isValidChar, UInt32.toNat_add, Nat.reducePow] at *
+      grind⟩
+  else none
+
+/--
+Computes the {name}`m`-th next {name}`Char`, skipping over surrogate code points (which are not
+valid {name}`Char`s) as necessary.
+
+This function is specified by its interaction with {name}`Char.ordinal`, see
+{name (scope := "Init.Data.Char.Ordinal")}`Char.succMany?_eq`.
+-/
+def succMany? (m : Nat) (c : Char) : Option Char :=
+  c.ordinal.addNat? m |>.map Char.ofOrdinal
+
+@[grind =]
+theorem coe_ordinal {c : Char} :
+    (c.ordinal : Nat) =
+      if c.val < 0xd800 then
+        c.val.toNat
+      else
+        c.val.toNat - Char.numSurrogates := by
+  grind [Char.ordinal]
+
+@[simp]
+theorem ordinal_zero : '\x00'.ordinal = 0 := by
+  ext
+  simp [coe_ordinal]
+
+@[grind =]
+theorem val_ofOrdinal {f : Fin Char.numCodePoints} :
+    (Char.ofOrdinal f).val =
+      if h : (f : Nat) < 0xd800 then
+        UInt32.ofNatLT f (by grind)
+      else
+        UInt32.ofNatLT (f + Char.numSurrogates) (by grind) := by
+  grind [Char.ofOrdinal]
+
+@[simp]
+theorem ofOrdinal_ordinal {c : Char} : Char.ofOrdinal c.ordinal = c := by
+  ext
+  simp only [val_ofOrdinal, coe_ordinal, UInt32.ofNatLT_add]
+  split
+  · grind [UInt32.lt_iff_toNat_lt, UInt32.ofNatLT_toNat]
+  · rw [dif_neg]
+    · simp only [← UInt32.toNat_inj, UInt32.toNat_add, UInt32.toNat_ofNatLT, Nat.reducePow]
+      grind [UInt32.toNat_lt, UInt32.lt_iff_toNat_lt]
+    · grind [UInt32.lt_iff_toNat_lt]
+
+@[simp]
+theorem ordinal_ofOrdinal {f : Fin Char.numCodePoints} : (Char.ofOrdinal f).ordinal = f := by
+  ext
+  simp [coe_ordinal, val_ofOrdinal]
+  split
+  · rw [if_pos, UInt32.toNat_ofNatLT]
+    simpa [UInt32.lt_iff_toNat_lt]
+  · rw [if_neg, UInt32.toNat_add, UInt32.toNat_ofNatLT, UInt32.toNat_ofNatLT, Nat.mod_eq_of_lt,
+      Nat.add_sub_cancel]
+    · grind
+    · simp only [UInt32.lt_iff_toNat_lt, UInt32.toNat_add, UInt32.toNat_ofNatLT, Nat.reducePow,
+        UInt32.reduceToNat, Nat.not_lt]
+      grind
+
+@[simp]
+theorem ordinal_comp_ofOrdinal : Char.ordinal ∘ Char.ofOrdinal = id := by
+  ext; simp
+
+@[simp]
+theorem ofOrdinal_comp_ordinal : Char.ofOrdinal ∘ Char.ordinal = id := by
+  ext; simp
+
+@[simp]
+theorem ordinal_inj {c d : Char} : c.ordinal = d.ordinal ↔ c = d :=
+  ⟨fun h => by simpa using congrArg Char.ofOrdinal h, (· ▸ rfl)⟩
+
+theorem ordinal_injective : Function.Injective Char.ordinal :=
+  fun _ _ => ordinal_inj.1
+
+@[simp]
+theorem ofOrdinal_inj {f g : Fin Char.numCodePoints} :
+    Char.ofOrdinal f = Char.ofOrdinal g ↔ f = g :=
+  ⟨fun h => by simpa using congrArg Char.ordinal h, (· ▸ rfl)⟩
+
+theorem ofOrdinal_injective : Function.Injective Char.ofOrdinal :=
+   fun _ _ => ofOrdinal_inj.1
+
+theorem ordinal_le_of_le {c d : Char} (h : c ≤ d) : c.ordinal ≤ d.ordinal := by
+  simp only [le_def, UInt32.le_iff_toNat_le] at h
+  simp only [Fin.le_def, coe_ordinal, UInt32.lt_iff_toNat_lt, UInt32.reduceToNat]
+  grind
+
+theorem ofOrdinal_le_of_le {f g : Fin Char.numCodePoints} (h : f ≤ g) :
+    Char.ofOrdinal f ≤ Char.ofOrdinal g := by
+  simp only [Fin.le_def] at h
+  simp only [le_def, val_ofOrdinal, UInt32.ofNatLT_add, UInt32.le_iff_toNat_le]
+  split
+  · simp only [UInt32.toNat_ofNatLT]
+    split
+    · simpa
+    · simp only [UInt32.toNat_add, UInt32.toNat_ofNatLT, Nat.reducePow]
+      grind
+  · simp only [UInt32.toNat_add, UInt32.toNat_ofNatLT, Nat.reducePow]
+    rw [dif_neg (by grind)]
+    simp only [UInt32.toNat_add, UInt32.toNat_ofNatLT, Nat.reducePow]
+    grind
+
+theorem le_iff_ordinal_le {c d : Char} : c ≤ d ↔ c.ordinal ≤ d.ordinal :=
+  ⟨ordinal_le_of_le, fun h => by simpa using ofOrdinal_le_of_le h⟩
+
+theorem le_iff_ofOrdinal_le {f g : Fin Char.numCodePoints} :
+    f ≤ g ↔ Char.ofOrdinal f ≤ Char.ofOrdinal g :=
+  ⟨ofOrdinal_le_of_le, fun h => by simpa using ordinal_le_of_le h⟩
+
+theorem lt_iff_ordinal_lt {c d : Char} : c < d ↔ c.ordinal < d.ordinal := by
+  simp only [Std.lt_iff_le_and_not_ge, le_iff_ordinal_le]
+
+theorem lt_iff_ofOrdinal_lt {f g : Fin Char.numCodePoints} :
+    f < g ↔ Char.ofOrdinal f < Char.ofOrdinal g := by
+  simp only [Std.lt_iff_le_and_not_ge, le_iff_ofOrdinal_le]
+
+theorem succ?_eq {c : Char} : c.succ? = (c.ordinal.addNat? 1).map Char.ofOrdinal := by
+  fun_cases Char.succ? with
+  | case1 h =>
+    rw [Fin.addNat?_eq_some]
+    · simp only [coe_ordinal, Option.map_some, Option.some.injEq, Char.ext_iff, val_ofOrdinal,
+        UInt32.ofNatLT_add, UInt32.reduceOfNatLT]
+      split
+      · simp only [UInt32.ofNatLT_toNat, dite_eq_ite, left_eq_ite_iff, Nat.not_lt,
+          Nat.reduceLeDiff, UInt32.left_eq_add]
+        grind [UInt32.lt_iff_toNat_lt]
+      · grind
+    · simp [coe_ordinal]
+      grind [UInt32.lt_iff_toNat_lt]
+  | case2 =>
+    rw [Fin.addNat?_eq_some]
+    · simp [coe_ordinal, *, Char.ext_iff, val_ofOrdinal, numSurrogates]
+    · simp [coe_ordinal, *, numCodePoints]
+  | case3 =>
+    rw [Fin.addNat?_eq_some]
+    · simp only [coe_ordinal, Option.map_some, Option.some.injEq, Char.ext_iff, val_ofOrdinal,
+        UInt32.ofNatLT_add, UInt32.reduceOfNatLT]
+      split
+      · grind
+      · rw [dif_neg]
+        · simp only [← UInt32.toNat_inj, UInt32.toNat_add, UInt32.reduceToNat, Nat.reducePow,
+            UInt32.toNat_ofNatLT, Nat.mod_add_mod]
+          grind [UInt32.lt_iff_toNat_lt, UInt32.toNat_inj]
+        · grind [UInt32.lt_iff_toNat_lt, UInt32.toNat_inj]
+    · grind [UInt32.lt_iff_toNat_lt]
+  | case4 =>
+    rw [eq_comm]
+    grind [UInt32.lt_iff_toNat_lt]
+
+theorem map_ordinal_succ? {c : Char} : c.succ?.map ordinal = c.ordinal.addNat? 1 := by
+  simp [succ?_eq]
+
+theorem succMany?_eq {m : Nat} {c : Char} :
+    c.succMany? m = (c.ordinal.addNat? m).map Char.ofOrdinal := by
+  rfl
+
+end Char

src/Init/Data/Fin.lean

@@ -11,3 +11,4 @@ public import Init.Data.Fin.Log2
 public import Init.Data.Fin.Iterate
 public import Init.Data.Fin.Fold
 public import Init.Data.Fin.Lemmas
+public import Init.Data.Fin.OverflowAware

src/Init/Data/Fin/OverflowAware.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.Fin.Basic
+import Init.Data.Fin.Lemmas
+
+set_option doc.verso true
+
+public section
+
+namespace Fin
+
+/--
+Overflow-aware addition of a natural number to an element of {lean}`Fin n`.
+
+Examples:
+* {lean}`(2 : Fin 3).addNat? 1 = (none : Option (Fin 3))`
+* {lean}`(2 : Fin 4).addNat? 1 = (some 3 : Option (Fin 4))`
+-/
+@[inline]
+protected def addNat? (i : Fin n) (m : Nat) : Option (Fin n) :=
+  if h : i + m < n then some ⟨i + m, h⟩ else none
+
+theorem addNat?_eq_some {i : Fin n} (h : i + m < n) : i.addNat? m = some ⟨i + m, h⟩ := by
+  simp [Fin.addNat?, h]
+
+theorem addNat?_eq_some_iff {i : Fin n} :
+    i.addNat? m = some j ↔ i + m < n ∧ j = i + m := by
+  simp only [Fin.addNat?]
+  split <;> simp [Fin.ext_iff, eq_comm, *]
+
+@[simp]
+theorem addNat?_eq_none_iff {i : Fin n} : i.addNat? m = none ↔ n ≤ i + m := by
+  simp only [Fin.addNat?]
+  split <;> simp_all [Nat.not_lt]
+
+@[simp]
+theorem addNat?_zero {i : Fin n} : i.addNat? 0 = some i := by
+  simp [addNat?_eq_some_iff]
+
+@[grind =]
+theorem addNat?_eq_dif {i : Fin n} :
+    i.addNat? m = if h : i + m < n then some ⟨i + m, h⟩ else none := by
+  rfl
+
+end Fin

src/Init/Data/Option.lean

@@ -15,3 +15,4 @@ public import Init.Data.Option.Attach
 public import Init.Data.Option.List
 public import Init.Data.Option.Monadic
 public import Init.Data.Option.Array
+public import Init.Data.Option.Function

src/Init/Data/Option/Function.lean

@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.Function
+import Init.Data.Option.Lemmas
+
+public section
+
+namespace Option
+
+theorem map_injective {f : α → β} (hf : Function.Injective f) :
+    Function.Injective (Option.map f) := by
+  intros a b hab
+  cases a <;> cases b
+  · simp
+  · simp at hab
+  · simp at hab
+  · simp only [map_some, some.injEq] at hab
+    simpa using hf hab
+
+end Option

src/Init/Data/Option/Lemmas.lean

@@ -307,12 +307,20 @@ theorem map_id' {x : Option α} : (x.map fun a => a) = x := congrFun map_id x
 
 theorem map_id_apply' {α : Type u} {x : Option α} : Option.map (fun (a : α) => a) x = x := by simp
 
+/-- See `Option.apply_get` for a version that can be rewritten in the reverse direction. -/
 @[simp, grind =] theorem get_map {f : α → β} {o : Option α} {h : (o.map f).isSome} :
     (o.map f).get h = f (o.get (by simpa using h)) := by
   cases o with
   | none => simp at h
   | some a => simp
 
+/-- See `Option.get_map` for a version that can be rewritten in the reverse direction. -/
+theorem apply_get {f : α → β} {o : Option α} {h} :
+    f (o.get h) = (o.map f).get (by simp [h]) := by
+  cases o
+  · simp at h
+  · simp
+
 @[simp] theorem map_map (h : β → γ) (g : α → β) (x : Option α) :
     (x.map g).map h = x.map (h ∘ g) := by
   cases x <;> simp only [map_none, map_some, ·∘·]
@@ -732,6 +740,11 @@ theorem get_merge {o o' : Option α} {f : α → α → α} {i : α} [Std.Lawful
 theorem elim_guard : (guard p a).elim b f = if p a then f a else b := by
   cases h : p a <;> simp [*, guard]
 
+@[simp]
+theorem Option.elim_map {f : α → β} {g' : γ} {g : β → γ} (o : Option α) :
+    (o.map f).elim g' g = o.elim g' (g ∘ f) := by
+  cases o <;> simp
+
 -- I don't see how to construct a good grind pattern to instantiate this.
 @[simp] theorem getD_map (f : α → β) (x : α) (o : Option α) :
   (o.map f).getD (f x) = f (getD o x) := by cases o <;> rfl

src/Init/Data/Range/Polymorphic.lean

@@ -10,7 +10,10 @@ public import Init.Data.Range.Polymorphic.Basic
 public import Init.Data.Range.Polymorphic.Iterators
 public import Init.Data.Range.Polymorphic.Stream
 public import Init.Data.Range.Polymorphic.Lemmas
+public import Init.Data.Range.Polymorphic.Map
 
+public import Init.Data.Range.Polymorphic.Fin
+public import Init.Data.Range.Polymorphic.Char
 public import Init.Data.Range.Polymorphic.Nat
 public import Init.Data.Range.Polymorphic.Int
 public import Init.Data.Range.Polymorphic.BitVec

src/Init/Data/Range/Polymorphic/Char.lean

@@ -0,0 +1,79 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.Char.Ordinal
+public import Init.Data.Range.Polymorphic.Fin
+import Init.Data.Range.Polymorphic.Lemmas
+import Init.Data.Range.Polymorphic.Map
+import Init.Data.Char.Order
+
+open Std Std.PRange Std.PRange.UpwardEnumerable
+
+namespace Char
+
+public instance : UpwardEnumerable Char where
+  succ?
+  succMany?
+
+@[simp]
+public theorem pRangeSucc?_eq : PRange.succ? (α := Char) = Char.succ? := rfl
+
+@[simp]
+public theorem pRangeSuccMany?_eq : PRange.succMany? (α := Char) = Char.succMany? := rfl
+
+public instance : Rxc.HasSize Char where
+  size lo hi := Rxc.HasSize.size lo.ordinal hi.ordinal
+
+public instance : Rxo.HasSize Char where
+  size lo hi := Rxo.HasSize.size lo.ordinal hi.ordinal
+
+public instance : Rxi.HasSize Char where
+  size hi := Rxi.HasSize.size hi.ordinal
+
+public instance : Least? Char where
+  least? := some '\x00'
+
+@[simp]
+public theorem least?_eq : Least?.least? (α := Char) = some '\x00' := rfl
+
+def map : Map Char (Fin Char.numCodePoints) where
+  toFun := Char.ordinal
+  injective := ordinal_injective
+  succ?_toFun := by simp [succ?_eq]
+  succMany?_toFun := by simp [succMany?_eq]
+
+@[simp]
+theorem toFun_map : map.toFun = Char.ordinal := rfl
+
+instance : Map.PreservesLE map where
+  le_iff := by simp [le_iff_ordinal_le]
+
+instance : Map.PreservesRxcSize map where
+  size_eq := rfl
+
+instance : Map.PreservesRxoSize map where
+  size_eq := rfl
+
+instance : Map.PreservesRxiSize map where
+  size_eq := rfl
+
+instance : Map.PreservesLeast? map where
+  map_least? := by simp
+
+public instance : LawfulUpwardEnumerable Char := .ofMap map
+public instance : LawfulUpwardEnumerableLE Char := .ofMap map
+public instance : LawfulUpwardEnumerableLT Char := .ofMap map
+public instance : LawfulUpwardEnumerableLeast? Char := .ofMap map
+public instance : Rxc.LawfulHasSize Char := .ofMap map
+public instance : Rxc.IsAlwaysFinite Char := .ofMap map
+public instance : Rxo.LawfulHasSize Char := .ofMap map
+public instance : Rxo.IsAlwaysFinite Char := .ofMap map
+public instance : Rxi.LawfulHasSize Char := .ofMap map
+public instance : Rxi.IsAlwaysFinite Char := .ofMap map
+
+end Char

src/Init/Data/Range/Polymorphic/Fin.lean

@@ -0,0 +1,92 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.Range.Polymorphic.Instances
+public import Init.Data.Fin.OverflowAware
+import Init.Grind
+
+public section
+
+open Std Std.PRange
+
+namespace Fin
+
+instance : UpwardEnumerable (Fin n) where
+  succ? i := i.addNat? 1
+  succMany? m i := i.addNat? m
+
+@[simp, grind =]
+theorem pRangeSucc?_eq : PRange.succ? (α := Fin n) = (·.addNat? 1) := rfl
+
+@[simp, grind =]
+theorem pRangeSuccMany?_eq : PRange.succMany? m (α := Fin n) = (·.addNat? m) :=
+  rfl
+
+instance : LawfulUpwardEnumerable (Fin n) where
+  ne_of_lt a b := by grind [UpwardEnumerable.LT]
+  succMany?_zero a := by simp
+  succMany?_add_one m a := by grind
+
+instance : LawfulUpwardEnumerableLE (Fin n) where
+  le_iff x y := by
+    simp only [le_def, UpwardEnumerable.LE, pRangeSuccMany?_eq, Fin.addNat?_eq_dif,
+      Option.dite_none_right_eq_some, Option.some.injEq, ← val_inj, exists_prop]
+    exact ⟨fun h => ⟨y - x, by grind⟩, by grind⟩
+
+instance : Least? (Fin 0) where
+  least? := none
+
+instance : LawfulUpwardEnumerableLeast? (Fin 0) where
+  least?_le a := False.elim (Nat.not_lt_zero _ a.isLt)
+
+@[simp]
+theorem least?_eq_of_zero : Least?.least? (α := Fin 0) = none := rfl
+
+instance [NeZero n] : Least? (Fin n) where
+  least? := some 0
+
+instance [NeZero n] : LawfulUpwardEnumerableLeast? (Fin n) where
+  least?_le a := ⟨0, rfl, (LawfulUpwardEnumerableLE.le_iff 0 a).1 (Fin.zero_le _)⟩
+
+@[simp]
+theorem least?_eq [NeZero n] : Least?.least? (α := Fin n) = some 0 := rfl
+
+instance : LawfulUpwardEnumerableLT (Fin n) := inferInstance
+
+instance : Rxc.HasSize (Fin n) where
+  size lo hi := hi + 1 - lo
+
+@[grind =]
+theorem rxcHasSize_eq :
+    Rxc.HasSize.size (α := Fin n) = fun (lo hi : Fin n) => (hi + 1 - lo : Nat) := rfl
+
+instance : Rxc.LawfulHasSize (Fin n) where
+  size_eq_zero_of_not_le bound x := by grind
+  size_eq_one_of_succ?_eq_none lo hi := by grind
+  size_eq_succ_of_succ?_eq_some lo hi x := by grind
+
+instance : Rxc.IsAlwaysFinite (Fin n) := inferInstance
+
+instance : Rxo.HasSize (Fin n) := .ofClosed
+instance : Rxo.LawfulHasSize (Fin n) := inferInstance
+instance : Rxo.IsAlwaysFinite (Fin n) := inferInstance
+
+instance : Rxi.HasSize (Fin n) where
+  size lo := n - lo
+
+@[grind =]
+theorem rxiHasSize_eq :
+    Rxi.HasSize.size (α := Fin n) = fun (lo : Fin n) => (n - lo : Nat) := rfl
+
+instance : Rxi.LawfulHasSize (Fin n) where
+  size_eq_one_of_succ?_eq_none x := by grind
+  size_eq_succ_of_succ?_eq_some lo lo' := by grind
+
+instance : Rxi.IsAlwaysFinite (Fin n) := inferInstance
+
+end Fin

src/Init/Data/Range/Polymorphic/Map.lean

@@ -0,0 +1,195 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.Range.Polymorphic.Instances
+public import Init.Data.Function
+import Init.Data.Order.Lemmas
+import Init.Data.Option.Function
+
+public section
+
+/-!
+# Mappings between `UpwardEnumerable` types
+
+In this file we build machinery for pulling back lawfulness properties for `UpwardEnumerable` along
+injective functions that commute with the relevant operations.
+-/
+
+namespace Std
+
+namespace PRange
+
+namespace UpwardEnumerable
+
+/--
+An injective mapping between two types implementing `UpwardEnumerable` that commutes with `succ?`
+and `succMany?`.
+
+Having such a mapping means that all of the `Prop`-valued lawfulness classes around
+`UpwardEnumerable` can be pulled back.
+-/
+structure Map (α : Type u) (β : Type v) [UpwardEnumerable α] [UpwardEnumerable β] where
+  toFun : α → β
+  injective : Function.Injective toFun
+  succ?_toFun (a : α) : succ? (toFun a) = (succ? a).map toFun
+  succMany?_toFun (n : Nat) (a : α) : succMany? n (toFun a) = (succMany? n a).map toFun
+
+namespace Map
+
+variable [UpwardEnumerable α] [UpwardEnumerable β]
+
+theorem succ?_eq_none_iff (f : Map α β) {a : α} :
+    succ? a = none ↔ succ? (f.toFun a) = none := by
+  rw [← (Option.map_injective f.injective).eq_iff, Option.map_none, ← f.succ?_toFun]
+
+theorem succ?_eq_some_iff (f : Map α β) {a b : α} :
+    succ? a = some b ↔ succ? (f.toFun a) = some (f.toFun b) := by
+  rw [← (Option.map_injective f.injective).eq_iff, Option.map_some, ← f.succ?_toFun]
+
+theorem le_iff (f : Map α β) {a b : α} :
+    UpwardEnumerable.LE a b ↔ UpwardEnumerable.LE (f.toFun a) (f.toFun b) := by
+  simp only [UpwardEnumerable.LE, f.succMany?_toFun, Option.map_eq_some_iff]
+  refine ⟨fun ⟨n, hn⟩ => ⟨n, b, by simp [hn]⟩, fun ⟨n, c, hn⟩ => ⟨n, ?_⟩⟩
+  rw [hn.1, Option.some_inj, f.injective hn.2]
+
+theorem lt_iff (f : Map α β) {a b : α} :
+    UpwardEnumerable.LT a b ↔ UpwardEnumerable.LT (f.toFun a) (f.toFun b) := by
+  simp only [UpwardEnumerable.LT, f.succMany?_toFun, Option.map_eq_some_iff]
+  refine ⟨fun ⟨n, hn⟩ => ⟨n, b, by simp [hn]⟩, fun ⟨n, c, hn⟩ => ⟨n, ?_⟩⟩
+  rw [hn.1, Option.some_inj, f.injective hn.2]
+
+theorem succ?_toFun' (f : Map α β) : succ? ∘ f.toFun = Option.map f.toFun ∘ succ? := by
+  ext
+  simp [f.succ?_toFun]
+
+/-- Compatibility class for `Map` and `≤`. -/
+class PreservesLE [LE α] [LE β] (f : Map α β) where
+  le_iff : a ≤ b ↔ f.toFun a ≤ f.toFun b
+
+/-- Compatibility class for `Map` and `<`. -/
+class PreservesLT [LT α] [LT β] (f : Map α β) where
+  lt_iff : a < b ↔ f.toFun a < f.toFun b
+
+/-- Compatibility class for `Map` and `Rxc.HasSize`. -/
+class PreservesRxcSize [Rxc.HasSize α] [Rxc.HasSize β] (f : Map α β) where
+  size_eq : Rxc.HasSize.size a b = Rxc.HasSize.size (f.toFun a) (f.toFun b)
+
+/-- Compatibility class for `Map` and `Rxo.HasSize`. -/
+class PreservesRxoSize [Rxo.HasSize α] [Rxo.HasSize β] (f : Map α β) where
+  size_eq : Rxo.HasSize.size a b = Rxo.HasSize.size (f.toFun a) (f.toFun b)
+
+/-- Compatibility class for `Map` and `Rxi.HasSize`. -/
+class PreservesRxiSize [Rxi.HasSize α] [Rxi.HasSize β] (f : Map α β) where
+  size_eq : Rxi.HasSize.size b = Rxi.HasSize.size (f.toFun b)
+
+/-- Compatibility class for `Map` and `Least?`. -/
+class PreservesLeast? [Least? α] [Least? β] (f : Map α β) where
+  map_least? : Least?.least?.map f.toFun = Least?.least?
+
+end UpwardEnumerable.Map
+
+open UpwardEnumerable
+
+variable [UpwardEnumerable α] [UpwardEnumerable β]
+
+theorem LawfulUpwardEnumerable.ofMap [LawfulUpwardEnumerable β] (f : Map α β) :
+    LawfulUpwardEnumerable α where
+  ne_of_lt a b := by
+    simpa only [f.lt_iff, ← f.injective.ne_iff] using LawfulUpwardEnumerable.ne_of_lt _ _
+  succMany?_zero a := by
+    apply Option.map_injective f.injective
+    simpa [← f.succMany?_toFun] using LawfulUpwardEnumerable.succMany?_zero _
+  succMany?_add_one n a := by
+    apply Option.map_injective f.injective
+    rw [← f.succMany?_toFun, LawfulUpwardEnumerable.succMany?_add_one,
+      f.succMany?_toFun, Option.bind_map, Map.succ?_toFun', Option.map_bind]
+
+instance [LE α] [LT α] [LawfulOrderLT α] [LE β] [LT β] [LawfulOrderLT β] (f : Map α β)
+    [f.PreservesLE] : f.PreservesLT where
+  lt_iff := by simp [lt_iff_le_and_not_ge, Map.PreservesLE.le_iff (f := f)]
+
+theorem LawfulUpwardEnumerableLE.ofMap [LE α] [LE β] [LawfulUpwardEnumerableLE β] (f : Map α β)
+    [f.PreservesLE] : LawfulUpwardEnumerableLE α where
+  le_iff := by simp [Map.PreservesLE.le_iff (f := f), f.le_iff, LawfulUpwardEnumerableLE.le_iff]
+
+theorem LawfulUpwardEnumerableLT.ofMap [LT α] [LT β] [LawfulUpwardEnumerableLT β] (f : Map α β)
+    [f.PreservesLT] : LawfulUpwardEnumerableLT α where
+  lt_iff := by simp [Map.PreservesLT.lt_iff (f := f), f.lt_iff, LawfulUpwardEnumerableLT.lt_iff]
+
+theorem LawfulUpwardEnumerableLeast?.ofMap [Least? α] [Least? β] [LawfulUpwardEnumerableLeast? β]
+    (f : Map α β) [f.PreservesLeast?] : LawfulUpwardEnumerableLeast? α where
+  least?_le a := by
+    obtain ⟨l, hl, hl'⟩ := LawfulUpwardEnumerableLeast?.least?_le (f.toFun a)
+    have : (Least?.least? (α := α)).isSome := by
+      rw [← Option.isSome_map (f := f.toFun), Map.PreservesLeast?.map_least?,
+        hl, Option.isSome_some]
+    refine ⟨Option.get _ this, by simp, ?_⟩
+    rw [f.le_iff, Option.apply_get (f := f.toFun)]
+    simpa [Map.PreservesLeast?.map_least?, hl] using hl'
+
+end PRange
+
+open PRange PRange.UpwardEnumerable
+
+variable [UpwardEnumerable α] [UpwardEnumerable β]
+
+theorem Rxc.LawfulHasSize.ofMap [LE α] [LE β] [Rxc.HasSize α] [Rxc.HasSize β] [Rxc.LawfulHasSize β]
+    (f : Map α β) [f.PreservesLE] [f.PreservesRxcSize] : Rxc.LawfulHasSize α where
+  size_eq_zero_of_not_le a b := by
+    simpa [Map.PreservesRxcSize.size_eq (f := f), Map.PreservesLE.le_iff (f := f)] using
+      Rxc.LawfulHasSize.size_eq_zero_of_not_le _ _
+  size_eq_one_of_succ?_eq_none lo hi := by
+    simpa [Map.PreservesRxcSize.size_eq (f := f), Map.PreservesLE.le_iff (f := f),
+        f.succ?_eq_none_iff] using
+      Rxc.LawfulHasSize.size_eq_one_of_succ?_eq_none _ _
+  size_eq_succ_of_succ?_eq_some lo hi lo' := by
+    simpa [Map.PreservesRxcSize.size_eq (f := f), Map.PreservesLE.le_iff (f := f),
+        f.succ?_eq_some_iff] using
+      Rxc.LawfulHasSize.size_eq_succ_of_succ?_eq_some _ _ _
+
+theorem Rxo.LawfulHasSize.ofMap [LT α] [LT β] [Rxo.HasSize α] [Rxo.HasSize β] [Rxo.LawfulHasSize β]
+    (f : Map α β) [f.PreservesLT] [f.PreservesRxoSize] : Rxo.LawfulHasSize α where
+  size_eq_zero_of_not_le a b := by
+    simpa [Map.PreservesRxoSize.size_eq (f := f), Map.PreservesLT.lt_iff (f := f)] using
+      Rxo.LawfulHasSize.size_eq_zero_of_not_le _ _
+  size_eq_one_of_succ?_eq_none lo hi := by
+    simpa [Map.PreservesRxoSize.size_eq (f := f), Map.PreservesLT.lt_iff (f := f),
+        f.succ?_eq_none_iff] using
+      Rxo.LawfulHasSize.size_eq_one_of_succ?_eq_none _ _
+  size_eq_succ_of_succ?_eq_some lo hi lo' := by
+    simpa [Map.PreservesRxoSize.size_eq (f := f), Map.PreservesLT.lt_iff (f := f),
+        f.succ?_eq_some_iff] using
+      Rxo.LawfulHasSize.size_eq_succ_of_succ?_eq_some _ _ _
+
+theorem Rxi.LawfulHasSize.ofMap [Rxi.HasSize α] [Rxi.HasSize β] [Rxi.LawfulHasSize β]
+    (f : Map α β) [f.PreservesRxiSize] : Rxi.LawfulHasSize α where
+  size_eq_one_of_succ?_eq_none lo := by
+    simpa [Map.PreservesRxiSize.size_eq (f := f), f.succ?_eq_none_iff] using
+      Rxi.LawfulHasSize.size_eq_one_of_succ?_eq_none _
+  size_eq_succ_of_succ?_eq_some lo lo' := by
+    simpa [Map.PreservesRxiSize.size_eq (f := f), f.succ?_eq_some_iff] using
+      Rxi.LawfulHasSize.size_eq_succ_of_succ?_eq_some _ _
+
+theorem Rxc.IsAlwaysFinite.ofMap [LE α] [LE β] [Rxc.IsAlwaysFinite β] (f : Map α β)
+    [f.PreservesLE] : Rxc.IsAlwaysFinite α where
+  finite init hi := by
+    obtain ⟨n, hn⟩ := Rxc.IsAlwaysFinite.finite (f.toFun init) (f.toFun hi)
+    exact ⟨n, by simpa [f.succMany?_toFun, Map.PreservesLE.le_iff (f := f)] using hn⟩
+
+theorem Rxo.IsAlwaysFinite.ofMap [LT α] [LT β] [Rxo.IsAlwaysFinite β] (f : Map α β)
+    [f.PreservesLT] : Rxo.IsAlwaysFinite α where
+  finite init hi := by
+    obtain ⟨n, hn⟩ := Rxo.IsAlwaysFinite.finite (f.toFun init) (f.toFun hi)
+    exact ⟨n, by simpa [f.succMany?_toFun, Map.PreservesLT.lt_iff (f := f)] using hn⟩
+
+theorem Rxi.IsAlwaysFinite.ofMap [Rxi.IsAlwaysFinite β] (f : Map α β) : Rxi.IsAlwaysFinite α where
+  finite init := by
+    obtain ⟨n, hn⟩ := Rxi.IsAlwaysFinite.finite (f.toFun init)
+    exact ⟨n, by simpa [f.succMany?_toFun] using hn⟩
+
+end Std

src/Init/Data/SInt/Basic.lean

@@ -157,7 +157,7 @@ Converts an 8-bit signed integer to a natural number, mapping all negative numbe
 
 Use `Int8.toBitVec` to obtain the two's complement representation.
 -/
-@[inline] def Int8.toNatClampNeg (i : Int8) : Nat := i.toInt.toNat
+@[suggest_for Int8.toNat, inline] def Int8.toNatClampNeg (i : Int8) : Nat := i.toInt.toNat
 
 /-- Obtains the `Int8` whose 2's complement representation is the given `BitVec 8`. -/
 @[inline] def Int8.ofBitVec (b : BitVec 8) : Int8 := ⟨⟨b⟩⟩
@@ -510,7 +510,7 @@ Converts a 16-bit signed integer to a natural number, mapping all negative numbe
 
 Use `Int16.toBitVec` to obtain the two's complement representation.
 -/
-@[inline] def Int16.toNatClampNeg (i : Int16) : Nat := i.toInt.toNat
+@[suggest_for Int16.toNat, inline] def Int16.toNatClampNeg (i : Int16) : Nat := i.toInt.toNat
 
 /-- Obtains the `Int16` whose 2's complement representation is the given `BitVec 16`. -/
 @[inline] def Int16.ofBitVec (b : BitVec 16) : Int16 := ⟨⟨b⟩⟩
@@ -880,7 +880,7 @@ Converts a 32-bit signed integer to a natural number, mapping all negative numbe
 
 Use `Int32.toBitVec` to obtain the two's complement representation.
 -/
-@[inline] def Int32.toNatClampNeg (i : Int32) : Nat := i.toInt.toNat
+@[suggest_for Int32.toNat, inline] def Int32.toNatClampNeg (i : Int32) : Nat := i.toInt.toNat
 
 /-- Obtains the `Int32` whose 2's complement representation is the given `BitVec 32`. -/
 @[inline] def Int32.ofBitVec (b : BitVec 32) : Int32 := ⟨⟨b⟩⟩
@@ -1270,7 +1270,7 @@ Converts a 64-bit signed integer to a natural number, mapping all negative numbe
 
 Use `Int64.toBitVec` to obtain the two's complement representation.
 -/
-@[inline] def Int64.toNatClampNeg (i : Int64) : Nat := i.toInt.toNat
+@[suggest_for Int64.toNat, inline] def Int64.toNatClampNeg (i : Int64) : Nat := i.toInt.toNat
 
 /-- Obtains the `Int64` whose 2's complement representation is the given `BitVec 64`. -/
 @[inline] def Int64.ofBitVec (b : BitVec 64) : Int64 := ⟨⟨b⟩⟩
@@ -1637,7 +1637,7 @@ Converts a word-sized signed integer to a natural number, mapping all negative n
 
 Use `ISize.toBitVec` to obtain the two's complement representation.
 -/
-@[inline] def ISize.toNatClampNeg (i : ISize) : Nat := i.toInt.toNat
+@[suggest_for ISize.toNat, inline] def ISize.toNatClampNeg (i : ISize) : Nat := i.toInt.toNat
 
 /-- Obtains the `ISize` whose 2's complement representation is the given `BitVec`. -/
 @[inline] def ISize.ofBitVec (b : BitVec System.Platform.numBits) : ISize := ⟨⟨b⟩⟩

src/Init/Grind/Util.lean

@@ -4,12 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Init.Classical
-
 public section
-
 namespace Lean.Grind
 
 /-- A helper gadget for annotating nested proofs in goals. -/

src/Init/Prelude.lean

@@ -2810,6 +2810,8 @@ structure Char where
   /-- The value must be a legal scalar value. -/
   valid : val.isValidChar
 
+grind_pattern Char.valid => self.val
+
 private theorem isValidChar_UInt32 {n : Nat} (h : n.isValidChar) : LT.lt n UInt32.size :=
   match h with
   | Or.inl h      => Nat.lt_trans h (of_decide_eq_true rfl)

src/Init/Sym/Lemmas.lean

@@ -14,6 +14,8 @@ public section
 namespace Lean.Sym
 
 theorem ne_self (a : α) : (a ≠ a) = False := by simp
+theorem not_true_eq : (¬ True) = False := by simp
+theorem not_false_eq : (¬ False) = True := by simp
 
 theorem ite_cond_congr {α : Sort u} (c : Prop) {inst : Decidable c} (a b : α)
     (c' : Prop) {inst' : Decidable c'} (h : c = c') : @ite α c inst a b = @ite α c' inst' a b := by
@@ -46,6 +48,8 @@ theorem UInt32.lt_eq_true (a b : UInt32) (h : decide (a < b) = true) : (a < b) =
 theorem UInt64.lt_eq_true (a b : UInt64) (h : decide (a < b) = true) : (a < b) = True := by simp_all
 theorem Fin.lt_eq_true (a b : Fin n) (h : decide (a < b) = true) : (a < b) = True := by simp_all
 theorem BitVec.lt_eq_true (a b : BitVec n) (h : decide (a < b) = true) : (a < b) = True := by simp_all
+theorem String.lt_eq_true (a b : String) (h : decide (a < b) = true) : (a < b) = True := by simp_all
+theorem Char.lt_eq_true (a b : Char) (h : decide (a < b) = true) : (a < b) = True := by simp_all
 
 theorem Nat.lt_eq_false (a b : Nat) (h : decide (a < b) = false) : (a < b) = False := by simp_all
 theorem Int.lt_eq_false (a b : Int) (h : decide (a < b) = false) : (a < b) = False := by simp_all
@@ -60,6 +64,8 @@ theorem UInt32.lt_eq_false (a b : UInt32) (h : decide (a < b) = false) : (a < b)
 theorem UInt64.lt_eq_false (a b : UInt64) (h : decide (a < b) = false) : (a < b) = False := by simp_all
 theorem Fin.lt_eq_false (a b : Fin n) (h : decide (a < b) = false) : (a < b) = False := by simp_all
 theorem BitVec.lt_eq_false (a b : BitVec n) (h : decide (a < b) = false) : (a < b) = False := by simp_all
+theorem String.lt_eq_false (a b : String) (h : decide (a < b) = false) : (a < b) = False := by simp_all
+theorem Char.lt_eq_false (a b : Char) (h : decide (a < b) = false) : (a < b) = False := by simp_all
 
 theorem Nat.le_eq_true (a b : Nat) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
 theorem Int.le_eq_true (a b : Int) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
@@ -74,6 +80,8 @@ theorem UInt32.le_eq_true (a b : UInt32) (h : decide (a ≤ b) = true) : (a ≤
 theorem UInt64.le_eq_true (a b : UInt64) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
 theorem Fin.le_eq_true (a b : Fin n) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
 theorem BitVec.le_eq_true (a b : BitVec n) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
+theorem String.le_eq_true (a b : String) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
+theorem Char.le_eq_true (a b : Char) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
 
 theorem Nat.le_eq_false (a b : Nat) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
 theorem Int.le_eq_false (a b : Int) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
@@ -88,62 +96,8 @@ theorem UInt32.le_eq_false (a b : UInt32) (h : decide (a ≤ b) = false) : (a
 theorem UInt64.le_eq_false (a b : UInt64) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
 theorem Fin.le_eq_false (a b : Fin n) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
 theorem BitVec.le_eq_false (a b : BitVec n) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
-
-theorem Nat.gt_eq_true (a b : Nat) (h : decide (a > b) = true) : (a > b) = True := by simp_all
-theorem Int.gt_eq_true (a b : Int) (h : decide (a > b) = true) : (a > b) = True := by simp_all
-theorem Rat.gt_eq_true (a b : Rat) (h : decide (a > b) = true) : (a > b) = True := by simp_all
-theorem Int8.gt_eq_true (a b : Int8) (h : decide (a > b) = true) : (a > b) = True := by simp_all
-theorem Int16.gt_eq_true (a b : Int16) (h : decide (a > b) = true) : (a > b) = True := by simp_all
-theorem Int32.gt_eq_true (a b : Int32) (h : decide (a > b) = true) : (a > b) = True := by simp_all
-theorem Int64.gt_eq_true (a b : Int64) (h : decide (a > b) = true) : (a > b) = True := by simp_all
-theorem UInt8.gt_eq_true (a b : UInt8) (h : decide (a > b) = true) : (a > b) = True := by simp_all
-theorem UInt16.gt_eq_true (a b : UInt16) (h : decide (a > b) = true) : (a > b) = True := by simp_all
-theorem UInt32.gt_eq_true (a b : UInt32) (h : decide (a > b) = true) : (a > b) = True := by simp_all
-theorem UInt64.gt_eq_true (a b : UInt64) (h : decide (a > b) = true) : (a > b) = True := by simp_all
-theorem Fin.gt_eq_true (a b : Fin n) (h : decide (a > b) = true) : (a > b) = True := by simp_all
-theorem BitVec.gt_eq_true (a b : BitVec n) (h : decide (a > b) = true) : (a > b) = True := by simp_all
-
-theorem Nat.gt_eq_false (a b : Nat) (h : decide (a > b) = false) : (a > b) = False := by simp_all
-theorem Int.gt_eq_false (a b : Int) (h : decide (a > b) = false) : (a > b) = False := by simp_all
-theorem Rat.gt_eq_false (a b : Rat) (h : decide (a > b) = false) : (a > b) = False := by simp_all
-theorem Int8.gt_eq_false (a b : Int8) (h : decide (a > b) = false) : (a > b) = False := by simp_all
-theorem Int16.gt_eq_false (a b : Int16) (h : decide (a > b) = false) : (a > b) = False := by simp_all
-theorem Int32.gt_eq_false (a b : Int32) (h : decide (a > b) = false) : (a > b) = False := by simp_all
-theorem Int64.gt_eq_false (a b : Int64) (h : decide (a > b) = false) : (a > b) = False := by simp_all
-theorem UInt8.gt_eq_false (a b : UInt8) (h : decide (a > b) = false) : (a > b) = False := by simp_all
-theorem UInt16.gt_eq_false (a b : UInt16) (h : decide (a > b) = false) : (a > b) = False := by simp_all
-theorem UInt32.gt_eq_false (a b : UInt32) (h : decide (a > b) = false) : (a > b) = False := by simp_all
-theorem UInt64.gt_eq_false (a b : UInt64) (h : decide (a > b) = false) : (a > b) = False := by simp_all
-theorem Fin.gt_eq_false (a b : Fin n) (h : decide (a > b) = false) : (a > b) = False := by simp_all
-theorem BitVec.gt_eq_false (a b : BitVec n) (h : decide (a > b) = false) : (a > b) = False := by simp_all
-
-theorem Nat.ge_eq_true (a b : Nat) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
-theorem Int.ge_eq_true (a b : Int) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
-theorem Rat.ge_eq_true (a b : Rat) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
-theorem Int8.ge_eq_true (a b : Int8) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
-theorem Int16.ge_eq_true (a b : Int16) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
-theorem Int32.ge_eq_true (a b : Int32) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
-theorem Int64.ge_eq_true (a b : Int64) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
-theorem UInt8.ge_eq_true (a b : UInt8) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
-theorem UInt16.ge_eq_true (a b : UInt16) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
-theorem UInt32.ge_eq_true (a b : UInt32) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
-theorem UInt64.ge_eq_true (a b : UInt64) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
-theorem Fin.ge_eq_true (a b : Fin n) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
-theorem BitVec.ge_eq_true (a b : BitVec n) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
-
-theorem Nat.ge_eq_false (a b : Nat) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
-theorem Int.ge_eq_false (a b : Int) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
-theorem Rat.ge_eq_false (a b : Rat) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
-theorem Int8.ge_eq_false (a b : Int8) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
-theorem Int16.ge_eq_false (a b : Int16) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
-theorem Int32.ge_eq_false (a b : Int32) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
-theorem Int64.ge_eq_false (a b : Int64) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
-theorem UInt8.ge_eq_false (a b : UInt8) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
-theorem UInt16.ge_eq_false (a b : UInt16) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
-theorem UInt32.ge_eq_false (a b : UInt32) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
-theorem UInt64.ge_eq_false (a b : UInt64) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
-theorem Fin.ge_eq_false (a b : Fin n) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
-theorem BitVec.ge_eq_false (a b : BitVec n) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
+theorem String.le_eq_false (a b : String) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
+theorem Char.le_eq_false (a b : Char) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
 
 theorem Nat.eq_eq_true (a b : Nat) (h : decide (a = b) = true) : (a = b) = True := by simp_all
 theorem Int.eq_eq_true (a b : Int) (h : decide (a = b) = true) : (a = b) = True := by simp_all
@@ -158,6 +112,8 @@ theorem UInt32.eq_eq_true (a b : UInt32) (h : decide (a = b) = true) : (a = b) =
 theorem UInt64.eq_eq_true (a b : UInt64) (h : decide (a = b) = true) : (a = b) = True := by simp_all
 theorem Fin.eq_eq_true (a b : Fin n) (h : decide (a = b) = true) : (a = b) = True := by simp_all
 theorem BitVec.eq_eq_true (a b : BitVec n) (h : decide (a = b) = true) : (a = b) = True := by simp_all
+theorem String.eq_eq_true (a b : String) (h : decide (a = b) = true) : (a = b) = True := by simp_all
+theorem Char.eq_eq_true (a b : Char) (h : decide (a = b) = true) : (a = b) = True := by simp_all
 
 theorem Nat.eq_eq_false (a b : Nat) (h : decide (a = b) = false) : (a = b) = False := by simp_all
 theorem Int.eq_eq_false (a b : Int) (h : decide (a = b) = false) : (a = b) = False := by simp_all
@@ -172,34 +128,8 @@ theorem UInt32.eq_eq_false (a b : UInt32) (h : decide (a = b) = false) : (a = b)
 theorem UInt64.eq_eq_false (a b : UInt64) (h : decide (a = b) = false) : (a = b) = False := by simp_all
 theorem Fin.eq_eq_false (a b : Fin n) (h : decide (a = b) = false) : (a = b) = False := by simp_all
 theorem BitVec.eq_eq_false (a b : BitVec n) (h : decide (a = b) = false) : (a = b) = False := by simp_all
-
-theorem Nat.ne_eq_true (a b : Nat) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
-theorem Int.ne_eq_true (a b : Int) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
-theorem Rat.ne_eq_true (a b : Rat) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
-theorem Int8.ne_eq_true (a b : Int8) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
-theorem Int16.ne_eq_true (a b : Int16) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
-theorem Int32.ne_eq_true (a b : Int32) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
-theorem Int64.ne_eq_true (a b : Int64) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
-theorem UInt8.ne_eq_true (a b : UInt8) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
-theorem UInt16.ne_eq_true (a b : UInt16) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
-theorem UInt32.ne_eq_true (a b : UInt32) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
-theorem UInt64.ne_eq_true (a b : UInt64) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
-theorem Fin.ne_eq_true (a b : Fin n) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
-theorem BitVec.ne_eq_true (a b : BitVec n) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
-
-theorem Nat.ne_eq_false (a b : Nat) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
-theorem Int.ne_eq_false (a b : Int) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
-theorem Rat.ne_eq_false (a b : Rat) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
-theorem Int8.ne_eq_false (a b : Int8) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
-theorem Int16.ne_eq_false (a b : Int16) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
-theorem Int32.ne_eq_false (a b : Int32) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
-theorem Int64.ne_eq_false (a b : Int64) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
-theorem UInt8.ne_eq_false (a b : UInt8) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
-theorem UInt16.ne_eq_false (a b : UInt16) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
-theorem UInt32.ne_eq_false (a b : UInt32) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
-theorem UInt64.ne_eq_false (a b : UInt64) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
-theorem Fin.ne_eq_false (a b : Fin n) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
-theorem BitVec.ne_eq_false (a b : BitVec n) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
+theorem String.eq_eq_false (a b : String) (h : decide (a = b) = false) : (a = b) = False := by simp_all
+theorem Char.eq_eq_false (a b : Char) (h : decide (a = b) = false) : (a = b) = False := by simp_all
 
 theorem Nat.dvd_eq_true (a b : Nat) (h : decide (a ∣ b) = true) : (a ∣ b) = True := by simp_all
 theorem Int.dvd_eq_true (a b : Int) (h : decide (a ∣ b) = true) : (a ∣ b) = True := by simp_all

src/Init/Tactics.lean

@@ -518,14 +518,13 @@ syntax location := withPosition(ppGroup(" at" (locationWildcard <|> locationHyp)
   assuming these are definitionally equal.
 * `change t' at h` will change hypothesis `h : t` to have type `t'`, assuming
   assuming `t` and `t'` are definitionally equal.
--/
-syntax (name := change) "change " term (location)? : tactic
-
-/--
 * `change a with b` will change occurrences of `a` to `b` in the goal,
   assuming `a` and `b` are definitionally equal.
 * `change a with b at h` similarly changes `a` to `b` in the type of hypothesis `h`.
 -/
+syntax (name := change) "change " term (location)? : tactic
+
+@[tactic_alt change]
 syntax (name := changeWith) "change " term " with " term (location)? : tactic
 
 /--
@@ -905,8 +904,13 @@ The tactic supports all the same syntax variants and options as the `let` term.
 -/
 macro "let" c:letConfig d:letDecl : tactic => `(tactic| refine_lift let $c:letConfig $d:letDecl; ?_)
 
-/-- `let rec f : t := e` adds a recursive definition `f` to the current goal.
-The syntax is the same as term-mode `let rec`. -/
+/--
+`let rec f : t := e` adds a recursive definition `f` to the current goal.
+The syntax is the same as term-mode `let rec`.
+
+The tactic supports all the same syntax variants and options as the `let` term.
+-/
+@[tactic_name "let rec"]
 syntax (name := letrec) withPosition(atomic("let " &"rec ") letRecDecls) : tactic
 macro_rules
   | `(tactic| let rec $d) => `(tactic| refine_lift let rec $d; ?_)
@@ -1212,22 +1216,6 @@ while `congr 2` produces the intended `⊢ x + y = y + x`.
 syntax (name := congr) "congr" (ppSpace num)? : tactic
 
 
-/--
-In tactic mode, `if h : t then tac1 else tac2` can be used as alternative syntax for:
-```
-by_cases h : t
-· tac1
-· tac2
-```
-It performs case distinction on `h : t` or `h : ¬t` and `tac1` and `tac2` are the subproofs.
-
-You can use `?_` or `_` for either subproof to delay the goal to after the tactic, but
-if a tactic sequence is provided for `tac1` or `tac2` then it will require the goal to be closed
-by the end of the block.
--/
-syntax (name := tacDepIfThenElse)
-  ppRealGroup(ppRealFill(ppIndent("if " binderIdent " : " term " then") ppSpace matchRhsTacticSeq)
-    ppDedent(ppSpace) ppRealFill("else " matchRhsTacticSeq)) : tactic
 
 /--
 In tactic mode, `if t then tac1 else tac2` is alternative syntax for:
@@ -1236,16 +1224,34 @@ by_cases t
 · tac1
 · tac2
 ```
-It performs case distinction on `h† : t` or `h† : ¬t`, where `h†` is an anonymous
-hypothesis, and `tac1` and `tac2` are the subproofs. (It doesn't actually use
-nondependent `if`, since this wouldn't add anything to the context and hence would be
-useless for proving theorems. To actually insert an `ite` application use
-`refine if t then ?_ else ?_`.)
+It performs case distinction on `h† : t` or `h† : ¬t`, where `h†` is an anonymous hypothesis, and
+`tac1` and `tac2` are the subproofs. (It doesn't actually use nondependent `if`, since this wouldn't
+add anything to the context and hence would be useless for proving theorems. To actually insert an
+`ite` application use `refine if t then ?_ else ?_`.)
+
+The assumptions in each subgoal can be named. `if h : t then tac1 else tac2` can be used as
+alternative syntax for:
+```
+by_cases h : t
+· tac1
+· tac2
+```
+It performs case distinction on `h : t` or `h : ¬t`.
+
+You can use `?_` or `_` for either subproof to delay the goal to after the tactic, but
+if a tactic sequence is provided for `tac1` or `tac2` then it will require the goal to be closed
+by the end of the block.
 -/
 syntax (name := tacIfThenElse)
   ppRealGroup(ppRealFill(ppIndent("if " term " then") ppSpace matchRhsTacticSeq)
     ppDedent(ppSpace) ppRealFill("else " matchRhsTacticSeq)) : tactic
 
+
+@[tactic_alt tacIfThenElse]
+syntax (name := tacDepIfThenElse)
+  ppRealGroup(ppRealFill(ppIndent("if " binderIdent " : " term " then") ppSpace matchRhsTacticSeq)
+    ppDedent(ppSpace) ppRealFill("else " matchRhsTacticSeq)) : tactic
+
 /--
 The tactic `nofun` is shorthand for `exact nofun`: it introduces the assumptions, then performs an
 empty pattern match, closing the goal if the introduced pattern is impossible.

src/Lean/Compiler/ModPkgExt.lean

@@ -56,9 +56,9 @@ public def Environment.getModulePackageByIdx? (env : Environment) (idx : ModuleI
 Returns the standard base of the native symbol for the compiled constant {lean}`declName`.
 
 For many constants, this is the full symbol. However, initializers have an additional prefix
-(i.e., {lit}`_init_`) and boxed functions have an additional suffix (i.e., {lit}`___boxed`).
-Furthermore, some constants do not use this stem at all (e.g., {lit}`main` and definitions
-with {lit}`@[export]`).
+(i.e., {lit}`_init_`) and boxed functions have an additional suffix
+(see {name}`mkMangledBoxedName`). Furthermore, some constants do not use this stem at all
+(e.g., {lit}`main` and definitions with {lit}`@[export]`).
 -/
 @[export lean_get_symbol_stem]
 public def getSymbolStem (env : Environment) (declName : Name) : String :=

src/Lean/Compiler/NameMangling.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Lean.Setup
-import Init.Data.String.Termination
+import Init.Data.String.TakeDrop
 
 namespace String
 
@@ -133,6 +133,18 @@ def Name.mangleAux : Name → String
 public def Name.mangle (n : Name) (pre : String := "l_") : String :=
   pre ++ Name.mangleAux n
 
+/--
+Given `s = nm.mangle pre` for some `nm : Name` and `pre : String` with `nm != Name.anonymous`,
+returns `(mkBoxedName nm).mangle pre`. This is used in the interpreter to find names of boxed
+IR declarations.
+-/
+@[export lean_mk_mangled_boxed_name]
+public def mkMangledBoxedName (s : String) : String :=
+  if s.endsWith "__" then
+    s ++ "_00__boxed"
+  else
+    s ++ "___boxed"
+
 /--
 The mangled name of the name used to create the module initialization function.
 

src/Lean/DocString/Add.lean

@@ -125,7 +125,7 @@ Parses and elaborates a Verso module docstring.
 def versoModDocString
     (range : DeclarationRange) (doc : TSyntax ``document) :
     TermElabM VersoModuleDocs.Snippet := do
-  let level := getVersoModuleDocs (← getEnv) |>.terminalNesting |>.map (· + 1)
+  let level := getMainVersoModuleDocs (← getEnv) |>.terminalNesting |>.map (· + 1)
   Doc.elabModSnippet range (doc.raw.getArgs.map (⟨·⟩)) (level.getD 0) |>.execForModule
 
 

src/Lean/DocString/Extension.lean

@@ -409,11 +409,29 @@ private builtin_initialize versoModuleDocExt :
 }
 
 
-def getVersoModuleDocs (env : Environment) : VersoModuleDocs :=
+/--
+Returns the Verso module docs for the current main module.
+
+During elaboration, this will return the modules docs that have been added thus far, rather than
+those for the entire module.
+-/
+def getMainVersoModuleDocs (env : Environment) : VersoModuleDocs :=
   versoModuleDocExt.getState env
 
+@[deprecated getMainVersoModuleDocs (since := "2026-01-21")]
+def getVersoModuleDocs := @getMainVersoModuleDocs
+
+
+/--
+Returns all snippets of the Verso module docs from the indicated module, if they exist.
+-/
+def getVersoModuleDoc? (env : Environment) (moduleName : Name) :
+    Option (Array VersoModuleDocs.Snippet) :=
+  env.getModuleIdx? moduleName |>.map fun modIdx =>
+    versoModuleDocExt.getModuleEntries (level := .server) env modIdx
+
 def addVersoModuleDocSnippet (env : Environment) (snippet : VersoModuleDocs.Snippet) : Except String Environment :=
-  let docs := getVersoModuleDocs env
+  let docs := getMainVersoModuleDocs env
   if docs.canAdd snippet then
     pure <| versoModuleDocExt.addEntry env snippet
   else throw s!"Can't add - incorrect nesting {docs.terminalNesting.map (s!"(expected at most {·})") |>.getD ""})"

src/Lean/Elab/BuiltinCommand.lean

@@ -21,7 +21,7 @@ namespace Lean.Elab.Command
 
   match stx[1] with
   | Syntax.atom _ val =>
-    if getVersoModuleDocs (← getEnv) |>.isEmpty then
+    if getMainVersoModuleDocs (← getEnv) |>.isEmpty then
       let doc := String.Pos.Raw.extract val 0 (val.rawEndPos.unoffsetBy ⟨2⟩)
       modifyEnv fun env => addMainModuleDoc env ⟨doc, range⟩
     else

src/Lean/Elab/Tactic/Doc.lean

@@ -8,6 +8,7 @@ module
 prelude
 import Lean.DocString
 public import Lean.Elab.Command
+public import Lean.Parser.Tactic.Doc
 
 public section
 
@@ -38,30 +39,42 @@ open Lean.Parser.Command
   | _ => throwError "Malformed 'register_tactic_tag' command"
 
 /--
-Gets the first string token in a parser description. For example, for a declaration like
-`syntax "squish " term " with " term : tactic`, it returns `some "squish "`, and for a declaration
-like `syntax tactic " <;;;> " tactic : tactic`, it returns `some " <;;;> "`.
-
-Returns `none` for syntax declarations that don't contain a string constant.
+Computes a table that heuristically maps parser syntax kinds to their first tokens by inspecting the
+Pratt parsing tables for the `tactic syntax kind. If a custom name is provided for the tactic, then
+it is returned instead.
 -/
-private partial def getFirstTk (e : Expr) : MetaM (Option String) := do
-  match (← Meta.whnf e).getAppFnArgs with
-  | (``ParserDescr.node, #[_, _, p]) => getFirstTk p
-  | (``ParserDescr.trailingNode, #[_, _, _, p]) => getFirstTk p
-  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "withPosition")), p]) => getFirstTk p
-  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "atomic")), p]) => getFirstTk p
-  | (``ParserDescr.binary, #[.app _ (.lit (.strVal "andthen")), p, _]) => getFirstTk p
-  | (``ParserDescr.nonReservedSymbol, #[.lit (.strVal tk), _]) => pure (some tk)
-  | (``ParserDescr.symbol, #[.lit (.strVal tk)]) => pure (some tk)
-  | (``Parser.withAntiquot, #[_, p]) => getFirstTk p
-  | (``Parser.leadingNode, #[_, _, p]) => getFirstTk p
-  | (``HAndThen.hAndThen, #[_, _, _, _, p1, p2]) =>
-    if let some tk ← getFirstTk p1 then pure (some tk)
-    else getFirstTk (.app p2 (.const ``Unit.unit []))
-  | (``Parser.nonReservedSymbol, #[.lit (.strVal tk), _]) => pure (some tk)
-  | (``Parser.symbol, #[.lit (.strVal tk)]) => pure (some tk)
-  | _ => pure none
+def firstTacticTokens [Monad m] [MonadEnv m] : m (NameMap String) := do
+  let env ← getEnv
 
+  let some tactics := (Lean.Parser.parserExtension.getState env).categories.find? `tactic
+    | return {}
+
+  let mut firstTokens : NameMap String :=
+    tacticNameExt.toEnvExtension.getState env
+      |>.importedEntries
+      |>.push (tacticNameExt.exportEntriesFn env (tacticNameExt.getState env) .exported)
+      |>.foldl (init := {}) fun names inMods =>
+        inMods.foldl (init := names) fun names (k, n) =>
+          names.insert k n
+
+  firstTokens := addFirstTokens tactics tactics.tables.leadingTable firstTokens
+  firstTokens := addFirstTokens tactics tactics.tables.trailingTable firstTokens
+
+  return firstTokens
+where
+  addFirstTokens tactics table firsts : NameMap String := Id.run do
+    let mut firsts := firsts
+    for (tok, ps) in table do
+      -- Skip antiquotes
+      if tok == `«$» then continue
+      for (p, _) in ps do
+        for (k, ()) in p.info.collectKinds {} do
+          if tactics.kinds.contains k then
+            let tok := tok.toString (escape := false)
+            -- It's important here that the already-existing mapping is preserved, because it will
+            -- contain any user-provided custom name, and these shouldn't be overridden.
+            firsts := firsts.alter k (·.getD tok)
+    return firsts
 
 /--
 Creates some `MessageData` for a parser name.
@@ -71,18 +84,14 @@ identifiable leading token, then that token is shown. Otherwise, the underlying
 without an `@`. The name includes metadata that makes infoview hovers and the like work. This
 only works for global constants, as the local context is not included.
 -/
-private def showParserName (n : Name) : MetaM MessageData := do
+private def showParserName [Monad m] [MonadEnv m] (firsts : NameMap String) (n : Name) : m MessageData := do
   let env ← getEnv
   let params :=
     env.constants.find?' n |>.map (·.levelParams.map Level.param) |>.getD []
-  let tok ←
-    if let some descr := env.find? n |>.bind (·.value?) then
-      if let some tk ← getFirstTk descr then
-        pure <| Std.Format.text tk.trimAscii.copy
-      else pure <| format n
-    else pure <| format n
+
+  let tok := ((← customTacticName n) <|> firsts.get? n).map Std.Format.text |>.getD (format n)
   pure <| .ofFormatWithInfos {
-    fmt := "'" ++ .tag 0 tok ++ "'",
+    fmt := "`" ++ .tag 0 tok ++ "`",
     infos :=
       .ofList [(0, .ofTermInfo {
         lctx := .empty,
@@ -93,7 +102,6 @@ private def showParserName (n : Name) : MetaM MessageData := do
       })] _
   }
 
-
 /--
 Displays all available tactic tags, with documentation.
 -/
@@ -106,20 +114,22 @@ Displays all available tactic tags, with documentation.
     for (tac, tag) in arr do
       mapping := mapping.insert tag (mapping.getD tag {} |>.insert tac)
 
+  let firsts ← firstTacticTokens
+
   let showDocs : Option String → MessageData
     | none => .nil
     | some d => Format.line ++ MessageData.joinSep ((d.split '\n').map (toMessageData ∘ String.Slice.copy)).toList Format.line
 
-  let showTactics (tag : Name) : MetaM MessageData := do
+  let showTactics (tag : Name) : CommandElabM MessageData := do
     match mapping.find? tag with
     | none => pure .nil
     | some tacs =>
       if tacs.isEmpty then pure .nil
       else
         let tacs := tacs.toArray.qsort (·.toString < ·.toString) |>.toList
-        pure (Format.line ++ MessageData.joinSep (← tacs.mapM showParserName) ", ")
+        pure (Format.line ++ MessageData.joinSep (← tacs.mapM (showParserName firsts)) ", ")
 
-  let tagDescrs ← liftTermElabM <| (← allTagsWithInfo).mapM fun (name, userName, docs) => do
+  let tagDescrs ← (← allTagsWithInfo).mapM fun (name, userName, docs) => do
     pure <| m!"• " ++
       MessageData.nestD (m!"`{name}`" ++
         (if name.toString != userName then m!" — \"{userName}\"" else MessageData.nil) ++
@@ -146,13 +156,13 @@ structure TacticDoc where
   /-- Any docstring extensions that have been specified -/
   extensionDocs : Array String
 
-def allTacticDocs : MetaM (Array TacticDoc) := do
+def allTacticDocs (includeUnnamed : Bool := true) : MetaM (Array TacticDoc) := do
   let env ← getEnv
-  let all :=
-    tacticTagExt.toEnvExtension.getState (← getEnv)
-      |>.importedEntries |>.push (tacticTagExt.exportEntriesFn (← getEnv) (tacticTagExt.getState (← getEnv)) .exported)
+  let allTags :=
+    tacticTagExt.toEnvExtension.getState env |>.importedEntries
+      |>.push (tacticTagExt.exportEntriesFn env (tacticTagExt.getState env) .exported)
   let mut tacTags : NameMap NameSet := {}
-  for arr in all do
+  for arr in allTags do
     for (tac, tag) in arr do
       tacTags := tacTags.insert tac (tacTags.getD tac {} |>.insert tag)
 
@@ -160,15 +170,18 @@ def allTacticDocs : MetaM (Array TacticDoc) := do
 
   let some tactics := (Lean.Parser.parserExtension.getState env).categories.find? `tactic
     | return #[]
+
+  let firstTokens ← firstTacticTokens
+
   for (tac, _) in tactics.kinds do
     -- Skip noncanonical tactics
     if let some _ := alternativeOfTactic env tac then continue
-    let userName : String ←
-      if let some descr := env.find? tac |>.bind (·.value?) then
-        if let some tk ← getFirstTk descr then
-          pure tk.trimAscii.copy
-        else pure tac.toString
-      else pure tac.toString
+
+    let userName? : Option String := firstTokens.get? tac
+    let userName ←
+      if let some n := userName? then pure n
+      else if includeUnnamed then pure tac.toString
+      else continue
 
     docs := docs.push {
       internalName := tac,

src/Lean/Environment.lean

@@ -179,6 +179,13 @@ structure EnvironmentHeader where
   `ModuleIdx` for the same module.
   -/
   modules      : Array EffectiveImport := #[]
+  /-- For `getModuleIdx?` -/
+  private moduleName2Idx : Std.HashMap Name ModuleIdx := Id.run do
+    let mut m := {}
+    for _h : idx in [0:modules.size] do
+      let mod := modules[idx]
+      m := m.insert mod.module idx
+    return m
   /--
   Subset of `modules` for which `importAll` is `true`. This is assumed to be a much smaller set so
   we precompute it instead of iterating over all of `modules` multiple times. However, note that
@@ -267,7 +274,7 @@ structure Environment where
   -/
   private irBaseExts      : Array EnvExtensionState
   /-- The header contains additional information that is set at import time. -/
-  header                  : EnvironmentHeader := {}
+  header                  : EnvironmentHeader := private_decl% {}
 deriving Nonempty
 
 /-- Exceptions that can be raised by the kernel when type checking new declarations. -/
@@ -1174,7 +1181,7 @@ def isSafeDefinition (env : Environment) (declName : Name) : Bool :=
   | _ => false
 
 def getModuleIdx? (env : Environment) (moduleName : Name) : Option ModuleIdx :=
-  env.header.modules.findIdx? (·.module == moduleName)
+  env.header.moduleName2Idx[moduleName]?
 
 end Environment
 

src/Lean/Meta/Sym/Apply.lean

@@ -44,8 +44,11 @@ first because solving it often solves `?w`.
 def mkResultPos (pattern : Pattern) : List Nat := Id.run do
   let auxPrefix := `_sym_pre
   -- Initialize "found" mask with arguments that can be synthesized by type class resolution.
-  let mut found := pattern.isInstance
   let numArgs := pattern.varTypes.size
+  let mut found := if let some varInfos := pattern.varInfos? then
+     varInfos.argsInfo.map fun info : ProofInstArgInfo => info.isInstance
+  else
+     Array.replicate numArgs false
   let auxVars := pattern.varTypes.mapIdx fun i _ => mkFVar ⟨.num auxPrefix i⟩
   -- Collect arguments that occur in the pattern
   for fvarId in collectFVars {} (pattern.pattern.instantiateRev auxVars) |>.fvarIds do
@@ -96,6 +99,10 @@ def mkValue (expr : Expr) (pattern : Pattern) (result : MatchUnifyResult) : Expr
   else
     mkAppN (expr.instantiateLevelParams pattern.levelParams result.us) result.args
 
+public inductive ApplyResult where
+  | notApplicable
+  | goals (mvarId : List MVarId)
+
 /--
 Applies a backward rule to a goal, returning new subgoals.
 
@@ -103,27 +110,23 @@ Applies a backward rule to a goal, returning new subgoals.
 2. Assigns the goal metavariable to the theorem application
 3. Returns new goals for unassigned arguments (per `resultPos`)
 
-Returns `none` if unification fails.
+Returns `.notApplicable` if unification fails.
 -/
-public def BackwardRule.apply? (mvarId : MVarId) (rule : BackwardRule) : SymM (Option (List MVarId)) := mvarId.withContext do
+public def BackwardRule.apply (mvarId : MVarId) (rule : BackwardRule) : SymM ApplyResult := mvarId.withContext do
   let decl ← mvarId.getDecl
   if let some result ← rule.pattern.unify? decl.type then
     mvarId.assign (mkValue rule.expr rule.pattern result)
-    return some <| rule.resultPos.map fun i =>
+    return .goals <| rule.resultPos.map fun i =>
       result.args[i]!.mvarId!
   else
-    return none
+    return .notApplicable
 
 /--
-Similar to `BackwardRule.apply?`, but throws an error if unification fails.
+Similar to `BackwardRule.apply', but throws an error if unification fails.
 -/
-public def BackwardRule.apply (mvarId : MVarId) (rule : BackwardRule) : SymM (List MVarId) := mvarId.withContext do
-  let decl ← mvarId.getDecl
-  if let some result ← rule.pattern.unify? decl.type then
-    mvarId.assign (mkValue rule.expr rule.pattern result)
-    return rule.resultPos.map fun i =>
-      result.args[i]!.mvarId!
-  else
-    throwError "rule is not applicable to goal{mvarId}rule:{indentExpr rule.expr}"
+public def BackwardRule.apply' (mvarId : MVarId) (rule : BackwardRule) : SymM (List MVarId) := do
+  let .goals mvarIds ← rule.apply mvarId
+    | throwError "rule is not applicable to goal{mvarId}rule:{indentExpr rule.expr}"
+  return mvarIds
 
 end Lean.Meta.Sym

src/Lean/Meta/Sym/LitValues.lean

@@ -73,4 +73,14 @@ def getFinValue? (e : Expr) : OptionT Id FinValue := do
   let : NeZero n := ⟨h⟩
   return { n, val := Fin.ofNat n v }
 
+def getCharValue? (e : Expr) : OptionT Id Char := do
+  let_expr Char.ofNat n := e | failure
+  let .lit (.natVal n) := n | failure
+  return Char.ofNat n
+
+def getStringValue? (e : Expr) : Option String :=
+  match e with
+  | .lit (.strVal s) => some s
+  | _ => none
+
 end Lean.Meta.Sym

src/Lean/Meta/Sym/Pattern.lean

@@ -64,7 +64,11 @@ def mkProofInstInfoMapFor (pattern : Expr) : MetaM (AssocList Name ProofInstInfo
 public structure Pattern where
   levelParams    : List Name
   varTypes       : Array Expr
-  isInstance     : Array Bool
+  /--
+  If `some argsInfo`, `argsInfo` stores whether the pattern variables are instances/proofs.
+  It is `none` if no pattern variables are instance/proof.
+  -/
+  varInfos?      : Option ProofInstInfo
   pattern        : Expr
   fnInfos        : AssocList Name ProofInstInfo
   /--
@@ -78,6 +82,16 @@ public structure Pattern where
 
 def uvarPrefix : Name := `_uvar
 
+/-- Returns `true` if the `i`th argument / pattern variable is an instance. -/
+def Pattern.isInstance (p : Pattern) (i : Nat) : Bool := Id.run do
+  let some varInfos := p.varInfos? | return false
+  varInfos.argsInfo[i]!.isInstance
+
+/-- Returns `true` if the `i`th argument / pattern variable is a proof. -/
+def Pattern.isProof (p : Pattern) (i : Nat) : Bool := Id.run do
+  let some varInfos := p.varInfos? | return false
+  varInfos.argsInfo[i]!.isProof
+
 def isUVar? (n : Name) : Option Nat := Id.run do
   let .num p idx := n | return none
   unless p == uvarPrefix do return none
@@ -144,12 +158,13 @@ where
       else
         mask
 
-def mkPatternCore (levelParams : List Name) (varTypes : Array Expr) (isInstance : Array Bool)
-    (pattern : Expr) : MetaM Pattern := do
+def mkPatternCore (type : Expr) (levelParams : List Name) (varTypes : Array Expr) (pattern : Expr) : MetaM Pattern := do
   let fnInfos ← mkProofInstInfoMapFor pattern
   let checkTypeMask := mkCheckTypeMask pattern varTypes.size
   let checkTypeMask? := if checkTypeMask.all (· == false) then none else some checkTypeMask
-  return { levelParams, varTypes, isInstance, pattern, fnInfos, checkTypeMask? }
+  let varInfos? ← forallBoundedTelescope type varTypes.size fun xs _ =>
+    mkProofInstArgInfo? xs
+  return { levelParams, varTypes, pattern, fnInfos, varInfos?, checkTypeMask? }
 
 /--
 Creates a `Pattern` from the type of a theorem.
@@ -168,12 +183,12 @@ public def mkPatternFromDecl (declName : Name) (num? : Option Nat := none) : Met
   let (levelParams, type) ← preprocessPattern declName
   let hugeNumber := 10000000
   let num := num?.getD hugeNumber
-  let rec go (i : Nat) (type : Expr) (varTypes : Array Expr) (isInstance : Array Bool) : MetaM Pattern := do
+  let rec go (i : Nat) (pattern : Expr) (varTypes : Array Expr) : MetaM Pattern := do
     if i < num then
-      if let .forallE _ d b _ := type then
-        return (← go (i+1) b (varTypes.push d) (isInstance.push (isClass? (← getEnv) d).isSome))
-    mkPatternCore levelParams varTypes isInstance type
-  go 0 type #[] #[]
+      if let .forallE _ d b _ := pattern then
+        return (← go (i+1) b (varTypes.push d))
+    mkPatternCore type levelParams varTypes pattern
+  go 0 type #[]
 
 /--
 Creates a `Pattern` from an equational theorem, using the left-hand side of the equation.
@@ -188,14 +203,14 @@ Throws an error if the theorem's conclusion is not an equality.
 -/
 public def mkEqPatternFromDecl (declName : Name) : MetaM (Pattern × Expr) := do
   let (levelParams, type) ← preprocessPattern declName
-  let rec go (type : Expr) (varTypes : Array Expr) (isInstance : Array Bool) : MetaM (Pattern × Expr) := do
-    if let .forallE _ d b _ := type then
-      return (← go b (varTypes.push d) (isInstance.push (isClass? (← getEnv) d).isSome))
+  let rec go (pattern : Expr) (varTypes : Array Expr) : MetaM (Pattern × Expr) := do
+    if let .forallE _ d b _ := pattern then
+      return (← go b (varTypes.push d))
     else
-      let_expr Eq _ lhs rhs := type | throwError "resulting type for `{.ofConstName declName}` is not an equality"
-      let pattern ← mkPatternCore levelParams varTypes isInstance lhs
+      let_expr Eq _ lhs rhs := pattern | throwError "resulting type for `{.ofConstName declName}` is not an equality"
+      let pattern ← mkPatternCore type levelParams varTypes lhs
       return (pattern, rhs)
-  go type #[] #[]
+  go type #[]
 
 structure UnifyM.Context where
   pattern   : Pattern
@@ -799,7 +814,6 @@ def mkPreResult : UnifyM MkPreResultResult := do
     | none => mkFreshLevelMVar
   let pattern := (← read).pattern
   let varTypes := pattern.varTypes
-  let isInstance := pattern.isInstance
   let eAssignment := (← get).eAssignment
   let tPending := (← get).tPending
   let mut args := #[]
@@ -820,7 +834,7 @@ def mkPreResult : UnifyM MkPreResultResult := do
       let type := varTypes[i]!
       let type ← instantiateLevelParamsS type pattern.levelParams us
       let type ← instantiateRevBetaS type args
-      if isInstance[i]! then
+      if pattern.isInstance i then
         if let .some val ← trySynthInstance type then
           args := args.push (← shareCommon val)
           continue

src/Lean/Meta/Sym/ProofInstInfo.lean

@@ -7,17 +7,38 @@ module
 prelude
 public import Lean.Meta.Sym.SymM
 import Lean.Meta.Sym.IsClass
-import Lean.Meta.Tactic.Grind.Util
+import Lean.Meta.Sym.Util
+import Lean.Meta.Transform
 namespace Lean.Meta.Sym
 
 /--
 Preprocesses types that used for pattern matching and unification.
 -/
 public def preprocessType (type : Expr) : MetaM Expr := do
-  let type ← Grind.unfoldReducible type
+  let type ← Sym.unfoldReducible type
   let type ← Core.betaReduce type
   zetaReduce type
 
+/--
+Analyzes whether the given free variables (aka arguments) are proofs or instances.
+Returns `none` if no arguments are proofs or instances.
+-/
+public def mkProofInstArgInfo? (xs : Array Expr) : MetaM (Option ProofInstInfo) := do
+  let env ← getEnv
+  let mut argsInfo := #[]
+  let mut found := false
+  for x in xs do
+    let type ← Meta.inferType x
+    let isInstance := isClass? env type |>.isSome
+    let isProof ← isProp type
+    if isInstance || isProof then
+      found := true
+    argsInfo := argsInfo.push { isInstance, isProof }
+  if found then
+    return some { argsInfo }
+  else
+    return none
+
 /--
 Analyzes the type signature of `declName` and returns information about which arguments
 are proofs or instances. Returns `none` if no arguments are proofs or instances.
@@ -25,21 +46,7 @@ are proofs or instances. Returns `none` if no arguments are proofs or instances.
 public def mkProofInstInfo? (declName : Name) : MetaM (Option ProofInstInfo) := do
   let info ← getConstInfo declName
   let type ← preprocessType info.type
-  forallTelescopeReducing type fun xs _ => do
-    let env ← getEnv
-    let mut argsInfo := #[]
-    let mut found := false
-    for x in xs do
-      let type ← Meta.inferType x
-      let isInstance := isClass? env type |>.isSome
-      let isProof ← isProp type
-      if isInstance || isProof then
-        found := true
-      argsInfo := argsInfo.push { isInstance, isProof }
-    if found then
-      return some { argsInfo }
-    else
-      return none
+  forallTelescopeReducing type fun xs _ => mkProofInstArgInfo? xs
 
 /--
 Returns information about the type signature of `declName`. It contains information about which arguments

src/Lean/Meta/Sym/Simp.lean

@@ -21,3 +21,4 @@ public import Lean.Meta.Sym.Simp.Debug
 public import Lean.Meta.Sym.Simp.EvalGround
 public import Lean.Meta.Sym.Simp.Discharger
 public import Lean.Meta.Sym.Simp.ControlFlow
+public import Lean.Meta.Sym.Simp.Goal

src/Lean/Meta/Sym/Simp/Debug.lean

@@ -9,6 +9,7 @@ public import Lean.Meta.Sym.Simp.SimpM
 public import Lean.Meta.Sym.Simp.Discharger
 import Lean.Meta.Sym.Simp.Theorems
 import Lean.Meta.Sym.Simp.Rewrite
+import Lean.Meta.Sym.Simp.Goal
 import Lean.Meta.Sym.Util
 import Lean.Meta.Tactic.Util
 import Lean.Meta.AppBuilder
@@ -27,24 +28,9 @@ public def mkSimprocFor (declNames : Array Name) (d : Discharger := dischargeNon
 public def mkMethods (declNames : Array Name) : MetaM Methods := do
   return { post := (← mkSimprocFor declNames) }
 
-public def simpWith (k : Expr → SymM Result) (mvarId : MVarId) : MetaM (Option MVarId) := SymM.run do
-  let mvarId ← preprocessMVar mvarId
-  let decl ← mvarId.getDecl
-  let target := decl.type
-  match (← k target) with
-  | .rfl _ => throwError "`Sym.simp` made no progress "
-  | .step target' h _ =>
-    let mvarNew ← mkFreshExprSyntheticOpaqueMVar target' decl.userName
-    let h ← mkAppM ``Eq.mpr #[h, mvarNew]
-    mvarId.assign h
-    if target'.isTrue then
-      mvarNew.mvarId!.assign (mkConst ``True.intro)
-      return none
-    else
-      return some mvarNew.mvarId!
-
-public def simpGoal (declNames : Array Name) (mvarId : MVarId) : MetaM (Option MVarId) := SymM.run do mvarId.withContext do
+public def simpGoalUsing (declNames : Array Name) (mvarId : MVarId) : MetaM (Option MVarId) := SymM.run do
   let methods ← mkMethods declNames
-  simpWith (simp · methods) mvarId
+  let mvarId ← preprocessMVar mvarId
+  (← simpGoal mvarId methods).toOption
 
 end Lean.Meta.Sym

src/Lean/Meta/Sym/Simp/EvalGround.lean

@@ -9,6 +9,7 @@ public import Lean.Meta.Sym.Simp.SimpM
 import Init.Sym.Lemmas
 import Init.Data.Int.Gcd
 import Lean.Meta.Sym.LitValues
+import Lean.Meta.Sym.AlphaShareBuilder
 namespace Lean.Meta.Sym.Simp
 
 /-!
@@ -392,6 +393,8 @@ def evalLT (α : Expr) (a b : Expr) : SimpM Result :=
   | UInt64 => evalBinPred getUInt64Value? (mkConst ``UInt64.lt_eq_true) (mkConst ``UInt64.lt_eq_false) (. < .) a b
   | Fin n => evalFinPred n (mkConst ``Fin.lt_eq_true) (mkConst ``Fin.lt_eq_false) (. < .) a b
   | BitVec n => evalBitVecPred n (mkConst ``BitVec.lt_eq_true) (mkConst ``BitVec.lt_eq_false) (. < .) a b
+  | String => evalBinPred getStringValue? (mkConst ``String.lt_eq_true) (mkConst ``String.lt_eq_false) (. < .) a b
+  | Char => evalBinPred getCharValue? (mkConst ``Char.lt_eq_true) (mkConst ``Char.lt_eq_false) (. < .) a b
   | _ => return .rfl
 
 def evalLE (α : Expr) (a b : Expr) : SimpM Result :=
@@ -409,40 +412,8 @@ def evalLE (α : Expr) (a b : Expr) : SimpM Result :=
   | UInt64 => evalBinPred getUInt64Value? (mkConst ``UInt64.le_eq_true) (mkConst ``UInt64.le_eq_false) (. ≤ .) a b
   | Fin n => evalFinPred n (mkConst ``Fin.le_eq_true) (mkConst ``Fin.le_eq_false) (. ≤ .) a b
   | BitVec n => evalBitVecPred n (mkConst ``BitVec.le_eq_true) (mkConst ``BitVec.le_eq_false) (. ≤ .) a b
-  | _ => return .rfl
-
-def evalGT (α : Expr) (a b : Expr) : SimpM Result :=
-  match_expr α with
-  | Nat => evalBinPred getNatValue? (mkConst ``Nat.gt_eq_true) (mkConst ``Nat.gt_eq_false) (. > .) a b
-  | Int => evalBinPred getIntValue? (mkConst ``Int.gt_eq_true) (mkConst ``Int.gt_eq_false) (. > .) a b
-  | Rat => evalBinPred getRatValue? (mkConst ``Rat.gt_eq_true) (mkConst ``Rat.gt_eq_false) (. > .) a b
-  | Int8 => evalBinPred getInt8Value? (mkConst ``Int8.gt_eq_true) (mkConst ``Int8.gt_eq_false) (. > .) a b
-  | Int16 => evalBinPred getInt16Value? (mkConst ``Int16.gt_eq_true) (mkConst ``Int16.gt_eq_false) (. > .) a b
-  | Int32 => evalBinPred getInt32Value? (mkConst ``Int32.gt_eq_true) (mkConst ``Int32.gt_eq_false) (. > .) a b
-  | Int64 => evalBinPred getInt64Value? (mkConst ``Int64.gt_eq_true) (mkConst ``Int64.gt_eq_false) (. > .) a b
-  | UInt8 => evalBinPred getUInt8Value? (mkConst ``UInt8.gt_eq_true) (mkConst ``UInt8.gt_eq_false) (. > .) a b
-  | UInt16 => evalBinPred getUInt16Value? (mkConst ``UInt16.gt_eq_true) (mkConst ``UInt16.gt_eq_false) (. > .) a b
-  | UInt32 => evalBinPred getUInt32Value? (mkConst ``UInt32.gt_eq_true) (mkConst ``UInt32.gt_eq_false) (. > .) a b
-  | UInt64 => evalBinPred getUInt64Value? (mkConst ``UInt64.gt_eq_true) (mkConst ``UInt64.gt_eq_false) (. > .) a b
-  | Fin n => evalFinPred n (mkConst ``Fin.gt_eq_true) (mkConst ``Fin.gt_eq_false) (. > .) a b
-  | BitVec n => evalBitVecPred n (mkConst ``BitVec.gt_eq_true) (mkConst ``BitVec.gt_eq_false) (. > .) a b
-  | _ => return .rfl
-
-def evalGE (α : Expr) (a b : Expr) : SimpM Result :=
-  match_expr α with
-  | Nat => evalBinPred getNatValue? (mkConst ``Nat.ge_eq_true) (mkConst ``Nat.ge_eq_false) (. ≥ .) a b
-  | Int => evalBinPred getIntValue? (mkConst ``Int.ge_eq_true) (mkConst ``Int.ge_eq_false) (. ≥ .) a b
-  | Rat => evalBinPred getRatValue? (mkConst ``Rat.ge_eq_true) (mkConst ``Rat.ge_eq_false) (. ≥ .) a b
-  | Int8 => evalBinPred getInt8Value? (mkConst ``Int8.ge_eq_true) (mkConst ``Int8.ge_eq_false) (. ≥ .) a b
-  | Int16 => evalBinPred getInt16Value? (mkConst ``Int16.ge_eq_true) (mkConst ``Int16.ge_eq_false) (. ≥ .) a b
-  | Int32 => evalBinPred getInt32Value? (mkConst ``Int32.ge_eq_true) (mkConst ``Int32.ge_eq_false) (. ≥ .) a b
-  | Int64 => evalBinPred getInt64Value? (mkConst ``Int64.ge_eq_true) (mkConst ``Int64.ge_eq_false) (. ≥ .) a b
-  | UInt8 => evalBinPred getUInt8Value? (mkConst ``UInt8.ge_eq_true) (mkConst ``UInt8.ge_eq_false) (. ≥ .) a b
-  | UInt16 => evalBinPred getUInt16Value? (mkConst ``UInt16.ge_eq_true) (mkConst ``UInt16.ge_eq_false) (. ≥ .) a b
-  | UInt32 => evalBinPred getUInt32Value? (mkConst ``UInt32.ge_eq_true) (mkConst ``UInt32.ge_eq_false) (. ≥ .) a b
-  | UInt64 => evalBinPred getUInt64Value? (mkConst ``UInt64.ge_eq_true) (mkConst ``UInt64.ge_eq_false) (. ≥ .) a b
-  | Fin n => evalFinPred n (mkConst ``Fin.ge_eq_true) (mkConst ``Fin.ge_eq_false) (. ≥ .) a b
-  | BitVec n => evalBitVecPred n (mkConst ``BitVec.ge_eq_true) (mkConst ``BitVec.ge_eq_false) (. ≥ .) a b
+  | String => evalBinPred getStringValue? (mkConst ``String.le_eq_true) (mkConst ``String.le_eq_false) (. ≤ .) a b
+  | Char => evalBinPred getCharValue? (mkConst ``Char.le_eq_true) (mkConst ``Char.le_eq_false) (. ≤ .) a b
   | _ => return .rfl
 
 def evalEq (α : Expr) (a b : Expr) : SimpM Result :=
@@ -464,27 +435,8 @@ def evalEq (α : Expr) (a b : Expr) : SimpM Result :=
   | UInt64 => evalBinPred getUInt64Value? (mkConst ``UInt64.eq_eq_true) (mkConst ``UInt64.eq_eq_false) (. = .) a b
   | Fin n => evalFinPred n (mkConst ``Fin.eq_eq_true) (mkConst ``Fin.eq_eq_false) (. = .) a b
   | BitVec n => evalBitVecPred n (mkConst ``BitVec.eq_eq_true) (mkConst ``BitVec.eq_eq_false) (. = .) a b
-  | _ => return .rfl
-
-def evalNe (α : Expr) (a b : Expr) : SimpM Result :=
-  if isSameExpr a b then do
-    let e ← share <| mkConst ``False
-    let u ← getLevel α
-    return .step e (mkApp2 (mkConst ``ne_self [u]) α a) (done := true)
-  else match_expr α with
-  | Nat => evalBinPred getNatValue? (mkConst ``Nat.ne_eq_true) (mkConst ``Nat.ne_eq_false) (. ≠ .) a b
-  | Int => evalBinPred getIntValue? (mkConst ``Int.ne_eq_true) (mkConst ``Int.ne_eq_false) (. ≠ .) a b
-  | Rat => evalBinPred getRatValue? (mkConst ``Rat.ne_eq_true) (mkConst ``Rat.ne_eq_false) (. ≠ .) a b
-  | Int8 => evalBinPred getInt8Value? (mkConst ``Int8.ne_eq_true) (mkConst ``Int8.ne_eq_false) (. ≠ .) a b
-  | Int16 => evalBinPred getInt16Value? (mkConst ``Int16.ne_eq_true) (mkConst ``Int16.ne_eq_false) (. ≠ .) a b
-  | Int32 => evalBinPred getInt32Value? (mkConst ``Int32.ne_eq_true) (mkConst ``Int32.ne_eq_false) (. ≠ .) a b
-  | Int64 => evalBinPred getInt64Value? (mkConst ``Int64.ne_eq_true) (mkConst ``Int64.ne_eq_false) (. ≠ .) a b
-  | UInt8 => evalBinPred getUInt8Value? (mkConst ``UInt8.ne_eq_true) (mkConst ``UInt8.ne_eq_false) (. ≠ .) a b
-  | UInt16 => evalBinPred getUInt16Value? (mkConst ``UInt16.ne_eq_true) (mkConst ``UInt16.ne_eq_false) (. ≠ .) a b
-  | UInt32 => evalBinPred getUInt32Value? (mkConst ``UInt32.ne_eq_true) (mkConst ``UInt32.ne_eq_false) (. ≠ .) a b
-  | UInt64 => evalBinPred getUInt64Value? (mkConst ``UInt64.ne_eq_true) (mkConst ``UInt64.ne_eq_false) (. ≠ .) a b
-  | Fin n => evalFinPred n (mkConst ``Fin.ne_eq_true) (mkConst ``Fin.ne_eq_false) (. ≠ .) a b
-  | BitVec n => evalBitVecPred n (mkConst ``BitVec.ne_eq_true) (mkConst ``BitVec.ne_eq_false) (. ≠ .) a b
+  | Char => evalBinPred getCharValue? (mkConst ``Char.eq_eq_true) (mkConst ``Char.eq_eq_false) (. = .) a b
+  | String => evalBinPred getStringValue? (mkConst ``String.eq_eq_true) (mkConst ``String.eq_eq_false) (. = .) a b
   | _ => return .rfl
 
 def evalDvd (α : Expr) (a b : Expr) : SimpM Result :=
@@ -554,6 +506,16 @@ macro "declare_eval_bin_bool_pred" id:ident op:term : command =>
 declare_eval_bin_bool_pred evalBEq (· == ·)
 declare_eval_bin_bool_pred evalBNe (· != ·)
 
+open Internal in
+def evalNot (a : Expr) : SimpM Result :=
+  /-
+  **Note**: We added `evalNot` because some abbreviations expanded into `Not`s.
+  -/
+  match_expr a with
+  | True => return .step (← mkConstS ``False) (mkConst ``Sym.not_true_eq) (done := true)
+  | False => return .step (← mkConstS ``True) (mkConst ``Sym.not_false_eq) (done := true)
+  | _ => return .rfl
+
 public structure EvalStepConfig where
   maxExponent := 255
 
@@ -594,14 +556,12 @@ public def evalGround (config : EvalStepConfig := {}) : Simproc := fun e =>
   | Int.fmod a b => evalBinInt Int.fmod a b
   | Int.bmod a b => evalIntBMod a b
   | LE.le α _ a b => evalLE α a b
-  | GE.ge α _ a b => evalGE α a b
   | LT.lt α _ a b => evalLT α a b
-  | GT.gt α _ a b => evalGT α a b
   | Dvd.dvd α _ a b => evalDvd α a b
   | Eq α a b => evalEq α a b
-  | Ne α a b => evalNe α a b
   | BEq.beq α _ a b => evalBEq α a b
   | bne α _ a b => evalBNe α a b
+  | Not a => evalNot a
   | _  => return .rfl
 
 end Lean.Meta.Sym.Simp

src/Lean/Meta/Sym/Simp/Forall.lean

@@ -81,7 +81,7 @@ public def simpForall (e : Expr) : SimpM Result := do
   else if (← isProp e) then
     let n := getForallTelescopeSize e.bindingBody! 1
     forallBoundedTelescope e n fun xs b => withoutModifyingCacheIfNotWellBehaved do
-      main xs b
+      main xs (← shareCommon b)
   else
     return .rfl
 where
@@ -90,7 +90,7 @@ where
     | .rfl _ => return .rfl
     | .step b' h _ =>
       let h ← mkLambdaFVars xs h
-      let e' ← shareCommonInc (← mkForallFVars xs b')
+      let e' ← shareCommon (← mkForallFVars xs b')
       -- **Note**: consider caching the forall-congr theorems
       let hcongr ← mkForallCongrFor xs
       return .step e' (mkApp3 hcongr (← mkLambdaFVars xs b) (← mkLambdaFVars xs b') h)

src/Lean/Meta/Sym/Simp/Goal.lean

@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Sym.Simp.SimpM
+import Lean.Meta.Tactic.Util
+import Lean.Meta.AppBuilder
+import Lean.Meta.Sym.InferType
+namespace Lean.Meta.Sym
+/-!
+# Goal simplification
+
+Applies `Sym.simp` to a goal's target type, producing a simplified goal or closing it if
+the result is `True`.
+-/
+
+/-- Result of simplifying a goal with `Sym.simp`. -/
+public inductive SimpGoalResult where
+  /-- No simplification was possible. -/
+  | noProgress
+  /-- The goal was closed (simplified to `True`). -/
+  | closed
+  /-- The goal was simplified to a new goal. -/
+  | goal (mvarId : MVarId)
+
+/--
+Converts a `SimpGoalResult` to an optional goal.
+Returns `none` if closed, `some mvarId` if simplified, or throws an error if no progress.
+-/
+public def SimpGoalResult.toOption : SimpGoalResult → CoreM (Option MVarId)
+  | .noProgress => throwError "`Sym.simp` made no progress "
+  | .closed => return none
+  | .goal mvarId => return some mvarId
+
+public def SimpGoalResult.ignoreNoProgress : SimpGoalResult → MVarId → SimpGoalResult
+  | .noProgress, mvarId => .goal mvarId
+  | r, _ => r
+
+/--
+Converts a `Simp.Result` value into `SimpGoalResult`.
+-/
+public def Simp.Result.toSimpGoalResult (result : Simp.Result) (mvarId : MVarId) : SymM SimpGoalResult := do
+  let decl ← mvarId.getDecl
+  match result with
+  | .rfl _ => return .noProgress
+  | .step target' h _ =>
+    let mvarNew ← mkFreshExprSyntheticOpaqueMVar target' decl.userName
+    let u ← getLevel decl.type
+    let h := mkApp4 (mkConst ``Eq.mpr [u]) decl.type target' h mvarNew
+    mvarId.assign h
+    if target'.isTrue then
+      mvarNew.mvarId!.assign (mkConst ``True.intro)
+      return .closed
+    else
+      return .goal mvarNew.mvarId!
+
+/--
+Simplifies the target of `mvarId` using `Sym.simp`.
+Returns `.closed` if the target simplifies to `True`, `.simp mvarId'` if simplified
+to a new goal, or `.noProgress` if no simplification occurred.
+
+This function assumed the input goal is a valid `Sym` goal (e.g., expressions are maximally shared).
+-/
+public def simpGoal (mvarId : MVarId) (methods :  Simp.Methods := {}) (config : Simp.Config := {})
+    : SymM SimpGoalResult := mvarId.withContext do
+  let decl ← mvarId.getDecl
+  (← simp decl.type methods config).toSimpGoalResult mvarId
+
+/--
+Similar to `simpGoal`, but returns `.goal mvarId` if no progress was made.
+-/
+public def trySimpGoal (mvarId : MVarId) (methods :  Simp.Methods := {}) (config : Simp.Config := {})
+    : SymM SimpGoalResult := do
+  match (← simpGoal mvarId methods config) with
+  | .noProgress => return .goal mvarId
+  | r => return r
+
+end Lean.Meta.Sym

src/Lean/Meta/Sym/Simp/Lambda.lean

@@ -48,14 +48,14 @@ def mkFunextFor (xs : Array Expr) (β : Expr) : MetaM Expr := do
 
 public def simpLambda (e : Expr) : SimpM Result := do
   lambdaTelescope e fun xs b => withoutModifyingCacheIfNotWellBehaved do
-    main xs b
+    main xs (← shareCommon b)
 where
   main (xs : Array Expr) (b : Expr) : SimpM Result := do
     match (← simp b) with
     | .rfl _ => return .rfl
     | .step b' h _ =>
       let h ← mkLambdaFVars xs h
-      let e' ← shareCommonInc (← mkLambdaFVars xs b')
+      let e' ← shareCommon (← mkLambdaFVars xs b')
       let funext ← getFunext xs b
       return .step e' (mkApp3 funext e e' h)
 

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

@@ -11,6 +11,7 @@ public import Lean.Meta.Sym.Simp.Theorems
 public import Lean.Meta.Sym.Simp.App
 public import Lean.Meta.Sym.Simp.Discharger
 import Lean.Meta.Sym.InstantiateS
+import Lean.Meta.Sym.InstantiateMVarsS
 import Lean.Meta.Sym.Simp.DiscrTree
 namespace Lean.Meta.Sym.Simp
 open Grind
@@ -20,31 +21,48 @@ Creates proof term for a rewriting step.
 Handles both constant expressions (common case, avoids `instantiateLevelParams`)
 and general expressions.
 -/
-def mkValue (expr : Expr) (pattern : Pattern) (result : MatchUnifyResult) : Expr :=
+def mkValue (expr : Expr) (pattern : Pattern) (us : List Level) (args : Array Expr) : Expr :=
   if let .const declName [] := expr then
-    mkAppN (mkConst declName result.us) result.args
+    mkAppN (mkConst declName us) args
   else
-    mkAppN (expr.instantiateLevelParams pattern.levelParams result.us) result.args
+    mkAppN (expr.instantiateLevelParams pattern.levelParams us) args
 
 /--
 Tries to rewrite `e` using the given theorem.
 -/
-public def Theorem.rewrite (thm : Theorem) (e : Expr) (d : Discharger := dischargeNone) : SimpM Result := do
+public def Theorem.rewrite (thm : Theorem) (e : Expr) (d : Discharger := dischargeNone) : SimpM Result :=
+  /-
+  **Note**: We use `withNewMCtxDepth` to ensure auxiliary metavariables used during the `match?`
+  do not pollute the metavariable context.
+  Thus, we must ensure that all assigned variables have be instantiate.
+  -/
+  withNewMCtxDepth do
   if let some result ← thm.pattern.match? e then
     -- **Note**: Potential optimization: check whether pattern covers all variables.
-    for arg in result.args do
-      let .mvar mvarId := arg | pure ()
-      unless (← mvarId.isAssigned) do
-        let decl ← mvarId.getDecl
-        if let some val ← d decl.type then
-          mvarId.assign val
+    let mut args := result.args.toVector
+    let us ← result.us.mapM instantiateLevelMVars
+    for h : i in *...args.size do
+      let arg := args[i]
+      if let .mvar mvarId := arg then
+        if (← mvarId.isAssigned) then
+          let arg ← instantiateMVarsS arg
+          args := args.set i arg
         else
-          -- **Note**: Failed to discharge hypothesis.
-          return .rfl
-    let proof := mkValue thm.expr thm.pattern result
-    let rhs   := thm.rhs.instantiateLevelParams thm.pattern.levelParams result.us
-    let rhs   ← shareCommonInc rhs
-    let expr  ← instantiateRevBetaS rhs result.args
+          let decl ← mvarId.getDecl
+          if let some val ← d decl.type then
+            let val ← instantiateMVarsS val
+            mvarId.assign val
+            args := args.set i val
+          else
+            -- **Note**: Failed to discharge hypothesis.
+            return .rfl
+      else if arg.hasMVar then
+        let arg ← instantiateMVarsS arg
+        args := args.set i arg
+    let proof := mkValue thm.expr thm.pattern us args.toArray
+    let rhs   := thm.rhs.instantiateLevelParams thm.pattern.levelParams us
+    let rhs   ← share rhs
+    let expr  ← instantiateRevBetaS rhs args.toArray
     if isSameExpr e expr then
       return .rfl
     else

src/Lean/Meta/Sym/Simp/SimpM.lean

@@ -101,7 +101,7 @@ invalidating the cache and causing O(2^n) behavior on conditional trees.
 /-- Configuration options for the structural simplifier. -/
 structure Config where
   /-- Maximum number of steps that can be performed by the simplifier. -/
-  maxSteps : Nat := 1000
+  maxSteps : Nat := 100_000
   /--
   Maximum depth of reentrant simplifier calls through dischargers.
   Prevents infinite loops when conditional rewrite rules trigger recursive discharge attempts.
@@ -173,16 +173,13 @@ abbrev Cache := PHashMap ExprPtr Result
 
 /-- Mutable state for the simplifier. -/
 structure State where
+  /-- Number of steps performed so far. -/
+  numSteps := 0
   /--
   Cache of previously simplified expressions to avoid redundant work.
   **Note**: Consider moving to `SymM.State`
   -/
   cache : Cache := {}
-  /-- Stack of free variables available for reuse when re-entering binders.
-  Each entry is (type pointer, fvarId). -/
-  binderStack : List (ExprPtr × FVarId) := []
-  /-- Number of steps performed so far. -/
-  numSteps := 0
   /-- Cache for generated funext theorems -/
   funext : PHashMap ExprPtr Expr := {}
 
@@ -221,8 +218,13 @@ opaque MethodsRef.toMethods (m : MethodsRef) : Methods
 def getMethods : SimpM Methods :=
   return MethodsRef.toMethods (← read)
 
+/-- Runs a `SimpM` computation with the given theorems, configuration, and initial state -/
+def SimpM.run (x : SimpM α) (methods : Methods := {}) (config : Config := {}) (s : State := {}) : SymM (α × State) := do
+  let initialLCtxSize := (← getLCtx).decls.size
+  x methods.toMethodsRef { initialLCtxSize, config } |>.run s
+
 /-- Runs a `SimpM` computation with the given theorems and configuration. -/
-def SimpM.run (x : SimpM α) (methods : Methods := {}) (config : Config := {}) : SymM α := do
+def SimpM.run' (x : SimpM α) (methods : Methods := {}) (config : Config := {}) : SymM α := do
   let initialLCtxSize := (← getLCtx).decls.size
   x methods.toMethodsRef { initialLCtxSize, config } |>.run' {}
 
@@ -243,7 +245,8 @@ abbrev post : Simproc := fun e => do
 
 abbrev withoutModifyingCache (k : SimpM α) : SimpM α := do
   let cache ← getCache
-  try k finally modify fun s => { s with cache }
+  let funext := (← get).funext
+  try k finally modify fun s => { s with cache, funext }
 
 abbrev withoutModifyingCacheIfNotWellBehaved (k : SimpM α) : SimpM α := do
   if (← getMethods).wellBehavedMethods then k else withoutModifyingCache k
@@ -251,6 +254,6 @@ abbrev withoutModifyingCacheIfNotWellBehaved (k : SimpM α) : SimpM α := do
 end Simp
 
 abbrev simp (e : Expr) (methods :  Simp.Methods := {}) (config : Simp.Config := {}) : SymM Simp.Result := do
-  Simp.SimpM.run (Simp.simp e) methods config
+  Simp.SimpM.run' (Simp.simp e) methods config
 
 end Lean.Meta.Sym

src/Lean/Meta/Sym/Util.lean

@@ -6,13 +6,56 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Sym.SymM
+public import Lean.Meta.Transform
+import Init.Grind.Util
+import Lean.Meta.WHNF
+import Lean.Util.ForEachExpr
 namespace Lean.Meta.Sym
-open Grind
+
+/--
+Returns `true` if `declName` is the name of a grind helper declaration that
+should not be unfolded by `unfoldReducible`.
+-/
+def isGrindGadget (declName : Name) : Bool :=
+  declName == ``Grind.EqMatch
+
+/--
+Auxiliary function for implementing `unfoldReducible` and `unfoldReducibleSimproc`.
+Performs a single step.
+-/
+public def unfoldReducibleStep (e : Expr) : MetaM TransformStep := do
+  let .const declName _ := e.getAppFn | return .continue
+  unless (← isReducible declName) do return .continue
+  if isGrindGadget declName then return .continue
+  -- See comment at isUnfoldReducibleTarget.
+  if (← getEnv).isProjectionFn declName then return .continue
+  let some v ← unfoldDefinition? e | return .continue
+  return .visit v
+
+def isUnfoldReducibleTarget (e : Expr) : CoreM Bool := do
+  let env ← getEnv
+  return Option.isSome <| e.find? fun e => Id.run do
+    let .const declName _ := e | return false
+    if getReducibilityStatusCore env declName matches .reducible then
+      -- Remark: it is wasteful to unfold projection functions since
+      -- kernel projections are folded again in the `foldProjs` preprocessing step.
+      return !isGrindGadget declName && !env.isProjectionFn declName
+    else
+      return false
+
+/--
+Unfolds all `reducible` declarations occurring in `e`.
+This is meant as a preprocessing step. It does **not** guarantee maximally shared terms
+-/
+public def unfoldReducible (e : Expr) : MetaM Expr := do
+  if !(← isUnfoldReducibleTarget e) then return e
+  Meta.transform e (pre := unfoldReducibleStep)
+
 /--
 Instantiates metavariables, unfold reducible, and applies `shareCommon`.
 -/
 def preprocessExpr (e : Expr) : SymM Expr := do
-  shareCommon (← instantiateMVars e)
+  shareCommon (← unfoldReducible (← instantiateMVars e))
 
 /--
 Helper function that removes gaps, instantiate metavariables, and applies `shareCommon`.
@@ -32,6 +75,7 @@ def preprocessLCtx (lctx : LocalContext) : SymM LocalContext := do
         let type ← preprocessExpr type
         let value ← preprocessExpr value
         pure <| LocalDecl.ldecl index fvarId userName type value nondep kind
+    index := index + 1
     decls := decls.push (some decl)
     fvarIdToDecl := fvarIdToDecl.insert decl.fvarId decl
   return { fvarIdToDecl, decls, auxDeclToFullName }
@@ -48,4 +92,21 @@ public def preprocessMVar (mvarId : MVarId) : SymM MVarId := do
   mvarId.assign mvarNew
   return mvarNew.mvarId!
 
+/-- Debug helper: throws if any subexpression of `e` is not in the table of maximally shared terms. -/
+public def _root_.Lean.Expr.checkMaxShared (e : Expr) (msg := "") : SymM Unit := do
+  e.forEach fun e => do
+    if let some prev := (← get).share.set.find? { expr := e } then
+      unless isSameExpr prev.expr e do
+        throwNotMaxShared e
+    else
+      throwNotMaxShared e
+where
+  throwNotMaxShared (e : Expr) : SymM Unit := do
+    let msg := if msg == "" then msg else s!"[{msg}] "
+    throwError "{msg}term is not in the maximally shared table{indentExpr e}"
+
+/-- Debug helper: throws if any subexpression of the goal's target type is not in the table of maximally shared. -/
+public def _root_.Lean.MVarId.checkMaxShared (mvarId : MVarId) (msg := "") : SymM Unit := do
+  (← mvarId.getDecl).type.checkMaxShared msg
+
 end Lean.Meta.Sym

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

@@ -11,6 +11,7 @@ import Lean.Util.ForEachExpr
 import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Match.Basic
 import Lean.Meta.Tactic.TryThis
+import Lean.Meta.Sym.Util
 public section
 namespace Lean.Meta.Grind
 /-!
@@ -281,7 +282,7 @@ private theorem normConfig_zetaDelta : normConfig.zetaDelta = true := rfl
 
 def preprocessPattern (pat : Expr) (normalizePattern := true) : MetaM Expr := do
   let pat ← instantiateMVars pat
-  let pat ← unfoldReducible pat
+  let pat ← Sym.unfoldReducible pat
   let pat ← if normalizePattern then normalize pat normConfig else pure pat
   let pat ← detectOffsets pat
   let pat ← foldProjs pat

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

@@ -8,6 +8,7 @@ prelude
 public import Lean.Meta.Tactic.Grind.Types
 import Init.Grind.Util
 import Lean.Meta.Sym.ExprPtr
+import Lean.Meta.Sym.Util
 import Lean.Meta.Tactic.Grind.Util
 public section
 namespace Lean.Meta.Grind
@@ -103,7 +104,7 @@ where
     -/
     /- We must also apply beta-reduction to improve the effectiveness of the congruence closure procedure. -/
     let e ← Core.betaReduce e
-    let e ← unfoldReducible e
+    let e ← Sym.unfoldReducible e
     /- We must mask proofs occurring in `prop` too. -/
     let e ← visit e
     let e ← eraseIrrelevantMData e

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

@@ -11,6 +11,7 @@ public import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.MatchDiscrOnly
 import Lean.Meta.Tactic.Grind.MarkNestedSubsingletons
+import Lean.Meta.Sym.Util
 public section
 namespace Lean.Meta.Grind
 
@@ -57,7 +58,7 @@ def preprocessImpl (e : Expr) : GoalM Simp.Result := do
   let e' ← instantiateMVars r.expr
   -- Remark: `simpCore` unfolds reducible constants, but it does not consistently visit all possible subterms.
   -- So, we must use the following `unfoldReducible` step. It is non-op in most cases
-  let e' ← unfoldReducible e'
+  let e' ← Sym.unfoldReducible e'
   let e' ← abstractNestedProofs e'
   let e' ← markNestedSubsingletons e'
   let e' ← eraseIrrelevantMData e'
@@ -97,6 +98,6 @@ but ensures assumptions made by `grind` are satisfied.
 -/
 def preprocessLight (e : Expr) : GoalM Expr := do
   let e ← instantiateMVars e
-  shareCommon (← canon (← normalizeLevels (← foldProjs (← eraseIrrelevantMData (← markNestedSubsingletons (← unfoldReducible e))))))
+  shareCommon (← canon (← normalizeLevels (← foldProjs (← eraseIrrelevantMData (← markNestedSubsingletons (← Sym.unfoldReducible e))))))
 
 end Lean.Meta.Grind

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

@@ -14,6 +14,7 @@ import Lean.Meta.Tactic.Grind.Arith.Simproc
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.List
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core
 import Lean.Meta.Tactic.Grind.Util
+import Lean.Meta.Sym.Util
 import Init.Grind.Norm
 public section
 namespace Lean.Meta.Grind
@@ -136,7 +137,7 @@ builtin_simproc_decl reduceCtorEqCheap (_ = _) := fun e => do
     return .done { expr := mkConst ``False, proof? := (← withDefault <| mkEqFalse' (← mkLambdaFVars #[h] (← mkNoConfusion (mkConst ``False) h))) }
 
 builtin_dsimproc_decl unfoldReducibleSimproc (_) := fun e => do
-  unfoldReducibleStep e
+  Sym.unfoldReducibleStep e
 
 /-- Returns the array of simprocs used by `grind`. -/
 protected def getSimprocs : MetaM (Array Simprocs) := do

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

@@ -11,6 +11,7 @@ import Lean.ProjFns
 import Lean.Meta.WHNF
 import Lean.Meta.AbstractNestedProofs
 import Lean.Meta.Tactic.Clear
+import Lean.Meta.Sym.Util
 public section
 namespace Lean.Meta.Grind
 /--
@@ -55,49 +56,11 @@ def _root_.Lean.MVarId.transformTarget (mvarId : MVarId) (f : Expr → MetaM Exp
   mvarId.assign mvarNew
   return mvarNew.mvarId!
 
-/--
-Returns `true` if `declName` is the name of a grind helper declaration that
-should not be unfolded by `unfoldReducible`.
--/
-def isGrindGadget (declName : Name) : Bool :=
-  declName == ``Grind.EqMatch
-
-def isUnfoldReducibleTarget (e : Expr) : CoreM Bool := do
-  let env ← getEnv
-  return Option.isSome <| e.find? fun e => Id.run do
-    let .const declName _ := e | return false
-    if getReducibilityStatusCore env declName matches .reducible then
-      -- Remark: it is wasteful to unfold projection functions since
-      -- kernel projections are folded again in the `foldProjs` preprocessing step.
-      return !isGrindGadget declName && !env.isProjectionFn declName
-    else
-      return false
-
-/--
-Auxiliary function for implementing `unfoldReducible` and `unfoldReducibleSimproc`.
-Performs a single step.
--/
-def unfoldReducibleStep (e : Expr) : MetaM TransformStep := do
-  let .const declName _ := e.getAppFn | return .continue
-  unless (← isReducible declName) do return .continue
-  if isGrindGadget declName then return .continue
-  -- See comment at isUnfoldReducibleTarget.
-  if (← getEnv).isProjectionFn declName then return .continue
-  let some v ← unfoldDefinition? e | return .continue
-  return .visit v
-
-/--
-Unfolds all `reducible` declarations occurring in `e`.
--/
-def unfoldReducible (e : Expr) : MetaM Expr := do
-  if !(← isUnfoldReducibleTarget e) then return e
-  Meta.transform e (pre := unfoldReducibleStep)
-
 /--
 Unfolds all `reducible` declarations occurring in the goal's target.
 -/
 def _root_.Lean.MVarId.unfoldReducible (mvarId : MVarId) : MetaM MVarId :=
-  mvarId.transformTarget Grind.unfoldReducible
+  mvarId.transformTarget Sym.unfoldReducible
 
 /--
 Beta-reduces the goal's target.

src/Lean/Parser/Attr.lean

@@ -54,7 +54,7 @@ def externEntry := leading_parser
   nonReservedSymbol "extern" >> many (ppSpace >> externEntry)
 
 /--
-Declare this tactic to be an alias or alternative form of an existing tactic.
+Declares this tactic to be an alias or alternative form of an existing tactic.
 
 This has the following effects:
  * The alias relationship is saved
@@ -64,13 +64,26 @@ This has the following effects:
   "tactic_alt" >> ppSpace >> ident
 
 /--
-Add one or more tags to a tactic.
+Adds one or more tags to a tactic.
 
 Tags should be applied to the canonical names for tactics.
 -/
 @[builtin_attr_parser] def «tactic_tag» := leading_parser
   "tactic_tag" >> many1 (ppSpace >> ident)
 
+/--
+Sets the tactic's name.
+
+Ordinarily, tactic names are automatically set to the first token in the tactic's parser. If this
+process fails, or if the tactic's name should be multiple tokens (e.g. `let rec`), then this
+attribute can be used to provide a name.
+
+The tactic's name is used in documentation as well as in completion. Thus, the name should be a
+valid prefix of the tactic's syntax.
+-/
+@[builtin_attr_parser] def «tactic_name» := leading_parser
+  "tactic_name" >> ppSpace >> (ident <|> strLit)
+
 end Attr
 
 end Lean.Parser

src/Lean/Parser/Tactic.lean

@@ -52,24 +52,7 @@ example (n : Nat) : n = n := by
   optional Term.motive >> sepBy1 Term.matchDiscr ", " >>
   " with " >> ppDedent matchAlts
 
-/--
-The tactic
-```
-intro
-| pat1 => tac1
-| pat2 => tac2
-```
-is the same as:
-```
-intro x
-match x with
-| pat1 => tac1
-| pat2 => tac2
-```
-That is, `intro` can be followed by match arms and it introduces the values while
-doing a pattern match. This is equivalent to `fun` with match arms in term mode.
--/
-@[builtin_tactic_parser] def introMatch := leading_parser
+@[builtin_tactic_parser, tactic_alt intro] def introMatch := leading_parser
   nonReservedSymbol "intro" >> matchAlts
 
 builtin_initialize

src/Lean/Parser/Tactic/Doc.lean

@@ -191,12 +191,13 @@ builtin_initialize
       unless kind == AttributeKind.global do throwAttrMustBeGlobal name kind
       let `(«tactic_tag»|tactic_tag $tags*) := stx
         | throwError "Invalid `[{name}]` attribute syntax"
+
       if (← getEnv).find? decl |>.isSome then
         if !(isTactic (← getEnv) decl) then
-          throwErrorAt stx "`{decl}` is not a tactic"
+          throwErrorAt stx "`{.ofConstName decl}` is not a tactic"
 
       if let some tgt' := alternativeOfTactic (← getEnv) decl then
-        throwErrorAt stx "`{decl}` is an alternative form of `{tgt'}`"
+        throwErrorAt stx "`{.ofConstName decl}` is an alternative form of `{.ofConstName tgt'}`"
 
       for t in tags do
         let tagName := t.getId
@@ -271,14 +272,81 @@ where
     | [l] => " * " ++ l ++ "\n\n"
     | l::ls => " * " ++ l ++ "\n" ++ String.join (ls.map indentLine) ++ "\n\n"
 
+/--
+The mapping between tactics and their custom names.
+
+The first projection in each pair is the tactic name, and the second is the custom name.
+-/
+builtin_initialize tacticNameExt
+    : PersistentEnvExtension
+        (Name × String)
+        (Name × String)
+        (NameMap String) ←
+  registerPersistentEnvExtension {
+    mkInitial := pure {},
+    addImportedFn := fun _ => pure {},
+    addEntryFn := fun as (src, tgt) => as.insert src tgt,
+    exportEntriesFn := fun es =>
+      es.foldl (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
+  }
+
+/--
+Finds the custom name assigned to `tac`, or returns `none` if there is no such custom name.
+-/
+def customTacticName [Monad m] [MonadEnv m] (tac : Name) : m (Option String) := do
+  let env ← getEnv
+  match env.getModuleIdxFor? tac with
+  | some modIdx =>
+    match (tacticNameExt.getModuleEntries env modIdx).binSearch (tac, default) (Name.quickLt ·.1 ·.1) with
+    | some (_, val) => return some val
+    | none => return none
+  | none => return tacticNameExt.getState env |>.find? tac
+
+builtin_initialize
+  let name := `tactic_name
+  registerBuiltinAttribute {
+    name := name,
+    ref := by exact decl_name%,
+    add := fun decl stx kind => do
+      unless kind == AttributeKind.global do throwAttrMustBeGlobal name kind
+      let name ←
+        match stx with
+        | `(«tactic_name»|tactic_name $name:str) =>
+          pure name.getString
+        | `(«tactic_name»|tactic_name $name:ident) =>
+          pure (name.getId.toString (escape := false))
+        | _ => throwError "Invalid `[{name}]` attribute syntax"
+
+      if (← getEnv).find? decl |>.isSome then
+        if !(isTactic (← getEnv) decl) then
+          throwErrorAt stx m!"`{.ofConstName decl}` is not a tactic"
+        if let some idx := (← getEnv).getModuleIdxFor? decl then
+          if let some mod := (← getEnv).allImportedModuleNames[idx]? then
+            throwErrorAt stx m!"`{.ofConstName decl}` is defined in `{mod}`, but custom names can only be added in the tactic's defining module."
+          else
+            throwErrorAt stx m!"`{.ofConstName decl}` is defined in an imported module, but custom names can only be added in the tactic's defining module."
+
+      if let some tgt' := alternativeOfTactic (← getEnv) decl then
+        throwErrorAt stx "`{.ofConstName decl}` is an alternative form of `{.ofConstName tgt'}`"
+
+      if let some n ← customTacticName decl then
+        throwError m!"The tactic `{.ofConstName decl}` already has the custom name `{n}`"
+
+      modifyEnv fun env => tacticNameExt.addEntry env (decl, name)
+
+    descr :=
+      "Registers a custom name for a tactic. This custom name should be a prefix of the " ++
+      "tactic's syntax, because it is used in completion.",
+    applicationTime := .beforeElaboration
+  }
 
 -- Note: this error handler doesn't prevent all cases of non-tactics being added to the data
 -- structure. But the module will throw errors during elaboration, and there doesn't seem to be
 -- another way to implement this, because the category parser extension attribute runs *after* the
 -- attributes specified before a `syntax` command.
 /--
-Validates that a tactic alternative is actually a tactic and that syntax tagged as tactics are
-tactics.
+Validates that a tactic alternative is actually a tactic, that syntax tagged as tactics are
+tactics, and that syntax with tactic names are tactics.
 -/
 private def tacticDocsOnTactics : ParserAttributeHook where
   postAdd (catName declName : Name) (_builtIn : Bool) := do
@@ -291,6 +359,8 @@ private def tacticDocsOnTactics : ParserAttributeHook where
     if let some tags := tacticTagExt.getState (← getEnv) |>.find? declName then
       if !tags.isEmpty then
         throwError m!"`{.ofConstName declName}` is not a tactic"
+    if let some n := tacticNameExt.getState (← getEnv) |>.find? declName then
+      throwError m!"`{MessageData.ofConstName declName}` is not a tactic, but it was assigned a tactic name `{n}`"
 
 builtin_initialize
   registerParserAttributeHook tacticDocsOnTactics

src/Lean/Server/CodeActions/UnknownIdentifier.lean

@@ -224,17 +224,22 @@ def computeQueries
       break
   return queries
 
-def importAllUnknownIdentifiersProvider : Name := `unknownIdentifiers
+def importAllUnknownIdentifiersProvider : Name := `allUnknownIdentifiers
+def importUnknownIdentifiersProvider : Name := `unknownIdentifiers
+
+def mkUnknownIdentifierCodeActionData (params : CodeActionParams)
+    (name := importUnknownIdentifiersProvider) : CodeActionResolveData := {
+  params,
+  providerName := name
+  providerResultIndex := 0
+  : CodeActionResolveData
+}
 
 def importAllUnknownIdentifiersCodeAction (params : CodeActionParams) (kind : String) : CodeAction := {
   title := "Import all unambiguous unknown identifiers"
   kind? := kind
-  data? := some <| toJson {
-    params,
-    providerName := importAllUnknownIdentifiersProvider
-    providerResultIndex := 0
-    : CodeActionResolveData
-  }
+  data? := some <| toJson <|
+    mkUnknownIdentifierCodeActionData params importAllUnknownIdentifiersProvider
 }
 
 private def mkImportText (ctx : Elab.ContextInfo) (mod : Name) :
@@ -311,6 +316,7 @@ def handleUnknownIdentifierCodeAction
               insertion.edit
             ]
           }
+          data? := some <| toJson <| mkUnknownIdentifierCodeActionData params
         }
         if isExactMatch then
           hasUnambiguousImportCodeAction := true
@@ -322,6 +328,7 @@ def handleUnknownIdentifierCodeAction
             textDocument := doc.versionedIdentifier
             edits := #[insertion.edit]
           }
+          data? := some <| toJson <| mkUnknownIdentifierCodeActionData params
         }
   if hasUnambiguousImportCodeAction then
     unknownIdentifierCodeActions := unknownIdentifierCodeActions.push <|

src/Lean/Server/Completion/CompletionCollectors.lean

@@ -597,7 +597,8 @@ def tacticCompletion
     (completionInfoPos : Nat)
     (ctx               : ContextInfo)
     : IO (Array ResolvableCompletionItem) := ctx.runMetaM .empty do
-  let allTacticDocs ← Tactic.Doc.allTacticDocs
+  -- Don't include tactics that are identified only by their internal parser name
+  let allTacticDocs ← Tactic.Doc.allTacticDocs (includeUnnamed := false)
   let items : Array ResolvableCompletionItem := allTacticDocs.map fun tacticDoc => {
       label          := tacticDoc.userName
       detail?        := none

src/Lean/Server/FileWorker.lean

@@ -793,21 +793,24 @@ section MessageHandling
         rpcEncode resp st.objects |>.map (·) ({st with objects := ·})
       return some <| .pure { response? := resp, serialized := resp.compress, isComplete := true }
     | "codeAction/resolve" =>
+      let jsonParams := params
       let params ← RequestM.parseRequestParams CodeAction params
       let some data := params.data?
         | throw (RequestError.invalidParams "Expected a data field on CodeAction.")
       let data ← RequestM.parseRequestParams CodeActionResolveData data
-      if data.providerName != importAllUnknownIdentifiersProvider then
-        return none
-      return some <| ← RequestM.asTask do
-        let unknownIdentifierRanges ← waitAllUnknownIdentifierMessageRanges st.doc
-        if unknownIdentifierRanges.isEmpty then
-          let p := toJson params
-          return { response? := p, serialized := p.compress, isComplete := true }
-        let action? ← handleResolveImportAllUnknownIdentifiersCodeAction? id params unknownIdentifierRanges
-        let action := action?.getD params
-        let action := toJson action
-        return { response? := action, serialized := action.compress, isComplete := true }
+      if data.providerName == importUnknownIdentifiersProvider then
+        return some <| RequestTask.pure { response? := jsonParams, serialized := jsonParams.compress, isComplete := true }
+      if data.providerName == importAllUnknownIdentifiersProvider then
+        return some <| ← RequestM.asTask do
+          let unknownIdentifierRanges ← waitAllUnknownIdentifierMessageRanges st.doc
+          if unknownIdentifierRanges.isEmpty then
+            let p := toJson params
+            return { response? := p, serialized := p.compress, isComplete := true }
+          let action? ← handleResolveImportAllUnknownIdentifiersCodeAction? id params unknownIdentifierRanges
+          let action := action?.getD params
+          let action := toJson action
+          return { response? := action, serialized := action.compress, isComplete := true }
+      return none
     | _ =>
       return none
 

src/Std.lean

@@ -6,6 +6,7 @@ Authors: Sebastian Ullrich
 module
 
 prelude
+public import Std.Async
 public import Std.Data
 public import Std.Do
 public import Std.Sat

src/Std/Async.lean

@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+module
+
+prelude
+public import Std.Async.Basic
+public import Std.Async.ContextAsync
+public import Std.Async.Timer
+public import Std.Async.TCP
+public import Std.Async.UDP
+public import Std.Async.DNS
+public import Std.Async.Select
+public import Std.Async.Process
+public import Std.Async.System
+public import Std.Async.Signal
+public import Std.Async.IO

src/Std/Async/Basic.lean

@@ -10,10 +10,7 @@ public import Init.System.Promise
 
 public section
 
-namespace Std
-namespace Internal
-namespace IO
-namespace Async
+namespace Std.Async
 
 /-!
 
@@ -104,10 +101,6 @@ instance [Monad m] [MonadAwait t m] : MonadAwait t (ReaderT n m) where
 instance [MonadAwait t m] : MonadAwait t (StateRefT' s n m) where
   await := liftM (m := m) ∘ MonadAwait.await
 
-@[default_instance]
-instance [Monad m] [MonadAwait t m] : MonadAwait t (StateT s m) where
-  await := liftM (m := m) ∘ MonadAwait.await
-
 @[default_instance]
 instance [MonadAsync t m] : MonadAsync t (ReaderT n m) where
   async p prio := MonadAsync.async (prio := prio) ∘ p
@@ -122,6 +115,19 @@ instance [Monad m] [Functor t] [inst : MonadAsync t m] : MonadAsync t (StateT s
     let t ← inst.async (prio := prio) (p s)
     pure (t <&> Prod.fst, s)
 
+/--
+Type class for converting a source type into an async computation.
+
+This provides a uniform interface for lifting various types (tasks, promises, etc.)
+into async monads.
+-/
+class ToAsync (source : Type) (target : outParam Type) where
+  /--
+  Convert the source value into an async computation using the default error message.
+  -/
+
+  toAsync : source → target
+
 /--
 A `Task` that may resolve to either a value of type `α` or an error value of type `ε`.
 -/
@@ -177,14 +183,12 @@ protected def mapEIO (f : α → EIO ε β) (x : ETask ε α) (prio := Task.Prio
     | .error e => throw e
 
 /--
-Block until the `ETask` in `x` finishes and returns its value. Propagates any error encountered
+Wait until the `ETask` in `x` finishes and returns its value. Propagates any error encountered
 during execution.
 -/
 @[inline]
-def block (x : ETask ε α) : EIO ε α := do
-  match x.get with
-  | .ok a => return a
-  | .error e => throw e
+def block (x : ETask ε α) : EIO ε α :=
+  liftExcept x.get
 
 /--
 Create an `ETask` that resolves to the value of the promise `x`. If the promise gets dropped then it
@@ -200,7 +204,7 @@ panics.
 -/
 @[inline]
 def ofPurePromise (x : IO.Promise α) : ETask ε α :=
-  x.result!.map pure (sync := true)
+  x.result!.map .ok (sync := true)
 
 /--
 Obtain the `IO.TaskState` of `x`.
@@ -212,9 +216,8 @@ def getState (x : ETask ε α) : BaseIO IO.TaskState :=
 instance : Functor (ETask ε) where
   map := ETask.map
 
-instance : Monad (ETask ε) where
-  pure := ETask.pure
-  bind := ETask.bind
+instance : ToAsync (IO.Promise (Except ε α)) (ETask ε α) where
+  toAsync := ETask.ofPromise!
 
 end ETask
 
@@ -225,6 +228,13 @@ abbrev AsyncTask := ETask IO.Error
 
 namespace AsyncTask
 
+/--
+Waits for the result of the `AsyncTask`, blocking if necessary.
+-/
+@[inline]
+protected def block (self : AsyncTask α) : IO α :=
+  ETask.block self
+
 /--
 Similar to `map`, however `f` has access to the `IO` monad. If `f` throws an error, the returned
 `AsyncTask` resolves to that error.
@@ -235,87 +245,39 @@ protected def mapIO (f : α → IO β) (x : AsyncTask α) (prio := Task.Priority
     | .ok a => f a
     | .error e => throw e
 
-/--
-Construct an `AsyncTask` that is already resolved with value `x`.
--/
-@[inline]
-protected def pure (x : α) : AsyncTask α :=
-  Task.pure <| .ok x
-
-/--
-Create a new `AsyncTask` that will run after `x` has finished.
-If `x`:
-- errors, return an `AsyncTask` that resolves to the error.
-- succeeds, run `f` on the result of `x` and return the `AsyncTask` produced by `f`.
--/
-@[inline]
-protected def bind (x : AsyncTask α) (f : α → AsyncTask β) (prio := Task.Priority.default) (sync := false) : AsyncTask β :=
-  Task.bind x (prio := prio) (sync := sync) fun
-    | .ok a => f a
-    | .error e => Task.pure <| .error e
-
-/--
-Create a new `AsyncTask` that will run after `x` has finished.
-If `x`:
-- errors, return an `AsyncTask` that resolves to the error.
-- succeeds, return an `AsyncTask` that resolves to `f x`.
--/
-@[inline]
-def map (f : α → β) (x : AsyncTask α) (prio := Task.Priority.default) (sync := false) : AsyncTask β :=
-  Task.map (x := x) (f <$> ·) prio sync
-
 /--
 Similar to `bind`, however `f` has access to the `IO` monad. If `f` throws an error, the returned
 `AsyncTask` resolves to that error.
 -/
 @[inline]
-def bindIO (x : AsyncTask α) (f : α → IO (AsyncTask β)) (prio := Task.Priority.default) (sync := false) : BaseIO (AsyncTask β) :=
+protected def bindIO (x : AsyncTask α) (f : α → IO (AsyncTask β)) (prio := Task.Priority.default) (sync := false) : BaseIO (AsyncTask β) :=
   IO.bindTask x (prio := prio) (sync := sync) fun
     | .ok a => f a
     | .error e => throw e
 
 /--
-Similar to `map`, however `f` has access to the `IO` monad. If `f` throws an error, the returned
-`AsyncTask` resolves to that error.
+Create an `AsyncTask` that resolves to the value of `x`. Returns an error if the promise is dropped.
 -/
 @[inline]
-def mapTaskIO (f : α → IO β) (x : AsyncTask α) (prio := Task.Priority.default) (sync := false) : BaseIO (AsyncTask β) :=
-  IO.mapTask (t := x) (prio := prio) (sync := sync) fun
-    | .ok a => f a
-    | .error e => throw e
-
-/--
-Block until the `AsyncTask` in `x` finishes.
--/
-def block (x : AsyncTask α) : IO α :=
-  match x.get with
-  | .ok a => return a
-  | .error e => throw e
-
-/--
-Create an `AsyncTask` that resolves to the value of `x`.
--/
-@[inline]
-def ofPromise (x : IO.Promise (Except IO.Error α)) (error : String := "the promise linked to the Async Task was dropped") : AsyncTask α :=
+def ofPromise (x : IO.Promise (Except IO.Error α)) (error : String := "the promise linked to the AsyncTask was dropped") : AsyncTask α :=
   x.result?.map fun
     | none => .error error
     | some res => res
 
 /--
-Create an `AsyncTask` that resolves to the value of `x`.
+Create an `AsyncTask` that resolves to the value of `x`. Returns an error if the promise is dropped.
 -/
 @[inline]
-def ofPurePromise (x : IO.Promise α) (error : String := "the promise linked to the Async Task was dropped") : AsyncTask α :=
+def ofPurePromise (x : IO.Promise α) (error : String := "the promise linked to the AsyncTask was dropped") : AsyncTask α :=
   x.result?.map (sync := true) fun
     | none => .error error
     | some res => pure res
 
-/--
-Obtain the `IO.TaskState` of `x`.
--/
-@[inline]
-def getState (x : AsyncTask α) : BaseIO IO.TaskState :=
-  IO.getTaskState x
+instance : ToAsync (IO.Promise (Except IO.Error α)) (AsyncTask α) where
+  toAsync x := AsyncTask.ofPromise x "the promise linked to the AsyncTask was dropped"
+
+instance : ToAsync (IO.Promise α) (AsyncTask α) where
+  toAsync x := AsyncTask.ofPurePromise x "the promise linked to the AsyncTask was dropped"
 
 end AsyncTask
 
@@ -397,10 +359,11 @@ def mk (x : BaseIO (MaybeTask α)) : BaseAsync α :=
   x
 
 /--
-Converts a `BaseAsync` into a `BaseIO`
+Unwraps a `BaseAsync` to access the underlying `BaseIO (MaybeTask α)`.
+This is an implementation detail and should not be used directly.
 -/
 @[inline]
-def toRawBaseIO (x : BaseAsync α) : BaseIO (MaybeTask α) :=
+protected def unwrap (x : BaseAsync α) : BaseIO (MaybeTask α) :=
   x
 
 /--
@@ -408,7 +371,7 @@ Converts a `BaseAsync` to a `BaseIO Task`.
 -/
 @[inline]
 protected def toBaseIO (x : BaseAsync α) : BaseIO (Task α) :=
-  MaybeTask.toTask <$> x.toRawBaseIO
+  MaybeTask.toTask <$> x.unwrap
 
 /--
 Creates a new `BaseAsync` out of a `Task`.
@@ -429,32 +392,29 @@ Maps the result of a `BaseAsync` computation with a function.
 -/
 @[inline]
 protected def map (f : α → β) (self : BaseAsync α) (prio := Task.Priority.default) (sync := false) : BaseAsync β :=
-  mk <| (·.map f prio sync) <$> self.toRawBaseIO
+  mk <| (·.map f prio sync) <$> self.unwrap
 
 /--
 Sequences two computations, allowing the second to depend on the value computed by the first.
 -/
 @[inline]
 protected def bind (self : BaseAsync α) (f : α → BaseAsync β) (prio := Task.Priority.default) (sync := false) : BaseAsync β :=
-  mk <| self.toRawBaseIO >>= (bindAsyncTask · f |>.toRawBaseIO)
-where
-  bindAsyncTask (t : MaybeTask α) (f : α → BaseAsync β) : BaseAsync β := .mk <|
-    match t with
-    | .pure a => (f a) |>.toRawBaseIO
-    | .ofTask t => .ofTask <$> BaseIO.bindTask t (fun a => MaybeTask.toTask <$> (f a |>.toRawBaseIO)) prio sync
+  mk <| self.unwrap >>= fun
+    | .pure a => (f a).unwrap
+    | .ofTask t => .ofTask <$> BaseIO.bindTask t (fun a => MaybeTask.toTask <$> (f a).unwrap) prio sync
 
 /--
 Lifts a `BaseIO` action into a `BaseAsync` computation.
 -/
 @[inline]
 protected def lift (x : BaseIO α) : BaseAsync α :=
-  .mk <| (pure ∘ pure) =<< x
+  .mk <| MaybeTask.pure <$> x
 
 /--
 Waits for the result of the `BaseAsync` computation, blocking if necessary.
 -/
 @[inline]
-protected def wait (self : BaseAsync α) : BaseIO α :=
+protected def block (self : BaseAsync α) : BaseIO α :=
   pure ∘ Task.get =<< self.toBaseIO
 
 /--
@@ -462,7 +422,7 @@ Lifts a `BaseAsync` computation into a `Task` that can be awaited and joined.
 -/
 @[inline]
 protected def asTask (x : BaseAsync α) (prio := Task.Priority.default) : BaseIO (Task α) := do
-  let res ← BaseIO.asTask (prio := prio) x.toRawBaseIO
+  let res ← BaseIO.asTask (prio := prio) x.unwrap
   return MaybeTask.joinTask res
 
 /--
@@ -527,16 +487,20 @@ The other result is lost and the other task is not cancelled, so the task will c
 until the end.
 -/
 @[inline, specialize]
-def race [Inhabited α] (x : BaseAsync α) (y : BaseAsync α) (prio := Task.Priority.default) : BaseAsync α := do
-  let promise ← IO.Promise.new
+def race (x : BaseAsync α) (y : BaseAsync α) (prio := Task.Priority.default) : BaseAsync α := do
+  -- Use Option α for the promise to avoid Inhabited constraint
+  let promise : IO.Promise (Option α) ← IO.Promise.new
 
   let task₁ : Task _ ← MonadAsync.async (prio := prio) x
   let task₂ : Task _ ← MonadAsync.async (prio := prio) y
 
-  BaseIO.chainTask task₁ (liftM ∘ promise.resolve)
-  BaseIO.chainTask task₂ (liftM ∘ promise.resolve)
+  BaseIO.chainTask task₁ (liftM ∘ promise.resolve ∘ some)
+  BaseIO.chainTask task₂ (liftM ∘ promise.resolve ∘ some)
 
-  MonadAwait.await promise.result!
+  let result ← MonadAwait.await promise.result!
+  match result with
+  | some a => pure a
+  | none => MonadAwait.await task₁  -- Fallback, shouldn't happen in practice
 
 /--
 Runs all computations in an `Array` concurrently and returns all results as an array.
@@ -561,6 +525,12 @@ def raceAll [Inhabited α] [ForM BaseAsync c (BaseAsync α)] (xs : c) (prio := T
 
   MonadAwait.await promise.result!
 
+instance : ToAsync (Task α) (BaseAsync α) where
+  toAsync := BaseAsync.ofTask
+
+instance : ToAsync (Except Empty α) (BaseAsync α) where
+  toAsync := BaseAsync.ofExcept
+
 end BaseAsync
 
 /--
@@ -575,10 +545,10 @@ Converts a `EAsync` to a `ETask`.
 -/
 @[inline]
 protected def toBaseIO (x : EAsync ε α) : BaseIO (ETask ε α) :=
-  MaybeTask.toTask <$> x.toRawBaseIO
+  MaybeTask.toTask <$> x.unwrap
 
 /--
-Creates a new `EAsync` out of a `RTask`.
+Creates a new `EAsync` out of an `ETask`.
 -/
 @[inline]
 protected def ofTask (x : ETask ε α) : EAsync ε α :=
@@ -589,14 +559,7 @@ Converts a `BaseAsync` to a `EIO ETask`.
 -/
 @[inline]
 protected def toEIO (x : EAsync ε α) : EIO ε (ETask ε α) :=
-  MaybeTask.toTask <$> x.toRawBaseIO
-
-/--
-Creates a new `EAsync` out of a `ETask`.
--/
-@[inline]
-protected def ofETask (x : ETask ε α) : EAsync ε α :=
-  .mk <| BaseAsync.ofTask x
+  MaybeTask.toTask <$> x.unwrap
 
 /--
 Creates an `EAsync` computation that immediately returns the given value.
@@ -609,15 +572,15 @@ protected def pure (a : α) : EAsync ε α :=
 Maps the result of an `EAsync` computation with a pure function.
 -/
 @[inline]
-protected def map (f : α → β) (self : EAsync ε α) : EAsync ε β :=
-  .mk <| BaseAsync.map (.map f) self
+protected def map (f : α → β) (self : EAsync ε α) (prio := Task.Priority.default) (sync := false) : EAsync ε β :=
+  .mk <| BaseAsync.map (.map f) self prio sync
 
 /--
 Sequences two computations, allowing the second to depend on the value computed by the first.
 -/
 @[inline]
-protected def bind (self : EAsync ε α) (f : α → EAsync ε β) : EAsync ε β :=
-  .mk <| BaseAsync.bind self fun
+protected def bind (self : EAsync ε α) (f : α → EAsync ε β) (prio := Task.Priority.default) (sync := false) : EAsync ε β :=
+  .mk <| BaseAsync.bind (prio := prio) (sync := sync) self fun
     | .ok a => f a
     | .error e => BaseAsync.pure (.error e)
 
@@ -632,11 +595,8 @@ protected def lift (x : EIO ε α) : EAsync ε α :=
 Waits for the result of the `EAsync` computation, blocking if necessary.
 -/
 @[inline]
-protected def wait (self : EAsync ε α) : EIO ε α := do
-  let result ← self |> BaseAsync.wait
-  match result with
-  | .ok a => return a
-  | .error e => throw e
+protected def block (self : EAsync ε α) : EIO ε α :=
+  liftExcept =<< BaseAsync.block self
 
 /--
 Lifts an `EAsync` computation into an `ETask` that can be awaited and joined.
@@ -645,13 +605,6 @@ Lifts an `EAsync` computation into an `ETask` that can be awaited and joined.
 protected def asTask (x : EAsync ε α) (prio := Task.Priority.default) : EIO ε (ETask ε α) :=
   x |> BaseAsync.asTask (prio := prio)
 
-/--
-Block until the `EAsync` finishes and returns its value. Propagates any error encountered during execution.
--/
-@[inline]
-protected def block (x : EAsync ε α) (prio := Task.Priority.default) : EIO ε α :=
-  x.asTask (prio := prio) >>= ETask.block
-
 /--
 Raises an error of type `ε` within the `EAsync` monad.
 -/
@@ -671,11 +624,9 @@ protected def tryCatch (x : EAsync ε α) (f : ε → EAsync ε α) (prio := Tas
 /--
 Runs an action, ensuring that some other action always happens afterward.
 -/
-protected def tryFinally'
-    (x : EAsync ε α) (f : Option α → EAsync ε β)
-    (prio := Task.Priority.default) (sync := false) :
-    EAsync ε (α × β) :=
-  .mk <| BaseAsync.bind x (prio := prio) (sync := sync) fun
+@[inline]
+protected def tryFinally' (x : EAsync ε α) (f : Option α → EAsync ε β) : EAsync ε (α × β) :=
+  .mk <| BaseAsync.bind x fun
     | .ok a => do
       match ← (f (some a)) with
       | .ok b => BaseAsync.pure (.ok (a, b))
@@ -776,7 +727,7 @@ protected partial def forIn
       | .ok (.yield b) => loop b
 
   loop init
-  .mk <| EAsync.ofETask promise.result!
+  .mk <| EAsync.ofTask promise.result!
 
 instance : ForIn (EAsync ε) Lean.Loop Unit where
   forIn _ := EAsync.forIn
@@ -805,19 +756,22 @@ The other result is lost and the other task is not cancelled, so the task will c
 until the end.
 -/
 @[inline, specialize]
-def race [Inhabited α] (x : EAsync ε α) (y : EAsync ε α)
+def race (x : EAsync ε α) (y : EAsync ε α)
     (prio := Task.Priority.default) :
     EAsync ε α := do
-  let promise ← IO.Promise.new
+  -- Use Option to avoid Inhabited constraint
+  let promise : IO.Promise (Option (Except ε α)) ← IO.Promise.new
 
   let task₁ : ETask ε _ ← MonadAsync.async (prio := prio) x
   let task₂ : ETask ε _ ← MonadAsync.async (prio := prio) y
 
-  BaseIO.chainTask task₁ (liftM ∘ promise.resolve)
-  BaseIO.chainTask task₂ (liftM ∘ promise.resolve)
+  BaseIO.chainTask task₁ (liftM ∘ promise.resolve ∘ some)
+  BaseIO.chainTask task₂ (liftM ∘ promise.resolve ∘ some)
 
   let result ← MonadAwait.await promise.result!
-  EAsync.ofExcept result
+  match result with
+  | some res => EAsync.ofExcept res
+  | none => MonadAwait.await task₁  -- Fallback, shouldn't happen
 
 /--
 Runs all computations in an `Array` concurrently and returns all results as an array.
@@ -843,6 +797,12 @@ def raceAll [Inhabited α] [ForM (EAsync ε) c (EAsync ε α)] (xs : c) (prio :=
   let result ← MonadAwait.await promise.result!
   EAsync.ofExcept result
 
+instance : ToAsync (ETask ε α) (EAsync ε α) where
+  toAsync := EAsync.ofTask
+
+instance : ToAsync (Except ε α) (EAsync ε α) where
+  toAsync := EAsync.ofExcept
+
 end EAsync
 
 /--
@@ -857,20 +817,20 @@ Converts a `Async` to a `AsyncTask`.
 -/
 @[inline]
 protected def toIO (x : Async α) : IO (AsyncTask α) :=
-  MaybeTask.toTask <$> x.toRawBaseIO
+  MaybeTask.toTask <$> x.unwrap
 
 /--
-Block until the `Async` finishes and returns its value. Propagates any error encountered during execution.
+Waits for the result of the `Async` computation, blocking if necessary.
 -/
 @[inline]
-protected def block (x : Async α) (prio := Task.Priority.default) : IO α :=
-  x.asTask (prio := prio) >>= ETask.block
+protected def block (self : Async α) : IO α :=
+  EAsync.block self
 
 /--
 Converts `Promise` into `Async`.
 -/
 @[inline]
-protected def ofPromise (task : IO (IO.Promise (Except IO.Error α))) (error : String := "the promise linked to the Async was dropped") : Async α := do
+protected def ofIOPromise (task : IO (IO.Promise (Except IO.Error α))) (error : String := "the promise linked to the Async was dropped") : Async α := do
   match ← task.toBaseIO with
   | .ok data => pure (f := BaseIO) <| MaybeTask.ofTask <| data.result?.map fun
     | none => .error error
@@ -932,12 +892,8 @@ instance : MonadAwait IO.Promise Async :=
 Runs two computations concurrently and returns both results as a pair.
 -/
 @[inline, specialize]
-def concurrently (x : Async α) (y : Async β) (prio := Task.Priority.default) : Async (α × β) := do
-  let taskX ← MonadAsync.async x (prio := prio)
-  let taskY ← MonadAsync.async y (prio := prio)
-  let resultX ← MonadAwait.await taskX
-  let resultY ← MonadAwait.await taskY
-  return (resultX, resultY)
+def concurrently (x : Async α) (y : Async β) (prio := Task.Priority.default) : Async (α × β) :=
+  EAsync.concurrently x y prio
 
 /--
 Runs two computations concurrently and returns the result of the one that finishes first.
@@ -945,27 +901,15 @@ The other result is lost and the other task is not cancelled, so the task will c
 until the end.
 -/
 @[inline, specialize]
-def race [Inhabited α] (x : Async α) (y : Async α)
-    (prio := Task.Priority.default) :
-    Async α := do
-  let promise ← IO.Promise.new
-
-  let task₁ ← MonadAsync.async (t := AsyncTask) (prio := prio) x
-  let task₂ ← MonadAsync.async (t := AsyncTask) (prio := prio) y
-
-  BaseIO.chainTask task₁ (liftM ∘ promise.resolve)
-  BaseIO.chainTask task₂ (liftM ∘ promise.resolve)
-
-  let result ← MonadAwait.await promise
-  Async.ofExcept result
+def race (x : Async α) (y : Async α) (prio := Task.Priority.default) : Async α :=
+  EAsync.race x y prio
 
 /--
 Runs all computations in an `Array` concurrently and returns all results as an array.
 -/
 @[inline, specialize]
-def concurrentlyAll (xs : Array (Async α)) (prio := Task.Priority.default) : Async (Array α) := do
-  let tasks : Array (AsyncTask α) ← xs.mapM (MonadAsync.async (prio := prio))
-  tasks.mapM MonadAwait.await
+def concurrentlyAll (xs : Array (Async α)) (prio := Task.Priority.default) : Async (Array α) :=
+  EAsync.concurrentlyAll xs prio
 
 /--
 Runs all computations concurrently and returns the result of the first one to finish.
@@ -973,15 +917,23 @@ All other results are lost, and the tasks are not cancelled, so they'll continue
 until the end.
 -/
 @[inline, specialize]
-def raceAll [ForM Async c (Async α)] (xs : c) (prio := Task.Priority.default) : Async α := do
-  let promise ← IO.Promise.new
+def raceAll [Inhabited α] [ForM (EAsync IO.Error) c (EAsync IO.Error α)] (xs : c) (prio := Task.Priority.default) : Async α :=
+  EAsync.raceAll xs prio
 
-  ForM.forM xs fun x => do
-    let task₁ ← MonadAsync.async (t := AsyncTask) (prio := prio) x
-    BaseIO.chainTask task₁ (liftM ∘ promise.resolve)
+instance : ToAsync (AsyncTask α) (Async α) where
+  toAsync := Async.ofAsyncTask
 
-  let result ← MonadAwait.await promise
-  Async.ofExcept result
+instance : ToAsync (Task α) (Async α) where
+  toAsync := Async.ofTask
+
+instance : ToAsync (Except IO.Error α) (Async α) where
+  toAsync := Async.ofExcept
+
+instance : ToAsync (IO (IO.Promise (Except IO.Error α))) (Async α) where
+  toAsync x := Async.ofIOPromise x "the promise linked to the Async was dropped"
+
+instance : ToAsync (IO (IO.Promise α)) (Async α) where
+  toAsync x := Async.ofPurePromise x "the promise linked to the Async was dropped"
 
 end Async
 
@@ -995,7 +947,4 @@ This function transforms the operation inside the monad `m` into a task and let
 def background [Monad m] [MonadAsync t m] (action : m α) (prio := Task.Priority.default) : m Unit :=
   discard (async (t := t) (prio := prio) action)
 
-end Async
-end IO
-end Internal
-end Std
+end Std.Async

src/Std/Async/ContextAsync.lean

@@ -8,8 +8,8 @@ module
 prelude
 public import Std.Time
 public import Std.Internal.UV
-public import Std.Internal.Async.Basic
-public import Std.Internal.Async.Timer
+public import Std.Async.Basic
+public import Std.Async.Timer
 public import Std.Sync.CancellationContext
 
 public section
@@ -19,10 +19,7 @@ This module contains the implementation of `ContextAsync`, a monad for asynchron
 cooperative cancellation support that must be explicitly checked for and cancelled explicitly.
 -/
 
-namespace Std
-namespace Internal
-namespace IO
-namespace Async
+namespace Std.Async
 
 /--
 An asynchronous computation with cooperative cancellation support via a `CancellationContext`. `ContextAsync α`
@@ -267,7 +264,4 @@ This is useful for selecting on cancellation alongside other asynchronous operat
 def Selector.cancelled : ContextAsync (Selector Unit) := do
   ContextAsync.doneSelector
 
-end Async
-end IO
-end Internal
-end Std
+end Std.Async

src/Std/Async/DNS.lean

@@ -8,17 +8,13 @@ module
 prelude
 public import Std.Time
 public import Std.Internal.UV
-public import Std.Internal.Async.Basic
+public import Std.Async.Basic
 
 public section
 
-namespace Std
-namespace Internal
-namespace IO
-namespace Async
-namespace DNS
+namespace Std.Async.DNS
 
-open Std.Net
+open Std.Net Internal UV
 
 /--
 Represents a resolved hostname and service name from a socket address.
@@ -39,7 +35,7 @@ Asynchronously resolves a hostname and service to an array of socket addresses.
 -/
 @[inline]
 def getAddrInfo (host : String) (service : String) (addrFamily : Option AddressFamily := none) : Async (Array IPAddr) := do
-  Async.ofPromise <| UV.DNS.getAddrInfo
+  Async.ofIOPromise <| UV.DNS.getAddrInfo
     host
     service
     (match addrFamily with
@@ -53,11 +49,7 @@ Performs a reverse DNS lookup on a `SocketAddress`.
 @[inline]
 def getNameInfo (host : @& SocketAddress) : Async NameInfo :=
   UV.DNS.getNameInfo host
-  |> Async.ofPromise
+  |> Async.ofIOPromise
   |>.map (Function.uncurry NameInfo.mk)
 
-end DNS
-end Async
-end IO
-end Internal
-end Std
+end Std.Async.DNS

src/Std/Async/IO.lean

@@ -6,16 +6,11 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Async.Select
+public import Std.Async.Select
 
 public section
 
-namespace Std
-namespace Internal
-namespace Async
-namespace IO
-
-open Std.Internal.IO.Async
+namespace Std.Async
 
 /-!
 This module provides buffered asynchronous I/O operations for efficient reading and writing.
@@ -48,7 +43,4 @@ class AsyncStream (α : Type) (β : outParam Type) where
   stop : α → IO Unit :=
     fun _ => pure ()
 
-end IO
-end Async
-end Internal
-end Std
+end Std.Async

src/Std/Async/Process.lean

@@ -12,13 +12,9 @@ public import Std.Data.HashMap
 
 public section
 
+namespace Std.Async.Process
 open Std Time
-open System
-
-namespace Std
-namespace Internal
-namespace IO
-namespace Process
+open Internal UV System
 
 /--
 Represents resource usage statistics for a process or thread.
@@ -236,7 +232,4 @@ Returns the available memory for allocation in bytes.
 def availableMemory : IO UInt64 :=
   UV.System.availableMemory
 
-end Process
-end IO
-end Internal
-end Std
+end Std.Async.Process

src/Std/Async/Select.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Init.Data.Random
-public import Std.Internal.Async.Basic
+public import Std.Async.Basic
 import Init.Data.ByteArray.Extra
 
 public section
@@ -18,10 +18,7 @@ The main entrypoint for users is `Selectable.one` and the various functions to p
 `Selector`s from other modules.
 -/
 
-namespace Std
-namespace Internal
-namespace IO
-namespace Async
+namespace Std.Async
 
 /--
 The core data structure for racing on winning a `Selectable.one` if multiple event sources are ready
@@ -166,7 +163,7 @@ partial def Selectable.one (selectables : Array (Selectable α)) : Async α := d
 
         async.toBaseIO
 
-  Async.ofPromise (pure promise)
+  Async.ofIOPromise (pure promise)
 
 /--
 Performs fair and data-loss free non-blocking multiplexing on the `Selectable`s in `selectables`.
@@ -245,7 +242,4 @@ def Selectable.combine (selectables : Array (Selectable α)) : IO (Selector α)
         selectable.selector.unregisterFn
   }
 
-end Async
-end IO
-end Internal
-end Std
+end Std.Async

src/Std/Async/Signal.lean

@@ -8,14 +8,11 @@ module
 prelude
 public import Std.Time
 public import Std.Internal.UV.Signal
-public import Std.Internal.Async.Select
+public import Std.Async.Select
 
 public section
 
-namespace Std
-namespace Internal
-namespace IO
-namespace Async
+namespace Std.Async
 
 /--
 Unix style signals for Unix and Windows. SIGKILL and SIGSTOP are missing because they cannot be caught.
@@ -261,3 +258,5 @@ def selector (s : Signal.Waiter) : Selector Unit :=
     unregisterFn := s.native.cancel
 
   }
+
+end Std.Async.Signal.Waiter

src/Std/Async/System.lean

@@ -18,13 +18,9 @@ manipulation.
 -/
 
 open Std Time
-open System
+open Internal UV System
 
-namespace Std
-namespace Internal
-namespace IO
-namespace Async
-namespace System
+namespace Std.Async.System
 
 /--
 A group identifier, represented by a numeric ID in UNIX systems (e.g. 1000).
@@ -314,8 +310,4 @@ def getGroup (groupId : GroupId) : IO (Option GroupInfo) := do
     members := group.members
   }
 
-end System
-end Async
-end IO
-end Internal
-end Std
+end Std.Async.System

src/Std/Async/TCP.lean

@@ -8,15 +8,11 @@ module
 prelude
 public import Std.Time
 public import Std.Internal.UV.TCP
-public import Std.Internal.Async.Select
+public import Std.Async.Select
 
 public section
 
-namespace Std
-namespace Internal
-namespace IO
-namespace Async
-namespace TCP
+namespace Std.Async.TCP
 open Std.Net
 
 namespace Socket
@@ -66,7 +62,7 @@ Accepts an incoming connection.
 @[inline]
 def accept (s : Server) : Async Client := do
   s.native.accept
-  |> Async.ofPromise
+  |> Async.ofIOPromise
   |>.map Client.ofNative
 
 /--
@@ -153,21 +149,21 @@ Connects the client socket to the given address.
 -/
 @[inline]
 def connect (s : Client) (addr : SocketAddress) : Async Unit :=
-  Async.ofPromise <| s.native.connect addr
+  Async.ofIOPromise <| s.native.connect addr
 
 /--
 Sends multiple data buffers through the client socket.
 -/
 @[inline]
 def sendAll (s : Client) (data : Array ByteArray) : Async Unit :=
-  Async.ofPromise <| s.native.send data
+  Async.ofIOPromise <| s.native.send data
 
 /--
 Sends data through the client socket.
 -/
 @[inline]
 def send (s : Client) (data : ByteArray) : Async Unit :=
-  Async.ofPromise <| s.native.send #[data]
+  Async.ofIOPromise <| s.native.send #[data]
 
 /--
 Receives data from the client socket. If data is received, it’s wrapped in .some. If EOF is reached,
@@ -177,7 +173,7 @@ Furthermore calling this function in parallel with `recvSelector` is not support
 -/
 @[inline]
 def recv? (s : Client) (size : UInt64) : Async (Option ByteArray) :=
-  Async.ofPromise <| s.native.recv? size
+  Async.ofIOPromise <| s.native.recv? size
 
 /--
 Creates a `Selector` that resolves once `s` has data available, up to at most `size` bytes,
@@ -224,7 +220,7 @@ Shuts down the write side of the client socket.
 -/
 @[inline]
 def shutdown (s : Client) : Async Unit :=
-  Async.ofPromise <| s.native.shutdown
+  Async.ofIOPromise <| s.native.shutdown
 
 /--
 Gets the remote address of the client socket.
@@ -256,8 +252,4 @@ def keepAlive (s : Client) (enable : Bool) (delay : Std.Time.Second.Offset) (_ :
 
 end Client
 end Socket
-end TCP
-end Async
-end IO
-end Internal
-end Std
+end Std.Async.TCP

src/Std/Async/Timer.lean

@@ -8,15 +8,12 @@ module
 prelude
 public import Std.Time
 public import Std.Internal.UV.Timer
-public import Std.Internal.Async.Select
+public import Std.Async.Select
 
 public section
 
 
-namespace Std
-namespace Internal
-namespace IO
-namespace Async
+namespace Std.Async
 
 /--
 `Sleep` can be used to sleep for some duration once.
@@ -167,7 +164,4 @@ def stop (i : Interval) : IO Unit :=
 
 end Interval
 
-end Async
-end IO
-end Internal
-end Std
+end Std.Async

src/Std/Async/UDP.lean

@@ -8,15 +8,11 @@ module
 prelude
 public import Std.Time
 public import Std.Internal.UV.UDP
-public import Std.Internal.Async.Select
+public import Std.Async.Select
 
 public section
 
-namespace Std
-namespace Internal
-namespace IO
-namespace Async
-namespace UDP
+namespace Std.Async.UDP
 
 open Std.Net
 
@@ -66,7 +62,7 @@ address. If `addr` is `none`, the data is sent to the default peer address set b
 -/
 @[inline]
 def sendAll (s : Socket) (data : Array ByteArray) (addr : Option SocketAddress := none) : Async Unit :=
-  Async.ofPromise <| s.native.send data addr
+  Async.ofIOPromise <| s.native.send data addr
 
 /--
 Sends data through an UDP socket. The `addr` parameter specifies the destination address. If `addr`
@@ -74,7 +70,7 @@ is `none`, the data is sent to the default peer address set by `connect`.
 -/
 @[inline]
 def send (s : Socket) (data : ByteArray) (addr : Option SocketAddress := none) : Async Unit :=
-  Async.ofPromise <| s.native.send #[data] addr
+  Async.ofIOPromise <| s.native.send #[data] addr
 
 /--
 Receives data from an UDP socket. `size` is for the maximum bytes to receive.
@@ -85,7 +81,7 @@ Furthermore calling this function in parallel with `recvSelector` is not support
 -/
 @[inline]
 def recv (s : Socket) (size : UInt64) : Async (ByteArray × Option SocketAddress) :=
-  Async.ofPromise <| s.native.recv size
+  Async.ofIOPromise <| s.native.recv size
 
 /--
 Creates a `Selector` that resolves once `s` has data available, up to at most `size` bytes,
@@ -190,8 +186,4 @@ def setTTL (s : Socket) (ttl : UInt32) : IO Unit :=
 
 end Socket
 
-end UDP
-end Async
-end IO
-end Internal
-end Std
+end Std.Async.UDP

src/Std/Internal.lean

@@ -6,7 +6,6 @@ Authors: Henrik Böving
 module
 
 prelude
-public import Std.Internal.Async
 public import Std.Internal.Parsec
 public import Std.Internal.UV
 

src/Std/Internal/Async.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving
--/
-module
-
-prelude
-public import Std.Internal.Async.Basic
-public import Std.Internal.Async.ContextAsync
-public import Std.Internal.Async.Timer
-public import Std.Internal.Async.TCP
-public import Std.Internal.Async.UDP
-public import Std.Internal.Async.DNS
-public import Std.Internal.Async.Select
-public import Std.Internal.Async.Process
-public import Std.Internal.Async.System
-public import Std.Internal.Async.Signal
-public import Std.Internal.Async.IO

src/Std/Sync/Broadcast.lean

@@ -10,14 +10,13 @@ public import Std.Data
 public import Init.Data.Queue
 public import Init.Data.Vector
 public import Std.Sync.Mutex
-public import Std.Internal.Async.IO
+public import Std.Async.IO
 
 public section
 
 namespace Std
 
-open Std.Internal.Async.IO
-open Std.Internal.IO.Async
+open Std.Async
 
 /-!
 The `Std.Sync.Broadcast` module implements a broadcasting primitive for sending values
@@ -60,7 +59,7 @@ instance instMonadLiftBroadcastIO : MonadLift (EIO Broadcast.Error) IO where
 
 private structure Broadcast.Consumer (α : Type) where
   promise : IO.Promise Bool
-  waiter : Option (Internal.IO.Async.Waiter (Option α))
+  waiter : Option (Async.Waiter (Option α))
 
 private def Broadcast.Consumer.resolve (c : Broadcast.Consumer α) (b : Bool) : BaseIO Unit :=
   c.promise.resolve b
@@ -403,7 +402,6 @@ private def recvReady'
     let slotVal ← slot.get
     return slotVal.pos = next
 
-open Internal.IO.Async in
 private partial def recvSelector (ch : Bounded.Receiver α) : Selector (Option α) where
   tryFn := do
     ch.state.atomically do
@@ -537,8 +535,6 @@ the next available message. This will block until a message is available.
 def recv [Inhabited α] (ch : Broadcast.Receiver α) : BaseIO (Task (Option α)) := do
   Std.Bounded.Receiver.recv ch.inner
 
-open Internal.IO.Async in
-
 /--
 Creates a `Selector` that resolves once the broadcast channel `ch` has data available and provides that data.
 -/
@@ -567,7 +563,7 @@ instance [Inhabited α] : AsyncStream (Broadcast.Receiver α) (Option α) where
   stop channel := channel.unsubscribe
 
 instance [Inhabited α] : AsyncRead (Broadcast.Receiver α) (Option α) where
-  read receiver := Internal.IO.Async.Async.ofIOTask receiver.recv
+  read receiver := Async.ofIOTask receiver.recv
 
 instance [Inhabited α] : AsyncWrite (Broadcast α) α where
   write receiver x := do

src/Std/Sync/CancellationContext.lean

@@ -11,7 +11,7 @@ public import Init.System.Promise
 public import Init.Data.Queue
 public import Std.Sync.Mutex
 public import Std.Sync.CancellationToken
-public import Std.Internal.Async.Select
+public import Std.Async.Select
 
 public section
 
@@ -21,7 +21,7 @@ automatically cancels all child contexts.
 -/
 
 namespace Std
-open Std.Internal.IO.Async
+open Std.Async
 
 structure CancellationContext.State where
   /--

src/Std/Sync/CancellationToken.lean

@@ -9,7 +9,7 @@ prelude
 public import Std.Data
 public import Init.Data.Queue
 public import Std.Sync.Mutex
-public import Std.Internal.Async.Select
+public import Std.Async.Select
 
 public section
 
@@ -21,7 +21,7 @@ that a cancellation has occurred.
 -/
 
 namespace Std
-open Std.Internal.IO.Async
+open Std.Async
 
 /--
 Reasons for cancellation.

src/Std/Sync/Channel.lean

@@ -8,13 +8,13 @@ module
 prelude
 public import Init.Data.Queue
 public import Std.Sync.Mutex
-public import Std.Internal.Async.IO
+public import Std.Async.IO
 import Init.Data.Vector.Basic
 
 public section
 
-open Std.Internal.Async.IO
-open Std.Internal.IO.Async
+open Std.Async
+open Std.Async
 
 /-!
 This module contains the implementation of `Std.Channel`. `Std.Channel` is a multi-producer
@@ -51,7 +51,6 @@ instance : ToString Error where
 instance : MonadLift (EIO Error) IO where
   monadLift x := EIO.toIO (.userError <| toString ·) x
 
-open Internal.IO.Async in
 private inductive Consumer (α : Type) where
   | normal (promise : IO.Promise (Option α))
   | select (finished : Waiter (Option α))
@@ -172,7 +171,6 @@ private def recvReady' [Monad m] [MonadLiftT (ST IO.RealWorld) m] :
   let st ← get
   return !st.values.isEmpty || st.closed
 
-open Internal.IO.Async in
 private def recvSelector (ch : Unbounded α) : Selector (Option α) where
   tryFn := do
     ch.state.atomically do
@@ -322,7 +320,6 @@ private def recvReady' [Monad m] [MonadLiftT (ST IO.RealWorld) m] :
   let st ← get
   return !st.producers.isEmpty || st.closed
 
-open Internal.IO.Async in
 private def recvSelector (ch : Zero α) : Selector (Option α) where
   tryFn := do
     ch.state.atomically do
@@ -356,7 +353,6 @@ private def recvSelector (ch : Zero α) : Selector (Option α) where
 
 end Zero
 
-open Internal.IO.Async in
 private structure Bounded.Consumer (α : Type) where
   promise : IO.Promise Bool
   waiter : Option (Waiter (Option α))
@@ -558,7 +554,6 @@ private def recvReady' [Monad m] [MonadLiftT (ST IO.RealWorld) m] :
   let st ← get
   return st.bufCount != 0 || st.closed
 
-open Internal.IO.Async in
 private partial def recvSelector (ch : Bounded α) : Selector (Option α) where
   tryFn := do
     ch.state.atomically do
@@ -732,7 +727,6 @@ def recv (ch : CloseableChannel α) : BaseIO (Task (Option α)) :=
   | .zero ch => CloseableChannel.Zero.recv ch
   | .bounded ch => CloseableChannel.Bounded.recv ch
 
-open Internal.IO.Async in
 /--
 Creates a `Selector` that resolves once `ch` has data available and provides that data.
 In particular if `ch` is closed while waiting on this `Selector` and no data is available already
@@ -759,7 +753,7 @@ instance [Inhabited α] : AsyncStream (CloseableChannel α) (Option α) where
   next channel := channel.recvSelector
 
 instance [Inhabited α] : AsyncRead (CloseableChannel α) (Option α) where
-  read receiver := Internal.IO.Async.Async.ofIOTask receiver.recv
+  read receiver := Async.ofIOTask receiver.recv
 
 instance [Inhabited α] : AsyncWrite (CloseableChannel α) α where
   write receiver x := do
@@ -877,7 +871,6 @@ def recv [Inhabited α] (ch : Channel α) : BaseIO (Task α) := do
       | some val => return .pure val
       | none => unreachable!
 
-open Internal.IO.Async in
 /--
 Creates a `Selector` that resolves once `ch` has data available and provides that data.
 -/
@@ -909,7 +902,7 @@ instance [Inhabited α] : AsyncStream (Channel α) α where
   next channel := channel.recvSelector
 
 instance [Inhabited α] : AsyncRead (Channel α) α where
-  read receiver := Internal.IO.Async.Async.ofIOTask receiver.recv
+  read receiver := Async.ofIOTask receiver.recv
 
 instance [Inhabited α] : AsyncWrite (Channel α) α where
   write receiver x := do

src/Std/Sync/Notify.lean

@@ -8,7 +8,7 @@ module
 prelude
 public import Init.Data.Queue
 public import Std.Sync.Mutex
-public import Std.Internal.Async.Select
+public import Std.Async.Select
 
 public section
 
@@ -24,7 +24,7 @@ will be woken up per notification.
 -/
 
 namespace Std
-open Std.Internal.IO.Async
+open Std.Async
 
 inductive Notify.Consumer (α : Type) where
   | normal (promise : IO.Promise α)

src/Std/Sync/StreamMap.lean

@@ -8,19 +8,17 @@ module
 prelude
 public import Std.Data
 public import Init.Data.Queue
-public import Std.Internal.Async.IO
+public import Std.Async.IO
 
 public section
 
-open Std.Internal.Async.IO
-open Std.Internal.IO.Async
-
 /-!
 This module provides `StreamMap`, a container that maps keys to async streams.
 It allows for dynamic management of multiple named streams with async operations.
 -/
 
 namespace Std
+open Std.Async
 
 /--
 This is an existential wrapper for AsyncStream that is used for the `.ofArray` function

src/Std/Tactic/Do/Syntax.lean

@@ -290,6 +290,7 @@ syntax "∀" binderIdent : mintroPat
 @[tactic_alt Lean.Parser.Tactic.mintroMacro]
 syntax (name := mintro) "mintro" (ppSpace colGt mintroPat)+ : tactic
 
+@[tactic_alt Lean.Parser.Tactic.mintroMacro]
 macro (name := mintroError) "mintro" : tactic => Macro.throwError "`mintro` expects at least one pattern"
 
 macro_rules

src/lake/Lake/Build/Common.lean

@@ -9,7 +9,7 @@ prelude
 public import Lake.Build.Job.Monad
 public import Lake.Config.Monad
 public import Lake.Util.JsonObject
-import Lake.Util.IO
+public import Lake.Util.IO
 import Lake.Build.Target.Fetch
 public import Lake.Build.Actions
 
@@ -304,17 +304,20 @@ and log are saved to `traceFile`, if the build completes without a fatal error
   (depTrace : BuildTrace) (traceFile : FilePath) (build : JobM α)
   (action : JobAction := .build)
 : JobM α := do
+  updateAction action
+  let noBuildTraceFile := traceFile.addExtension "nobuild"
   if (← getNoBuild) then
-    updateAction .build
+    modify ({· with wantsRebuild := true})
+    writeBuildTrace noBuildTraceFile depTrace Json.null {}
     error s!"target is out-of-date and needs to be rebuilt"
   else
-    updateAction action
     let startTime ← IO.monoMsNow
     try
       let iniPos ← getLogPos
       let a ← build -- fatal errors will abort here
       let log := (← getLog).takeFrom iniPos
       writeBuildTrace traceFile depTrace (toOutputJson a) log
+      removeFileIfExists noBuildTraceFile
       return a
     finally
       let endTime ← IO.monoMsNow

src/lake/Lake/Build/Job/Basic.lean

@@ -63,6 +63,8 @@ public structure JobState where
   log : Log := {}
   /-- Tracks whether this job performed any significant build action. -/
   action : JobAction := .unknown
+  /-- Whether this job failed due to a request to rebuild for `--no-build`. -/
+  wantsRebuild : Bool := false
   /-- Current trace of a build job. -/
   trace : BuildTrace := .nil
   /-- How long the job spent building (in milliseconds). -/
@@ -72,6 +74,7 @@ public structure JobState where
 public def JobState.merge (a b : JobState) : JobState where
   log := a.log ++ b.log
   action := a.action.merge b.action
+  wantsRebuild := a.wantsRebuild || b.wantsRebuild
   trace := mixTrace a.trace b.trace
   buildTime := a.buildTime + b.buildTime
 

src/lake/Lake/Build/Run.lean

@@ -50,14 +50,14 @@ private structure MonitorContext where
   /-- How often to poll jobs (in milliseconds). -/
   updateFrequency : Nat
 
-@[inline] def MonitorContext.logger (ctx : MonitorContext) : MonadLog IO :=
+@[inline] def MonitorContext.logger (ctx : MonitorContext) : MonadLog BaseIO :=
   .stream ctx.out ctx.outLv ctx.useAnsi
 
 /-- State of the Lake build monitor. -/
 private structure MonitorState where
   jobNo : Nat := 0
   totalJobs : Nat := 0
-  didBuild : Bool := false
+  wantsRebuild : Bool := false
   failures : Array String
   resetCtrl : String
   lastUpdate : Nat
@@ -114,16 +114,17 @@ private def renderProgress (running unfinished : Array OpaqueJob) (h : 0 < unfin
     flush
 
 private def reportJob (job : OpaqueJob) : MonitorM PUnit := do
-  let {jobNo, totalJobs, didBuild, ..} ← get
+  let {jobNo, totalJobs, ..} ← get
   let {failLv, outLv, showOptional, out, useAnsi, showProgress, minAction, showTime, ..} ← read
   let {task, caption, optional, ..} := job
-  let {log, action, buildTime, ..} := task.get.state
+  let {log, action, wantsRebuild, buildTime, ..} := task.get.state
   let maxLv := log.maxLv
   let failed := strictAnd log.hasEntries (maxLv ≥ failLv)
-   if !didBuild && action = .build then
-    modify fun s => {s with didBuild := true}
   if failed && !optional then
-    modify fun s => {s with failures := s.failures.push caption}
+    modify fun s => {s with
+      failures := s.failures.push caption
+      wantsRebuild := s.wantsRebuild || wantsRebuild
+    }
   let hasOutput := failed || (log.hasEntries && maxLv ≥ outLv)
   let showJob :=
     (!optional || showOptional) &&
@@ -195,7 +196,7 @@ end Monitor
 
 /-- **For internal use only.** -/
 public structure MonitorResult where
-  didBuild : Bool
+  wantsRebuild : Bool
   failures : Array String
   numJobs : Nat
 
@@ -233,11 +234,11 @@ def monitorJobs'
   return {
     failures := s.failures
     numJobs := s.totalJobs
-    didBuild := s.didBuild
+    wantsRebuild := s.wantsRebuild
   }
 
 /-- The job monitor function. An auxiliary definition for `runFetchM`. -/
-@[inline, deprecated "Deprecated without replacement" (since := "2025-01-08")]
+@[inline, deprecated "Deprecated without replacement." (since := "2025-01-08")]
 public def monitorJobs
   (initJobs : Array OpaqueJob)
   (jobs : IO.Ref (Array OpaqueJob))
@@ -259,9 +260,9 @@ public def monitorJobs
 public def noBuildCode : ExitCode := 3
 
 def Workspace.saveOutputs
-  [logger : MonadLog IO] (ws : Workspace)
+  [logger : MonadLog BaseIO] (ws : Workspace)
   (out : IO.FS.Stream) (outputsFile : FilePath) (isVerbose : Bool)
-: IO Unit := do
+: BaseIO Unit := do
   unless ws.isRootArtifactCacheEnabled do
     logWarning s!"{ws.root.prettyName}: \
       the artifact cache is not enabled for this package, so the artifacts described \
@@ -313,13 +314,20 @@ def monitorJob (ctx : MonitorContext) (job : Job α) : BaseIO (BuildResult α) :
   else
     return {toMonitorResult := result, out := .error "build failed"}
 
-def monitorFetchM
-  (mctx : MonitorContext) (bctx : BuildContext) (build : FetchM α)
+def mkBuildContext' (ws : Workspace) (cfg : BuildConfig) (jobs : JobQueue) : BuildContext where
+  opaqueWs := ws
+  toBuildConfig := cfg
+  registeredJobs := jobs
+  leanTrace := .ofHash (pureHash ws.lakeEnv.leanGithash)
+    s!"Lean {Lean.versionStringCore}, commit {ws.lakeEnv.leanGithash}"
+
+def Workspace.startBuild
+  (ws : Workspace)  (cfg : BuildConfig) (jobs : JobQueue) (build : FetchM α)
   (caption := "job computation")
-: BaseIO (BuildResult α) := do
+: BaseIO (Job α) := do
+  let bctx := mkBuildContext' ws cfg jobs
   let compute := Job.async build (caption := caption)
-  let job ← compute.run.run'.run bctx |>.run nilTrace
-  monitorJob mctx job
+  compute.run.run'.run bctx |>.run nilTrace
 
 def Workspace.finalizeBuild
   (ws : Workspace) (cfg : BuildConfig) (ctx : MonitorContext) (result : BuildResult α)
@@ -327,18 +335,11 @@ def Workspace.finalizeBuild
   reportResult cfg ctx.out result
   if let some outputsFile := cfg.outputsFile? then
     ws.saveOutputs (logger := ctx.logger) ctx.out outputsFile (cfg.verbosity matches .verbose)
-  if cfg.noBuild && result.didBuild then
+  if cfg.noBuild && result.wantsRebuild then
     IO.Process.exit noBuildCode.toUInt8
   else
     IO.ofExcept result.out
 
-def mkBuildContext' (ws : Workspace) (cfg : BuildConfig) (jobs : JobQueue) : BuildContext where
-  opaqueWs := ws
-  toBuildConfig := cfg
-  registeredJobs := jobs
-  leanTrace := .ofHash (pureHash ws.lakeEnv.leanGithash)
-    s!"Lean {Lean.versionStringCore}, commit {ws.lakeEnv.leanGithash}"
-
 /--
 Run a build function in the Workspace's context using the provided configuration.
 Reports incremental build progress and build logs. In quiet mode, only reports
@@ -349,16 +350,13 @@ public def Workspace.runFetchM
 : IO α := do
   let jobs ← mkJobQueue
   let mctx ← mkMonitorContext cfg jobs
-  let bctx := mkBuildContext' ws cfg jobs
-  let result ← monitorFetchM mctx bctx build caption
+  let job ← ws.startBuild cfg jobs build caption
+  let result ← monitorJob mctx job
   ws.finalizeBuild cfg mctx result
 
-def monitorBuild
-  (mctx : MonitorContext) (bctx : BuildContext) (build : FetchM (Job α))
-  (caption := "job computation")
-: BaseIO (BuildResult α) := do
-  let result ← monitorFetchM mctx bctx build caption
-   match result.out with
+def monitorBuild (mctx : MonitorContext) (job : Job (Job α)) : BaseIO (BuildResult α) := do
+  let result ← monitorJob mctx job
+  match result.out with
   | .ok job =>
     if let some a ← job.wait? then
       return {result with out := .ok a}
@@ -374,24 +372,24 @@ Returns whether a build is needed to validate `build`. Does not report on the at
 
 This is equivalent to checking whether `lake build --no-build` exits with code 0.
 -/
-@[inline] public def Workspace.checkNoBuild
+public def Workspace.checkNoBuild
   (ws : Workspace) (build : FetchM (Job α))
 : BaseIO Bool := do
   let jobs ← mkJobQueue
   let cfg := {noBuild := true}
   let mctx ← mkMonitorContext cfg jobs
-  let bctx := mkBuildContext' ws cfg jobs
-  let result ← monitorBuild mctx bctx build
-  return result.isOk && !result.didBuild
+  let job ← ws.startBuild cfg jobs build
+  let result ← monitorBuild mctx job
+  return result.isOk -- `isOk` means no failures, and thus no `--no-build` failures
 
 /-- Run a build function in the Workspace's context and await the result. -/
-@[inline] public def Workspace.runBuild
+public def Workspace.runBuild
   (ws : Workspace) (build : FetchM (Job α)) (cfg : BuildConfig := {})
 : IO α := do
   let jobs ← mkJobQueue
   let mctx ← mkMonitorContext cfg jobs
-  let bctx := mkBuildContext' ws cfg jobs
-  let result ← monitorBuild mctx bctx build
+  let job ← ws.startBuild cfg jobs build
+  let result ← monitorBuild mctx job
   ws.finalizeBuild cfg mctx result
 
 /-- Produce a build job in the Lake monad's workspace and await the result. -/

src/lake/Lake/CLI/Main.lean

@@ -395,7 +395,7 @@ protected def get : CliM PUnit := do
   if let some file := mappings? then liftM (m := LoggerIO) do
     if opts.platform?.isSome || opts.toolchain?.isSome then
       logWarning "the `--platform` and `--toolchain` options do nothing for `cache get` with a mappings file"
-      if .warning ≤ opts.failLv then
+      if opts.failLv ≤ .warning then
         failure
     let some remoteScope := opts.scope?
       | error "to use `cache get` with a mappings file, `--scope` or `--repo` must be set"
@@ -470,7 +470,7 @@ where
     if (← repo.hasDiff) then
       logWarning s!"{pkg.prettyName}: package has changes; \
         only artifacts for committed code will be downloaded"
-      if .warning ≤ opts.failLv then
+      if opts.failLv ≤ .warning then
         failure
     let n := opts.maxRevs
     let revs ← repo.getHeadRevisions n
@@ -505,7 +505,7 @@ protected def put : CliM PUnit := do
   if (← repo.hasDiff) then
     logWarning s!"{pkg.prettyName}: package has changes; \
       artifacts will be uploaded for the most recent commit"
-    if .warning ≤ opts.failLv then
+    if opts.failLv ≤ .warning then
       exit 1
   let rev ← repo.getHeadRevision
   let map ← CacheMap.load file

src/lake/Lake/CLI/Shake.lean

@@ -65,7 +65,7 @@ instance : Union Bitset where
 instance : XorOp Bitset where
   xor a b := { toNat := a.toNat ^^^ b.toNat }
 
-def has (s : Bitset) (i : Nat) : Bool := s ∩ {i} ≠ ∅
+def has (s : Bitset) (i : Nat) : Bool := s.toNat.testBit i
 
 end Bitset
 
@@ -166,8 +166,19 @@ structure State where
   /-- Edits to be applied to the module imports. -/
   edits : Edits := {}
 
+  -- Memoizations
+  reservedNames : Std.HashSet Name := Id.run do
+    let mut m := {}
+    for (c, _) in env.constants do
+      if isReservedName env c then
+        m := m.insert c
+    return m
+  indirectModUses : Std.HashMap Name (Array ModuleIdx) :=
+    indirectModUseExt.getState env
+  modNames : Array Name :=
+    env.header.moduleNames
+
 def State.mods (s : State) := s.env.header.moduleData
-def State.modNames (s : State) := s.env.header.moduleNames
 
 /--
 Given module `j`'s transitive dependencies, computes the union of `transImps` and the transitive
@@ -222,9 +233,9 @@ def isDeclMeta' (env : Environment) (declName : Name) : Bool :=
 Given an `Expr` reference, returns the declaration name that should be considered the reference, if
 any.
 -/
-def getDepConstName? (env : Environment) (ref : Name) : Option Name := do
+def getDepConstName? (s : State) (ref : Name) : Option Name := do
   -- Ignore references to reserved names, they can be re-generated in-place
-  guard <| !isReservedName env ref
+  guard <| !s.reservedNames.contains ref
   -- `_simp_...` constants are similar, use base decl instead
   return if ref.isStr && ref.getString!.startsWith "_simp_" then
     ref.getPrefix
@@ -257,12 +268,12 @@ where
     let env := s.env
     Lean.Expr.foldConsts e deps fun c deps => Id.run do
       let mut deps := deps
-      if let some c := getDepConstName? env c then
+      if let some c := getDepConstName? s c then
         if let some j := env.getModuleIdxFor? c then
           let k := { k with isMeta := k.isMeta && !isDeclMeta' env c }
           if j != i then
             deps := deps.union k {j}
-            for indMod in (indirectModUseExt.getState env)[c]?.getD #[] do
+            for indMod in s.indirectModUses[c]?.getD #[] do
               if s.transDeps[i]!.has k indMod then
                 deps := deps.union k {indMod}
       return deps
@@ -298,11 +309,11 @@ where
     let env := s.env
     Lean.Expr.foldConsts e deps fun c deps => Id.run do
       let mut deps := deps
-      if let some c := getDepConstName? env c then
+      if let some c := getDepConstName? s c then
         if let some j := env.getModuleIdxFor? c then
           let k := { k with isMeta := k.isMeta && !isDeclMeta' env c }
           deps := addExplanation j k name c deps
-        for indMod in (indirectModUseExt.getState env)[c]?.getD #[] do
+        for indMod in s.indirectModUses[c]?.getD #[] do
           if s.transDeps[i]!.has k indMod then
             deps := addExplanation indMod k name (`_indirect ++ c) deps
       return deps
@@ -636,7 +647,7 @@ public def run (args : Args) (h : 0 < args.mods.size)
   let imps := mods.map ({ module := · })
   let (_, s) ← importModulesCore imps (isExported := true) |>.run
   let s := s.markAllExported
-  let mut env ← finalizeImport s (isModule := true) imps {} (leakEnv := false) (loadExts := false)
+  let mut env ← finalizeImport s (isModule := true) imps {} (leakEnv := true) (loadExts := false)
   if env.header.moduleData.any (!·.isModule) then
     throw <| .userError "`lake shake` only works with `module`s currently"
   -- the one env ext we want to initialize

src/lake/Lake/Config/Cache.lean

@@ -13,6 +13,7 @@ import Lake.Build.Actions
 import Lake.Util.Url
 import Lake.Util.Proc
 import Lake.Util.Reservoir
+import Lake.Util.JsonObject
 import Lake.Util.IO
 import Init.Data.String.Search
 import Init.Data.String.Lemmas.Basic
@@ -305,15 +306,26 @@ end Cache
 def uploadS3
   (file : FilePath) (contentType : String) (url : String) (key : String)
 : LoggerIO Unit := do
-  proc {
+  let out ← captureProc' {
     cmd := "curl"
     args := #[
-      "-s",
+      "-s", "-w", "%{stderr}%{json}\n",
       "--aws-sigv4", "aws:amz:auto:s3", "--user", key,
       "-X", "PUT", "-T", file.toString, url,
       "-H",  s!"Content-Type: {contentType}"
     ]
-  } (quiet := true)
+  }
+  match Json.parse out.stderr >>= JsonObject.fromJson? with
+  | .ok data =>
+    let code ← id do
+      match (data.get? "response_code" <|> data.get? "http_code") with
+      | .ok (some code) => return code
+      | .ok none => error s!"curl's JSON output did not contain a response code"
+      | .error e => error s!"curl's JSON output contained an invalid JSON response code: {e}"
+    unless code == 200 do
+      error s!"failed to upload artifact, error {code}; received:\n{out.stdout}"
+  | .error e =>
+    error s!"curl produced invalid JSON output: {e}"
 
 /--
 Configuration of a remote cache service (e.g., Reservoir or an S3 bucket).

src/library/ir_interpreter.cpp

@@ -200,7 +200,6 @@ option_ref<decl> find_ir_decl_boxed(elab_environment const & env, name const & n
 extern "C" double lean_float_of_nat(lean_obj_arg a);
 extern "C" float lean_float32_of_nat(lean_obj_arg a);
 
-static string_ref * g_boxed_mangled_suffix = nullptr;
 static name * g_interpreter_prefer_native = nullptr;
 DEBUG_CODE(static name * g_interpreter_step = nullptr;)
 DEBUG_CODE(static name * g_interpreter_call = nullptr;)
@@ -216,6 +215,12 @@ string_ref get_symbol_stem(elab_environment const & env, name const & fn) {
     return string_ref(lean_get_symbol_stem(env.to_obj_arg(), fn.to_obj_arg()));
 }
 
+extern "C" obj_res lean_mk_mangled_boxed_name(obj_arg str);
+
+string_ref mk_mangled_boxed_name(string_ref const & str) {
+    return string_ref(lean_mk_mangled_boxed_name(str.to_obj_arg()));
+}
+
 extern "C" object * lean_ir_format_fn_body_head(object * b);
 std::string format_fn_body_head(fn_body const & b) {
     object_ref s(lean_ir_format_fn_body_head(b.to_obj_arg()));
@@ -843,7 +848,7 @@ private:
         symbol_cache_entry e_new { get_decl(fn), {nullptr, false} };
         if (m_prefer_native || decl_tag(e_new.m_decl) == decl_kind::Extern || has_init_attribute(m_env, fn)) {
             string_ref mangled = get_symbol_stem(m_env, fn);
-            string_ref boxed_mangled(string_append(mangled.to_obj_arg(), g_boxed_mangled_suffix->raw()));
+            string_ref boxed_mangled = mk_mangled_boxed_name(mangled);
             // check for boxed version first
             if (void *p_boxed = lookup_symbol_in_cur_exe(boxed_mangled.data())) {
                 e_new.m_native.m_addr = p_boxed;
@@ -965,7 +970,7 @@ private:
         } else {
             if (decl_tag(e.m_decl) == decl_kind::Extern) {
                 string_ref mangled = get_symbol_stem(m_env, fn);
-                string_ref boxed_mangled(string_append(mangled.to_obj_arg(), g_boxed_mangled_suffix->raw()));
+                string_ref boxed_mangled = mk_mangled_boxed_name(mangled);
                 throw exception(sstream() << "Could not find native implementation of external declaration '" << fn
                                           << "' (symbols '" << boxed_mangled.data() << "' or '" << mangled.data() << "').\n"
                                           << "For declarations from `Init`, `Std`, or `Lean`, you need to set `supportInterpreter := true` "
@@ -1212,8 +1217,6 @@ extern "C" LEAN_EXPORT object * lean_run_init(object * env, object * opts, objec
 }
 
 void initialize_ir_interpreter() {
-    ir::g_boxed_mangled_suffix = new string_ref("___boxed");
-    mark_persistent(ir::g_boxed_mangled_suffix->raw());
     ir::g_interpreter_prefer_native = new name({"interpreter", "prefer_native"});
     ir::g_init_globals = new name_hash_map<object *>();
     register_bool_option(*ir::g_interpreter_prefer_native, LEAN_DEFAULT_INTERPRETER_PREFER_NATIVE, "(interpreter) whether to use precompiled code where available");
@@ -1236,6 +1239,5 @@ void finalize_ir_interpreter() {
     });
     delete ir::g_init_globals;
     delete ir::g_interpreter_prefer_native;
-    delete ir::g_boxed_mangled_suffix;
 }
 }