fix zero sized chunks

Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>

.github/workflows/ci.yml

@@ -279,8 +279,7 @@ jobs:
                 "os": large ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "enabled": true,
                 "check-rebootstrap": level >= 1,
-                // Done as part of test-bench
-                //"check-stage3": level >= 2,
+                "check-stage3": level >= 2,
                 "test": true,
                 // NOTE: `test-bench` currently seems to be broken on `ubuntu-latest`
                 "test-bench": large && level >= 2,
@@ -292,8 +291,7 @@ jobs:
                 "os": large ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "enabled": true,
                 "check-rebootstrap": level >= 1,
-                // Done as part of test-bench
-                //"check-stage3": level >= 2,
+                "check-stage3": level >= 2,
                 "test": true,
                 "secondary": true,
                 // NOTE: `test-bench` currently seems to be broken on `ubuntu-latest`

AGENTS.md

@@ -1 +0,0 @@
-.claude/CLAUDE.md

src/Init/Data/Nat/Basic.lean

@@ -59,9 +59,9 @@ Examples:
 * `Nat.repeat f 3 a = f <| f <| f <| a`
 * `Nat.repeat (· ++ "!") 4 "Hello" = "Hello!!!!"`
 -/
-@[specialize, expose] def «repeat» {α : Type u} (f : α → α) : (n : Nat) → (a : α) → α
+@[specialize, expose] def repeat {α : Type u} (f : α → α) : (n : Nat) → (a : α) → α
   | 0,      a => a
-  | succ n, a => f («repeat» f n a)
+  | succ n, a => f (repeat f n a)
 
 /--
 Applies a function to a starting value the specified number of times.
@@ -1221,9 +1221,9 @@ theorem not_lt_eq (a b : Nat) : (¬ (a < b)) = (b ≤ a) :=
 theorem not_gt_eq (a b : Nat) : (¬ (a > b)) = (a ≤ b) :=
   not_lt_eq b a
 
-@[csimp] theorem repeat_eq_repeatTR : @«repeat» = @repeatTR :=
+@[csimp] theorem repeat_eq_repeatTR : @repeat = @repeatTR :=
   funext fun α => funext fun f => funext fun n => funext fun init =>
-  let rec go : ∀ m n, repeatTR.loop f m («repeat» f n init) = «repeat» f (m + n) init
+  let rec go : ∀ m n, repeatTR.loop f m (repeat f n init) = repeat f (m + n) init
     | 0,      n => by simp [repeatTR.loop]
     | succ m, n => by rw [repeatTR.loop, succ_add]; exact go m (succ n)
   (go n 0).symm

src/Init/Data/Order/LemmasExtra.lean

@@ -87,7 +87,7 @@ public theorem IsLinearOrder.of_ord {α : Type u} [LE α] [Ord α] [LawfulOrderO
 /--
 This lemma derives a `LawfulOrderLT α` instance from a property involving an `Ord α` instance.
 -/
-public theorem LawfulOrderLT.of_ord (α : Type u) [Ord α] [LT α] [LE α] [LawfulOrderOrd α]
+public instance LawfulOrderLT.of_ord (α : Type u) [Ord α] [LT α] [LE α] [LawfulOrderOrd α]
     (lt_iff_compare_eq_lt : ∀ a b : α, a < b ↔ compare a b = .lt) :
     LawfulOrderLT α where
   lt_iff a b := by
@@ -96,7 +96,7 @@ public theorem LawfulOrderLT.of_ord (α : Type u) [Ord α] [LT α] [LE α] [Lawf
 /--
 This lemma derives a `LawfulOrderBEq α` instance from a property involving an `Ord α` instance.
 -/
-public theorem LawfulOrderBEq.of_ord (α : Type u) [Ord α] [BEq α] [LE α] [LawfulOrderOrd α]
+public instance LawfulOrderBEq.of_ord (α : Type u) [Ord α] [BEq α] [LE α] [LawfulOrderOrd α]
     (beq_iff_compare_eq_eq : ∀ a b : α, a == b ↔ compare a b = .eq) :
     LawfulOrderBEq α where
   beq_iff_le_and_ge := by
@@ -105,7 +105,7 @@ public theorem LawfulOrderBEq.of_ord (α : Type u) [Ord α] [BEq α] [LE α] [La
 /--
 This lemma derives a `LawfulOrderInf α` instance from a property involving an `Ord α` instance.
 -/
-public theorem LawfulOrderInf.of_ord (α : Type u) [Ord α] [Min α] [LE α] [LawfulOrderOrd α]
+public instance LawfulOrderInf.of_ord (α : Type u) [Ord α] [Min α] [LE α] [LawfulOrderOrd α]
     (compare_min_isLE_iff : ∀ a b c : α,
         (compare a (min b c)).isLE ↔ (compare a b).isLE ∧ (compare a c).isLE) :
     LawfulOrderInf α where
@@ -114,7 +114,7 @@ public theorem LawfulOrderInf.of_ord (α : Type u) [Ord α] [Min α] [LE α] [La
 /--
 This lemma derives a `LawfulOrderMin α` instance from a property involving an `Ord α` instance.
 -/
-public theorem LawfulOrderMin.of_ord (α : Type u) [Ord α] [Min α] [LE α] [LawfulOrderOrd α]
+public instance LawfulOrderMin.of_ord (α : Type u) [Ord α] [Min α] [LE α] [LawfulOrderOrd α]
     (compare_min_isLE_iff : ∀ a b c : α,
         (compare a (min b c)).isLE ↔ (compare a b).isLE ∧ (compare a c).isLE)
     (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b) :
@@ -125,7 +125,7 @@ public theorem LawfulOrderMin.of_ord (α : Type u) [Ord α] [Min α] [LE α] [La
 /--
 This lemma derives a `LawfulOrderSup α` instance from a property involving an `Ord α` instance.
 -/
-public theorem LawfulOrderSup.of_ord (α : Type u) [Ord α] [Max α] [LE α] [LawfulOrderOrd α]
+public instance LawfulOrderSup.of_ord (α : Type u) [Ord α] [Max α] [LE α] [LawfulOrderOrd α]
     (compare_max_isLE_iff : ∀ a b c : α,
         (compare (max a b) c).isLE ↔ (compare a c).isLE ∧ (compare b c).isLE) :
     LawfulOrderSup α where
@@ -134,7 +134,7 @@ public theorem LawfulOrderSup.of_ord (α : Type u) [Ord α] [Max α] [LE α] [La
 /--
 This lemma derives a `LawfulOrderMax α` instance from a property involving an `Ord α` instance.
 -/
-public theorem LawfulOrderMax.of_ord (α : Type u) [Ord α] [Max α] [LE α] [LawfulOrderOrd α]
+public instance LawfulOrderMax.of_ord (α : Type u) [Ord α] [Max α] [LE α] [LawfulOrderOrd α]
     (compare_max_isLE_iff : ∀ a b c : α,
         (compare (max a b) c).isLE ↔ (compare a c).isLE ∧ (compare b c).isLE)
     (max_eq_or : ∀ a b : α, max a b = a ∨ max a b = b) :

src/Init/Grind/Order.lean

@@ -75,9 +75,6 @@ theorem nat_eq (a b : Nat) (x y : Int) : NatCast.natCast a = x → NatCast.natCa
 theorem of_nat_eq (a b : Nat) (x y : Int) : NatCast.natCast a = x → NatCast.natCast b = y → a = b → x = y := by
   intro _ _; subst x y; intro; simp [*]
 
-theorem of_natCast_eq {α : Type u} [NatCast α] (a b : Nat) (x y : α) : NatCast.natCast a = x → NatCast.natCast b = y → a = b → x = y := by
-  intro h₁ h₂ h; subst h; exact h₁.symm.trans h₂
-
 theorem le_of_not_le {α} [LE α] [Std.IsLinearPreorder α]
     {a b : α} : ¬ a ≤ b → b ≤ a := by
   intro h

src/Init/While.lean

@@ -10,15 +10,13 @@ public import Init.Core
 
 public section
 
+/-!
+# Notation for `while` and `repeat` loops.
+-/
+
 namespace Lean
 
-/-!
-# `Loop` type backing `repeat`/`while`/`repeat ... until`
-
-The parsers and elaborators for `repeat`, `while`, and `repeat ... until` live in
-`Lean.Parser.Do` and `Lean.Elab.BuiltinDo.Repeat`. This module only provides the
-`Loop` type (and `ForIn` instance) that those elaborators expand to.
--/
+/-! # `repeat` and `while` notation -/
 
 inductive Loop where
   | mk
@@ -34,4 +32,26 @@ partial def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] (_ : Loop
 instance [Monad m] : ForIn m Loop Unit where
   forIn := Loop.forIn
 
+syntax "repeat " doSeq : doElem
+
+macro_rules
+  | `(doElem| repeat%$tk $seq) => `(doElem| for%$tk _ in Loop.mk do $seq)
+
+syntax "while " ident " : " termBeforeDo " do " doSeq : doElem
+
+macro_rules
+  | `(doElem| while%$tk $h : $cond do $seq) =>
+    `(doElem| repeat%$tk if $h:ident : $cond then $seq else break)
+
+syntax "while " termBeforeDo " do " doSeq : doElem
+
+macro_rules
+  | `(doElem| while%$tk $cond do $seq) => `(doElem| repeat%$tk if $cond then $seq else break)
+
+syntax "repeat " doSeq ppDedent(ppLine) "until " term : doElem
+
+macro_rules
+  | `(doElem| repeat%$tk $seq until $cond) =>
+    `(doElem| repeat%$tk do $seq:doSeq; if $cond then break)
+
 end Lean

src/Lean/Compiler/LCNF/EmitC.lean

@@ -207,7 +207,7 @@ def emitLns [EmitToString α] (as : List α) : EmitM Unit :=
   emitLn "}"
   return ret
 
-def toDigit (c : Nat) : String :=
+def toHexDigit (c : Nat) : String :=
   String.singleton c.digitChar
 
 def quoteString (s : String) : String :=
@@ -221,11 +221,7 @@ def quoteString (s : String) : String :=
       else if c == '\"' then "\\\""
       else if c == '?' then "\\?" -- avoid trigraphs
       else if c.toNat <= 31 then
-        -- Use octal escapes instead of hex escapes because C hex escapes are
-        -- greedy: "\x01abc" would be parsed as the single escape \x01abc rather
-        -- than \x01 followed by "abc".  Octal escapes consume at most 3 digits.
-        let n := c.toNat
-        "\\" ++ toDigit (n / 64) ++ toDigit ((n / 8) % 8) ++ toDigit (n % 8)
+        "\\x" ++ toHexDigit (c.toNat / 16) ++ toHexDigit (c.toNat % 16)
       -- TODO(Leo): we should use `\unnnn` for escaping unicode characters.
       else String.singleton c)
     q;

src/Lean/Data/Lsp/Capabilities.lean

@@ -64,12 +64,6 @@ structure WorkspaceClientCapabilities where
   deriving ToJson, FromJson
 
 structure LeanClientCapabilities where
-  /--
-  Whether the client supports incremental `textDocument/publishDiagnostics` updates.
-  If `none` or `false`, the server will never set `PublishDiagnosticsParams.isIncremental?`
-  and always report full diagnostic updates that replace the previous one.
-  -/
-  incrementalDiagnosticSupport? : Option Bool := none
   /--
   Whether the client supports `DiagnosticWith.isSilent = true`.
   If `none` or `false`, silent diagnostics will not be served to the client.
@@ -90,13 +84,6 @@ structure ClientCapabilities where
   lean?         : Option LeanClientCapabilities         := none
   deriving ToJson, FromJson
 
-def ClientCapabilities.incrementalDiagnosticSupport (c : ClientCapabilities) : Bool := Id.run do
-  let some lean := c.lean?
-    | return false
-  let some incrementalDiagnosticSupport := lean.incrementalDiagnosticSupport?
-    | return false
-  return incrementalDiagnosticSupport
-
 def ClientCapabilities.silentDiagnosticSupport (c : ClientCapabilities) : Bool := Id.run do
   let some lean := c.lean?
     | return false

src/Lean/Data/Lsp/Diagnostics.lean

@@ -159,14 +159,6 @@ abbrev Diagnostic := DiagnosticWith String
 structure PublishDiagnosticsParams where
   uri : DocumentUri
   version? : Option Int := none
-  /--
-  Whether the client should append this set of diagnostics to the previous set
-  rather than replacing the previous set by this one (the default LSP behavior).
-  `false` means the client should replace.
-  `none` is equivalent to `false`.
-  This is a Lean-specific extension (see `LeanClientCapabilities`).
-  -/
-  isIncremental? : Option Bool := none
   diagnostics : Array Diagnostic
   deriving Inhabited, BEq, ToJson, FromJson
 

src/Lean/Data/Lsp/Ipc.lean

@@ -102,32 +102,9 @@ def normalizePublishDiagnosticsParams (p : PublishDiagnosticsParams) :
     sorted.toArray
 }
 
-/--
-Merges a new `textDocument/publishDiagnostics` notification into a previously accumulated one.
-
-- If there is no previous notification, the new one is used as-is.
-- If `isIncremental?` is `true`, the new diagnostics are appended.
-- Otherwise the new notification replaces the previous one.
-
-The returned params always have `isIncremental? := some false` since they represent the full
-accumulated set.
--/
-def mergePublishDiagnosticsParams (prev? : Option PublishDiagnosticsParams)
-    (next : PublishDiagnosticsParams) : PublishDiagnosticsParams := Id.run do
-  let replace := { next with isIncremental? := some false }
-  let some prev := prev?
-    | return replace
-  if next.isIncremental?.getD false then
-    return { next with
-      diagnostics := prev.diagnostics ++ next.diagnostics
-      isIncremental? := some false }
-  return replace
-
 /--
 Waits for the worker to emit all diagnostic notifications for the current document version and
-returns the accumulated diagnostics, if any.
-
-Incoming notifications are merged using `mergePublishDiagnosticsParams`.
+returns the last notification, if any.
 
 We used to return all notifications but with debouncing in the server, this would not be
 deterministic anymore as what messages are dropped depends on wall-clock timing.
@@ -135,25 +112,22 @@ deterministic anymore as what messages are dropped depends on wall-clock timing.
 partial def collectDiagnostics (waitForDiagnosticsId : RequestID := 0) (target : DocumentUri) (version : Nat)
 : IpcM (Option (Notification PublishDiagnosticsParams)) := do
   writeRequest ⟨waitForDiagnosticsId, "textDocument/waitForDiagnostics", WaitForDiagnosticsParams.mk target version⟩
-  loop none
+  loop
 where
-  loop (accumulated? : Option PublishDiagnosticsParams) := do
+  loop := do
     match (←readMessage) with
     | Message.response id _ =>
-      if id == waitForDiagnosticsId then
-        return accumulated?.map fun p =>
-          ⟨"textDocument/publishDiagnostics", normalizePublishDiagnosticsParams p⟩
-      else loop accumulated?
-    | Message.responseError id _ msg _ =>
+      if id == waitForDiagnosticsId then return none
+      else loop
+    | Message.responseError id _    msg _ =>
       if id == waitForDiagnosticsId then
         throw $ userError s!"Waiting for diagnostics failed: {msg}"
-      else loop accumulated?
+      else loop
     | Message.notification "textDocument/publishDiagnostics" (some param) =>
       match fromJson? (toJson param) with
-      | Except.ok (diagnosticParam : PublishDiagnosticsParams) =>
-        loop (some (mergePublishDiagnosticsParams accumulated? diagnosticParam))
+      | Except.ok diagnosticParam => return (← loop).getD ⟨"textDocument/publishDiagnostics", normalizePublishDiagnosticsParams diagnosticParam⟩
       | Except.error inner => throw $ userError s!"Cannot decode publishDiagnostics parameters\n{inner}"
-    | _ => loop accumulated?
+    | _ => loop
 
 partial def waitForILeans (waitForILeansId : RequestID := 0) (target : DocumentUri) (version : Nat) : IpcM Unit := do
   writeRequest ⟨waitForILeansId, "$/lean/waitForILeans", WaitForILeansParams.mk target version⟩

src/Lean/DocString/Extension.lean

@@ -289,11 +289,9 @@ instance : ToMarkdown VersoModuleDocs.Snippet where
 
 structure VersoModuleDocs where
   snippets : PersistentArray VersoModuleDocs.Snippet := {}
+  terminalNesting : Option Nat := snippets.findSomeRev? (·.terminalNesting)
 deriving Inhabited
 
-def VersoModuleDocs.terminalNesting : VersoModuleDocs → Option Nat
-  | VersoModuleDocs.mk snippets => snippets.findSomeRev? (·.terminalNesting)
-
 instance : Repr VersoModuleDocs where
   reprPrec v _ :=
     .group <| .nest 2 <|
@@ -316,7 +314,10 @@ def add (docs : VersoModuleDocs) (snippet : Snippet) : Except String VersoModule
   unless docs.canAdd snippet do
     throw "Can't nest this snippet here"
 
-  return { docs with snippets := docs.snippets.push snippet }
+  return { docs with
+    snippets := docs.snippets.push snippet,
+    terminalNesting := snippet.terminalNesting
+  }
 
 def add! (docs : VersoModuleDocs) (snippet : Snippet) : VersoModuleDocs :=
   let ok :=
@@ -326,7 +327,10 @@ def add! (docs : VersoModuleDocs) (snippet : Snippet) : VersoModuleDocs :=
   if not ok then
     panic! "Can't nest this snippet here"
   else
-    { docs with snippets := docs.snippets.push snippet }
+    { docs with
+      snippets := docs.snippets.push snippet,
+      terminalNesting := snippet.terminalNesting
+    }
 
 
 private structure DocFrame where

src/Lean/Elab/BuiltinDo.lean

@@ -15,4 +15,3 @@ public import Lean.Elab.BuiltinDo.Jump
 public import Lean.Elab.BuiltinDo.Misc
 public import Lean.Elab.BuiltinDo.For
 public import Lean.Elab.BuiltinDo.TryCatch
-public import Lean.Elab.BuiltinDo.Repeat

src/Lean/Elab/BuiltinDo/Repeat.lean

@@ -1,44 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Graf
--/
-module
-
-prelude
-public import Lean.Elab.BuiltinDo.Basic
-meta import Lean.Parser.Do
-import Lean.Elab.BuiltinDo.For
-
-public section
-
-namespace Lean.Elab.Do
-
-open Lean.Parser.Term
-
-/--
-Builtin do-element elaborator for `repeat` (syntax kind `Lean.Parser.Term.doRepeat`).
-
-Expands to `for _ in Loop.mk do ...`. A follow-up change will extend this
-elaborator to choose between `Loop.mk` and a well-founded `Repeat.mk` based on a
-configuration option.
--/
-@[builtin_doElem_elab Lean.Parser.Term.doRepeat] def elabDoRepeat : DoElab := fun stx dec => do
-  let `(doElem| repeat%$tk $seq) := stx | throwUnsupportedSyntax
-  let expanded ← `(doElem| for%$tk _ in Loop.mk do $seq)
-  Term.withMacroExpansion stx expanded <|
-    withRef expanded <| elabDoElem ⟨expanded⟩ dec
-
-@[builtin_macro Lean.Parser.Term.doWhileH] def expandDoWhileH : Macro
-  | `(doElem| while%$tk $h : $cond do $seq) => `(doElem| repeat%$tk if $h:ident : $cond then $seq else break)
-  | _ => Macro.throwUnsupported
-
-@[builtin_macro Lean.Parser.Term.doWhile] def expandDoWhile : Macro
-  | `(doElem| while%$tk $cond do $seq) => `(doElem| repeat%$tk if $cond then $seq else break)
-  | _ => Macro.throwUnsupported
-
-@[builtin_macro Lean.Parser.Term.doRepeatUntil] def expandDoRepeatUntil : Macro
-  | `(doElem| repeat%$tk $seq until $cond) => `(doElem| repeat%$tk do $seq:doSeq; if $cond then break)
-  | _ => Macro.throwUnsupported
-
-end Lean.Elab.Do

src/Lean/Elab/Do/Basic.lean

@@ -587,7 +587,7 @@ def DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : Control
     withLocalDeclD nondupDec.resultName nondupDec.resultType fun r => do
     withLocalDeclsDND (mutDecls.map fun (d : LocalDecl) => (d.userName, d.type)) fun muts => do
     for (x, newX) in mutVars.zip muts do Term.addTermInfo' x newX
-    withDeadCode (if callerInfo.deadCode then .deadSemantically else .alive) do
+    withDeadCode (if callerInfo.numRegularExits > 0 then .alive else .deadSemantically) do
     let e ← nondupDec.k
     mkLambdaFVars (#[r] ++ muts) e
   unless ← joinRhsMVar.mvarId!.checkedAssign joinRhs do

src/Lean/Elab/Do/Control.lean

@@ -232,8 +232,9 @@ def ControlLifter.ofCont (info : ControlInfo) (dec : DoElemCont) : DoElabM Contr
     breakBase?,
     continueBase?,
     pureBase := controlStack,
-    -- The success continuation `origCont` is dead code iff the `ControlInfo` says so semantically.
-    pureDeadCode := if info.deadCode then .deadSemantically else .alive,
+    -- The success continuation `origCont` is dead code iff the `ControlInfo` says that there is no
+    -- regular exit.
+    pureDeadCode := if info.numRegularExits > 0 then .alive else .deadSemantically,
     liftedDoBlockResultType := (← controlStack.stM dec.resultType),
   }
 

src/Lean/Elab/Do/InferControlInfo.lean

@@ -16,77 +16,46 @@ namespace Lean.Elab.Do
 
 open Lean Meta Parser.Term
 
-/--
-Represents information about what control effects a `do` block has.
-
-The fields split by flavor:
-
-* `breaks`, `continues`, `returnsEarly`, and `reassigns` are **syntactic**: `true`/non-empty iff
-  the corresponding construct appears anywhere in the source text of the block, independent of
-  whether it is semantically reachable. Downstream elaborators must assume every such syntactic
-  effect may occur, because the elaborator visits every doElem (only top-level
-  `return`/`break`/`continue` short-circuit via `elabAsSyntacticallyDeadCode`).
-* `numRegularExits` is also **syntactic**: the number of times the block wires the enclosing
-  continuation into its elaborated expression. `withDuplicableCont` reads it as a join-point
-  duplication trigger (`> 1`).
-* `deadCode` is **semantic**: a conservative over-approximation of "every path through the block
-  fails to reach the end normally". It drives the dead-code warning.
-
-Invariant: `numRegularExits = 0 → deadCode = true`. The converse does not hold — for example a
-`repeat` with no `break` has `numRegularExits = 1` (the loop elaborator wires its continuation
-once for the normal-exit path) but `deadCode = true` (the loop never terminates normally).
--/
+/-- Represents information about what control effects a `do` block has. -/
 structure ControlInfo where
-  /-- The `do` block syntactically contains a `break`. -/
+  /-- The `do` block may `break`. -/
   breaks : Bool := false
-  /-- The `do` block syntactically contains a `continue`. -/
+  /-- The `do` block may `continue`. -/
   continues : Bool := false
-  /-- The `do` block syntactically contains an early `return`. -/
+  /-- The `do` block may `return` early. -/
   returnsEarly : Bool := false
   /--
-  The number of times the block wires the enclosing continuation into its elaborated expression.
-  Consumed by `withDuplicableCont` to decide whether to introduce a join point (`> 1`).
+  The number of regular exit paths the `do` block has.
+  Corresponds to the number of jumps to an ambient join point.
   -/
   numRegularExits : Nat := 1
-  /--
-  Conservative semantic flag: `true` iff every path through the block provably fails to reach the
-  end normally. Implied by `numRegularExits = 0`, but not equivalent (e.g. a `repeat` without
-  `break` has `numRegularExits = 1` yet is dead).
-  -/
-  deadCode : Bool := false
-  /-- The variables that are syntactically reassigned somewhere in the `do` block. -/
+  /-- The variables that are reassigned in the `do` block. -/
   reassigns : NameSet := {}
   deriving Inhabited
 
 def ControlInfo.pure : ControlInfo := {}
 
-def ControlInfo.sequence (a b : ControlInfo) : ControlInfo := {
-    -- Syntactic fields aggregate unconditionally; the elaborator keeps visiting `b` unless `a` is
-    -- a syntactically-terminal element (only top-level `return`/`break`/`continue` are, via
-    -- `elabAsSyntacticallyDeadCode`).
+def ControlInfo.sequence (a b : ControlInfo) : ControlInfo :=
+  if a.numRegularExits == 0 then a else {
     breaks := a.breaks || b.breaks,
     continues := a.continues || b.continues,
     returnsEarly := a.returnsEarly || b.returnsEarly,
-    reassigns := a.reassigns ++ b.reassigns,
     numRegularExits := b.numRegularExits,
-    -- Semantic: the sequence is dead if either part is dead.
-    deadCode := a.deadCode || b.deadCode,
+    reassigns := a.reassigns ++ b.reassigns,
   }
 
 def ControlInfo.alternative (a b : ControlInfo) : ControlInfo := {
     breaks := a.breaks || b.breaks,
     continues := a.continues || b.continues,
     returnsEarly := a.returnsEarly || b.returnsEarly,
-    reassigns := a.reassigns ++ b.reassigns,
     numRegularExits := a.numRegularExits + b.numRegularExits,
-    -- Semantic: alternatives are dead only if all branches are dead.
-    deadCode := a.deadCode && b.deadCode,
+    reassigns := a.reassigns ++ b.reassigns,
   }
 
 instance : ToMessageData ControlInfo where
   toMessageData info := m!"breaks: {info.breaks}, continues: {info.continues},
-    returnsEarly: {info.returnsEarly}, numRegularExits: {info.numRegularExits},
-    deadCode: {info.deadCode}, reassigns: {info.reassigns.toList}"
+    returnsEarly: {info.returnsEarly}, exitsRegularly: {info.numRegularExits},
+    reassigns: {info.reassigns.toList}"
 
 /-- A handler for inferring `ControlInfo` from a `doElem` syntax. Register with `@[doElem_control_info parserName]`. -/
 abbrev ControlInfoHandler := TSyntax `doElem → TermElabM ControlInfo
@@ -120,9 +89,9 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
     return ← ofElem ⟨stxNew⟩
 
   match stx with
-  | `(doElem| break) => return { breaks := true, numRegularExits := 0, deadCode := true }
-  | `(doElem| continue) => return { continues := true, numRegularExits := 0, deadCode := true }
-  | `(doElem| return $[$_]?) => return { returnsEarly := true, numRegularExits := 0, deadCode := true }
+  | `(doElem| break) => return { breaks := true, numRegularExits := 0 }
+  | `(doElem| continue) => return { continues := true, numRegularExits := 0 }
+  | `(doElem| return $[$_]?) => return { returnsEarly := true, numRegularExits := 0 }
   | `(doExpr| $_:term) => return { numRegularExits := 1 }
   | `(doElem| do $doSeq) => ofSeq doSeq
   -- Let
@@ -160,24 +129,12 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
     return thenInfo.alternative info
   | `(doElem| unless $_ do $elseSeq) =>
     ControlInfo.alternative {} <$> ofSeq elseSeq
-  -- For/Repeat
   | `(doElem| for $[$[$_ :]? $_ in $_],* do $bodySeq) =>
     let info ← ofSeq bodySeq
     return { info with  -- keep only reassigns and earlyReturn
       numRegularExits := 1,
       continues := false,
-      breaks := false,
-      deadCode := false,
-    }
-  | `(doRepeat| repeat $bodySeq) =>
-    let info ← ofSeq bodySeq
-    return { info with
-      -- Syntactically the loop elaborator wires the continuation once (for the break path).
-      numRegularExits := 1,
-      continues := false,
-      breaks := false,
-      -- Semantically the loop never terminates normally unless the body may `break`.
-      deadCode := !info.breaks,
+      breaks := false
     }
   -- Try
   | `(doElem| try $trySeq:doSeq $[$catches]* $[finally $finSeq?]?) =>
@@ -247,7 +204,17 @@ partial def ofLetOrReassign (reassigned : Array Ident) (rhs? : Option (TSyntax `
 partial def ofSeq (stx : TSyntax ``doSeq) : TermElabM ControlInfo := do
   let mut info : ControlInfo := {}
   for elem in getDoElems stx do
-    info := info.sequence (← ofElem elem)
+    if info.numRegularExits == 0 then
+      break
+    let elemInfo ← ofElem elem
+    info := {
+      info with
+      breaks := info.breaks || elemInfo.breaks
+      continues := info.continues || elemInfo.continues
+      returnsEarly := info.returnsEarly || elemInfo.returnsEarly
+      numRegularExits := elemInfo.numRegularExits
+      reassigns := info.reassigns ++ elemInfo.reassigns
+    }
   return info
 
 partial def ofOptionSeq (stx? : Option (TSyntax ``doSeq)) : TermElabM ControlInfo := do

src/Lean/Elab/Do/Legacy.lean

@@ -1782,10 +1782,6 @@ mutual
             doIfToCode doElem doElems
           else if k == ``Parser.Term.doUnless then
             doUnlessToCode doElem doElems
-          else if k == ``Parser.Term.doRepeat then
-            let seq := doElem[1]
-            let expanded ← `(doElem| for _ in Loop.mk do $seq)
-            doSeqToCode (expanded :: doElems)
           else if k == ``Parser.Term.doFor then withFreshMacroScope do
             doForToCode doElem doElems
           else if k == ``Parser.Term.doMatch then

src/Lean/Elab/PreDefinition/Basic.lean

@@ -222,8 +222,8 @@ private def addNonRecAux (docCtx : LocalContext × LocalInstances) (preDef : Pre
     if compile && shouldGenCodeFor preDef then
       compileDecl decl
     if applyAttrAfterCompilation then
-      saveEqnAffectingOptions preDef.declName
       enableRealizationsForConst preDef.declName
+      generateEagerEqns preDef.declName
     addPreDefDocs docCtx preDef
     if applyAttrAfterCompilation then
       applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation

src/Lean/Elab/PreDefinition/EqUnfold.lean

@@ -28,7 +28,7 @@ def getConstUnfoldEqnFor? (declName : Name) : MetaM (Option Name) := do
     trace[ReservedNameAction] "getConstUnfoldEqnFor? {declName} failed, no unfold theorem available"
     return none
   let name := mkEqLikeNameFor (← getEnv) declName eqUnfoldThmSuffix
-  realizeConst declName name <| withEqnOptions declName do
+  realizeConst declName name do
     -- we have to call `getUnfoldEqnFor?` again to make `unfoldEqnName` available in this context
     let some unfoldEqnName ← getUnfoldEqnFor? (nonRec := true) declName | unreachable!
     let info ← getConstInfo unfoldEqnName

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -367,7 +367,7 @@ def mkEqns (declName : Name) (declNames : Array Name) : MetaM (Array Name) := do
     thmNames := thmNames.push name
     -- determinism: `type` should be independent of the environment changes since `baseName` was
     -- added
-    realizeConst declName name (withEqnOptions declName (doRealize name info type))
+    realizeConst declName name (doRealize name info type)
   return thmNames
 where
   doRealize name info type := withOptions (tactic.hygienic.set · false) do

src/Lean/Elab/PreDefinition/Mutual.lean

@@ -69,10 +69,8 @@ def addPreDefAttributes (preDefs : Array PreDefinition) : TermElabM Unit := do
           a.name = `instance_reducible || a.name = `implicit_reducible do
         setIrreducibleAttribute preDef.declName
 
-  for preDef in preDefs do
-    saveEqnAffectingOptions preDef.declName
-
   /-
+  `enableRealizationsForConst` must happen before `generateEagerEqns`
   It must happen in reverse order so that constants realized as part of the first decl
   have realizations for the other ones enabled
   -/
@@ -80,6 +78,7 @@ def addPreDefAttributes (preDefs : Array PreDefinition) : TermElabM Unit := do
     enableRealizationsForConst preDef.declName
 
   for preDef in preDefs do
+    generateEagerEqns preDef.declName
     applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
 
 end Lean.Elab.Mutual

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

@@ -163,7 +163,7 @@ public def registerEqnsInfo (preDef : PreDefinition) (declNames : Array Name) (r
 /-- Generate the "unfold" lemma for `declName`. -/
 def mkUnfoldEq (declName : Name) (info : EqnInfo) : MetaM Name := do
   let name := mkEqLikeNameFor (← getEnv) info.declName unfoldThmSuffix
-  realizeConst info.declNames[0]! name (withEqnOptions declName (doRealize name))
+  realizeConst info.declNames[0]! name (doRealize name)
   return name
 where
   doRealize name := withOptions (tactic.hygienic.set · false) do

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

@@ -208,11 +208,11 @@ def structuralRecursion
         -/
         registerEqnsInfo preDef (preDefs.map (·.declName)) recArgPos fixedParamPerms
     addSmartUnfoldingDef docCtx preDef recArgPos
-  for preDef in preDefs do
-    saveEqnAffectingOptions preDef.declName
   for preDef in preDefs do
     -- must happen in separate loop so realizations can see eqnInfos of all other preDefs
     enableRealizationsForConst preDef.declName
+    -- must happen after `enableRealizationsForConst`
+    generateEagerEqns preDef.declName
   applyAttributesOf preDefsNonRec AttributeApplicationTime.afterCompilation
 
 

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -497,21 +497,14 @@ def forEachVar (hs : Array Syntax) (tac : MVarId → FVarId → MetaM MVarId) :
 /--
   Searches for a metavariable `g` s.t. `tag` is its exact name.
   If none then searches for a metavariable `g` s.t. `tag` is a suffix of its name.
-  If none, then it searches for a metavariable `g` s.t. `tag` is a prefix of its name.
-
-  We erase macro scopes from the metavariable's user name before comparing, so that
-  user-written tags match even when a previous tactic left hygienic macro scopes at
-  the end of the tag (e.g. `e_a.yield._@._internal._hyg.0`, where `yield` is not the
-  literal last component of the name). Case tags written by the user are never
-  macro-scoped, so erasing scopes on the mvar side is sufficient.
--/
+  If none, then it searches for a metavariable `g` s.t. `tag` is a prefix of its name. -/
 private def findTag? (mvarIds : List MVarId) (tag : Name) : TacticM (Option MVarId) := do
-  match (← mvarIds.findM? fun mvarId => return tag == (← mvarId.getDecl).userName.eraseMacroScopes) with
+  match (← mvarIds.findM? fun mvarId => return tag == (← mvarId.getDecl).userName) with
   | some mvarId => return mvarId
   | none =>
-  match (← mvarIds.findM? fun mvarId => return tag.isSuffixOf (← mvarId.getDecl).userName.eraseMacroScopes) with
+  match (← mvarIds.findM? fun mvarId => return tag.isSuffixOf (← mvarId.getDecl).userName) with
   | some mvarId => return mvarId
-  | none => mvarIds.findM? fun mvarId => return tag.isPrefixOf (← mvarId.getDecl).userName.eraseMacroScopes
+  | none => mvarIds.findM? fun mvarId => return tag.isPrefixOf (← mvarId.getDecl).userName
 
 private def getCaseGoals (tag : TSyntax ``binderIdent) : TacticM (MVarId × List MVarId) := do
   let gs ← getUnsolvedGoals

src/Lean/Elab/Tactic/Grind/Basic.lean

@@ -68,10 +68,7 @@ def setGoals (goals : List Goal) : GrindTacticM Unit :=
 
 def pruneSolvedGoals : GrindTacticM Unit := do
   let gs ← getGoals
-  let gs ← gs.filterM fun g => do
-    if g.inconsistent then return false
-    -- The metavariable may have been assigned by `isDefEq`
-    return !(← g.mvarId.isAssigned)
+  let gs := gs.filter fun g => !g.inconsistent
   setGoals gs
 
 def getUnsolvedGoals : GrindTacticM (List Goal) := do
@@ -332,19 +329,13 @@ def liftGoalM (k : GoalM α) : GrindTacticM α := do
   replaceMainGoal [goal]
   return a
 
-inductive LiftActionCoreResult where
-  | closed | subgoals
-
-def liftActionCore (a : Action) : GrindTacticM LiftActionCoreResult := do
+def liftAction (a : Action) : GrindTacticM Unit := do
   let goal ← getMainGoal
   let ka := fun _ => throwError "tactic is not applicable"
   let kp := fun goal => return .stuck [goal]
   match (← liftGrindM <| a goal ka kp) with
-  | .closed _ => replaceMainGoal []; return .closed
-  | .stuck gs => replaceMainGoal gs; return .subgoals
-
-def liftAction (a : Action) : GrindTacticM Unit := do
-  discard <| liftActionCore a
+  | .closed _ => replaceMainGoal []
+  | .stuck gs => replaceMainGoal gs
 
 def done : GrindTacticM Unit := do
   pruneSolvedGoals

src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean

@@ -111,9 +111,7 @@ def evalCheck (tacticName : Name) (k : GoalM Bool)
      This matches the behavior of these tactics in default tactic mode
      where `lia` can close `x > 1 → x + y + z > 0` directly. -/
   if (← read).sym then
-    match (← liftActionCore <| Action.intros 0 >> Action.assertAll) with
-    | .closed   => return () -- closed the goal
-    | .subgoals => pure () -- continue
+    liftAction <| Action.intros 0 >> Action.assertAll
   let recover := (← read).recover
   liftGoalM do
     let progress ← k

src/Lean/Meta/ACLt.lean

@@ -175,7 +175,6 @@ where
     return !(← allChildrenLt a b)
 
   lpo (a b : Expr) : MetaM Bool := do
-    checkSystem "Lean.Meta.acLt"
     -- Case 1: `a < b` if for some child `b_i` of `b`, we have `b_i >= a`
     if (← someChildGe b a) then
       return true

src/Lean/Meta/Eqns.lean

@@ -37,17 +37,12 @@ register_builtin_option backward.eqns.deepRecursiveSplit : Bool := {
 These options affect the generation of equational theorems in a significant way. For these, their
 value at definition time, not realization time, should matter.
 
-This is implemented by storing their values at definition time (when non-default) in an environment
-extension, and restoring them when the equations are lazily realized.
+This is implemented by
+ * eagerly realizing the equations when they are set to a non-default value
+ * when realizing them lazily, reset the options to their default
 -/
 def eqnAffectingOptions : Array (Lean.Option Bool) := #[backward.eqns.nonrecursive, backward.eqns.deepRecursiveSplit]
 
-/-- Environment extension that stores the values of `eqnAffectingOptions` at definition time,
-keyed by declaration name. Only populated when at least one option has a non-default value.
-Stores an association list of (option name, value) pairs for options that differ from defaults. -/
-builtin_initialize eqnOptionsExt : MapDeclarationExtension (Array (Name × DataValue)) ←
-  mkMapDeclarationExtension (asyncMode := .local)
-
 def eqnThmSuffixBase := "eq"
 def eqnThmSuffixBasePrefix := eqnThmSuffixBase ++ "_"
 def eqn1ThmSuffix := eqnThmSuffixBasePrefix ++ "1"
@@ -158,30 +153,12 @@ structure EqnsExtState where
 builtin_initialize eqnsExt : EnvExtension EqnsExtState ←
   registerEnvExtension (pure {}) (asyncMode := .local)
 
-/--
-Runs `act` with the equation-affecting options restored to the values stored for `declName`
-at definition time (or reset to their defaults if none were stored). Use this inside
-`realizeConst` callbacks, which otherwise see the caller-independent `ctx.opts` rather than
-the outer `getEqnsFor?` context. -/
-def withEqnOptions (declName : Name) (act : MetaM α) : MetaM α := do
-  let env ← getEnv
-  let setOpts : Options → Options :=
-    if let some values := eqnOptionsExt.find? env declName then
-      fun os => Id.run do
-        let mut os := eqnAffectingOptions.foldl (fun os o => o.set os o.defValue) os
-        for (name, v) in values do
-          os := os.insert name v
-        return os
-    else
-      fun os => eqnAffectingOptions.foldl (fun os o => o.set os o.defValue) os
-  withOptions setOpts act
-
 /--
 Simple equation theorem for nonrecursive definitions.
 -/
 def mkSimpleEqThm (declName : Name) (name : Name) : MetaM (Option Name) := do
   if let some (.defnInfo info) := (← getEnv).find? declName then
-    realizeConst declName name (withEqnOptions declName (doRealize name info))
+    realizeConst declName name (doRealize name info)
     return some name
   else
     return none
@@ -252,22 +229,19 @@ private def getEqnsFor?Core (declName : Name) : MetaM (Option (Array Name)) := w
 Returns equation theorems for the given declaration.
 -/
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := withLCtx {} {} do
-  withEqnOptions declName do
+  -- This is the entry point for lazy equation generation. Ignore the current value
+  -- of the options, and revert to the default.
+  withOptions (eqnAffectingOptions.foldl fun os o => o.set os o.defValue) do
     getEqnsFor?Core declName
 
 /--
-If any equation theorem affecting option is not the default value, store the option values
-for later use during lazy equation generation.
+If any equation theorem affecting option is not the default value, create the equations now.
 -/
-def saveEqnAffectingOptions (declName : Name) : MetaM Unit := do
+def generateEagerEqns (declName : Name) : MetaM Unit := do
   let opts ← getOptions
-  let mut nonDefaults : Array (Name × DataValue) := #[]
-  for o in eqnAffectingOptions do
-    if o.get opts != o.defValue then
-      nonDefaults := nonDefaults.push (o.name, KVMap.Value.toDataValue (o.get opts))
-  unless nonDefaults.isEmpty do
-    trace[Elab.definition.eqns] "saving equation-affecting options for {declName}"
-    modifyEnv (eqnOptionsExt.insert · declName nonDefaults)
+  if eqnAffectingOptions.any fun o => o.get opts != o.defValue then
+    trace[Elab.definition.eqns] "generating eager equations for {declName}"
+    let _ ← getEqnsFor?Core declName
 
 @[expose] def GetUnfoldEqnFn := Name → MetaM (Option Name)
 

src/Lean/Meta/Instances.lean

@@ -229,33 +229,8 @@ private partial def computeSynthOrder (inst : Expr) (projInfo? : Option Projecti
 
   return synthed
 
-def checkImpossibleInstance (c : Expr) : MetaM Unit := do
-  let cTy ← inferType c
-  forallTelescopeReducing cTy fun args ty => do
-    let argTys ← args.mapM inferType
-    let impossibleArgs ← args.zipIdx.filterMapM fun (arg, i) => do
-      let fv := arg.fvarId!
-      if (← fv.getDecl).binderInfo.isInstImplicit then return none
-      if ty.containsFVar fv then return none
-      if argTys[i+1:].any (·.containsFVar fv) then return none
-      return some m!"{arg} : {← inferType arg}"
-    if impossibleArgs.isEmpty then return
-    let impossibleArgs := MessageData.joinSep impossibleArgs.toList ", "
-    throwError m!"Instance {c} has arguments "
-      ++ impossibleArgs
-      ++ " that are impossible to infer. Those arguments are not instance-implicit and do not appear in another instance-implicit argument or the return type."
-
-def checkNonClassInstance (declName : Name) (c : Expr) : MetaM Unit := do
-  let type ← inferType c
-  forallTelescopeReducing type fun _ target => do
-    unless (← isClass? target).isSome do
-      unless target.isSorry do
-      throwError m!"instance `{declName}` target `{target}` is not a type class."
-
 def addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : MetaM Unit := do
   let c ← mkConstWithLevelParams declName
-  checkImpossibleInstance c
-  checkNonClassInstance declName c
   let keys ← mkInstanceKey c
   let status ← getReducibilityStatus declName
   unless status matches .reducible | .implicitReducible do

src/Lean/Meta/LevelDefEq.lean

@@ -38,9 +38,7 @@ and assigning `?m := max ?n v`
 private def solveSelfMax (mvarId : LMVarId) (v : Level) : MetaM Unit := do
   assert! v.isMax
   let n ← mkFreshLevelMVar
-  let v' := mkMaxArgsDiff mvarId v n
-  trace[Meta.isLevelDefEq.step] "solveSelfMax: {mkLevelMVar mvarId} := {v'}"
-  assignLevelMVar mvarId v'
+  assignLevelMVar mvarId <| mkMaxArgsDiff mvarId v n
 
 /--
 Returns true if `v` is `max u ?m` (or variant). That is, we solve `u =?= max u ?m` as `?m := u`.
@@ -55,7 +53,6 @@ private def tryApproxSelfMax (u v : Level) : MetaM Bool := do
 where
   solve (v' : Level) (mvarId : LMVarId) : MetaM Bool := do
     if u == v' then
-      trace[Meta.isLevelDefEq.step] "tryApproxSelfMax {mkLevelMVar mvarId} := {u}"
       assignLevelMVar mvarId u
       return true
     else
@@ -74,14 +71,8 @@ private def tryApproxMaxMax (u v : Level) : MetaM Bool := do
   | _, _ => return false
 where
   solve (u₁ u₂ v' : Level) (mvarId : LMVarId) : MetaM Bool := do
-    if u₁ == v' then
-      trace[Meta.isLevelDefEq.step] "tryApproxMaxMax {mkLevelMVar mvarId} := {u₂}"
-      assignLevelMVar mvarId u₂
-      return true
-    else if u₂ == v' then
-      trace[Meta.isLevelDefEq.step] "tryApproxMaxMax {mkLevelMVar mvarId} := {u₁}"
-      assignLevelMVar mvarId u₁
-      return true
+    if u₁ == v' then assignLevelMVar mvarId u₂; return true
+    else if u₂ == v' then assignLevelMVar mvarId u₁; return true
     else return false
 
 private def postponeIsLevelDefEq (lhs : Level) (rhs : Level) : MetaM Unit := do
@@ -106,11 +97,9 @@ mutual
       else if (← isMVarWithGreaterDepth v mvarId) then
         -- If both `u` and `v` are both metavariables, but depth of v is greater, then we assign `v := u`.
         -- This can only happen when levelAssignDepth is set to a smaller value than depth (e.g. during TC synthesis)
-        trace[Meta.isLevelDefEq.step] "{v} := {u}"
         assignLevelMVar v.mvarId! u
         return LBool.true
       else if !u.occurs v then
-        trace[Meta.isLevelDefEq.step] "{u} := {v}"
         assignLevelMVar u.mvarId! v
         return LBool.true
       else if v.isMax && !strictOccursMax u v then
@@ -144,9 +133,8 @@ mutual
   @[export lean_is_level_def_eq]
   partial def isLevelDefEqAuxImpl : Level → Level → MetaM Bool
     | Level.succ lhs, Level.succ rhs => isLevelDefEqAux lhs rhs
-    | lhs, rhs => do
-      withTraceNodeBefore `Meta.isLevelDefEq (fun _ =>
-          withOptions (·.set `pp.instantiateMVars false) do addMessageContext m!"{lhs} =?= {rhs}") do
+    | lhs, rhs =>
+      withTraceNode `Meta.isLevelDefEq (fun _ => return m!"{lhs} =?= {rhs}") do
       if lhs.getLevelOffset == rhs.getLevelOffset then
         return lhs.getOffset == rhs.getOffset
       else

src/Lean/Meta/Sym/Eta.lean

@@ -9,37 +9,19 @@ public import Lean.Meta.Sym.ExprPtr
 public import Lean.Meta.Basic
 import Lean.Meta.Transform
 namespace Lean.Meta.Sym
-
-/--
-Returns `true` if `e` contains a loose bound variable with index in `[0, n)`
-This function assumes `n` is small. If this becomes a bottleneck, we should
-implement a version of `lean_expr_has_loose_bvar` that checks the range in one traversal.
--/
-def hasLooseBVarsInRange (e : Expr) (n : Nat) : Bool :=
-  e.hasLooseBVars && go n
-where
-  go : Nat → Bool
-  | 0 => false
-  | i+1 => e.hasLooseBVar i || go i
-
 /--
 Checks if `body` is eta-expanded with `n` applications: `f (.bvar (n-1)) ... (.bvar 0)`.
-Returns `f` if so and `f` has no loose bvars with indices in the range `[0, n)`; otherwise returns `default`.
+Returns `f` if so and `f` has no loose bvars; otherwise returns `default`.
 - `n`: number of remaining applications to check
 - `i`: expected bvar index (starts at 0, increments with each application)
 - `default`: returned when not eta-reducible (enables pointer equality check)
 -/
-def etaReduceAux (body : Expr) (n : Nat) (i : Nat) (default : Expr) : Expr :=
-  go body n i
-where
-  go (body : Expr) (m : Nat) (i : Nat) : Expr := Id.run do
-    match m with
-    | 0 =>
-      if hasLooseBVarsInRange body n then default
-      else body.lowerLooseBVars n n
-    | m+1 =>
-      let .app f (.bvar j) := body | default
-      if j == i then go f m (i+1) else default
+def etaReduceAux (body : Expr) (n : Nat) (i : Nat) (default : Expr) : Expr := Id.run do
+  match n with
+  | 0 => if body.hasLooseBVars then default else body
+  | n+1 =>
+    let .app f (.bvar j) := body | default
+    if j == i then etaReduceAux f n (i+1) default else default
 
 /--
 If `e` is of the form `(fun x₁ ... xₙ => f x₁ ... xₙ)` and `f` does not contain `x₁`, ..., `xₙ`,

src/Lean/Meta/Sym/Intro.lean

@@ -48,8 +48,6 @@ def introCore (mvarId : MVarId) (max : Nat) (names : Array Name) : SymM (Array F
     assignDelayedMVar auxMVar.mvarId! fvars mvarId'
     mvarId.assign val
   let finalize (lctx : LocalContext) (localInsts : LocalInstances) (fvars : Array Expr) (type : Expr) : SymM (Array Expr × MVarId) := do
-    if fvars.isEmpty then
-      return (#[], mvarId)
     let type ← instantiateRevS type fvars
     let mvar' ← mkFreshExprMVarAt lctx localInsts type .syntheticOpaque mvarDecl.userName
     let mvarId' := mvar'.mvarId!

src/Lean/Meta/Tactic/Apply.lean

@@ -128,6 +128,7 @@ def postprocessAppMVars (tacticName : Name) (mvarId : MVarId) (newMVars : Array
     (synthAssignedInstances := true) (allowSynthFailures := false) : MetaM Unit := do
   synthAppInstances tacticName mvarId newMVars binderInfos synthAssignedInstances allowSynthFailures
   -- TODO: default and auto params
+  appendParentTag mvarId newMVars binderInfos
 
 private def dependsOnOthers (mvar : Expr) (otherMVars : Array Expr) : MetaM Bool :=
   otherMVars.anyM fun otherMVar => do
@@ -222,7 +223,6 @@ def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig :=
     let e ← instantiateMVars e
     mvarId.assign (mkAppN e newMVars)
     let newMVars ← newMVars.filterM fun mvar => not <$> mvar.mvarId!.isAssigned
-    appendParentTag mvarId newMVars binderInfos
     let otherMVarIds ← getMVarsNoDelayed e
     let newMVarIds ← reorderGoals newMVars cfg.newGoals
     let otherMVarIds := otherMVarIds.filter fun mvarId => !newMVarIds.contains mvarId

src/Lean/Meta/Tactic/Grind/Order/Assert.lean

@@ -148,14 +148,11 @@ def propagatePending : OrderM Unit := do
         - `h₁ : ↑ue' = ue`
         - `h₂ : ↑ve' = ve`
         - `h : ue = ve`
-        **Note**: We currently only support `Nat` originals. Thus `↑a` is actually
-        `NatCast.natCast a`. The lemma `nat_eq` is specialized to `Int`, so we
-        only invoke it when the cast destination is `Int`. For other types (e.g.
-        `Rat`), `pushEq ue ve h` above is sufficient and `grind` core can derive
-        the `Nat` equality via `norm_cast`/cast injectivity if needed.
+        **Note**: We currently only support `Nat`. Thus `↑a` is actually
+        `NatCast.natCast a`. If we decide to support arbitrary semirings
+        in this module, we must adjust this code.
         -/
-        if (← inferType ue) == Int.mkType then
-          pushEq ue' ve' <| mkApp7 (mkConst ``Grind.Order.nat_eq) ue' ve' ue ve h₁ h₂ h
+        pushEq ue' ve' <| mkApp7 (mkConst ``Grind.Order.nat_eq) ue' ve' ue ve h₁ h₂ h
 where
   /--
   If `e` is an auxiliary term used to represent some term `a`, returns
@@ -346,7 +343,7 @@ def getStructIdOf? (e : Expr) : GoalM (Option Nat) := do
   return (← get').exprToStructId.find? { expr := e }
 
 def propagateIneq (e : Expr) : GoalM Unit := do
-  if let some { e := e', h := he, .. } := (← get').termMap.find? { expr := e } then
+  if let some (e', he) := (← get').termMap.find? { expr := e } then
     go e' (some he)
   else
     go e none
@@ -372,27 +369,20 @@ builtin_grind_propagator propagateLT ↓LT.lt := propagateIneq
 public def processNewEq (a b : Expr) : GoalM Unit := do
   unless isSameExpr a b do
     let h ← mkEqProof a b
-    if let some { e := a', h := h₁, α } ← getAuxTerm? a then
-      let some { e := b', h := h₂, .. } ← getAuxTerm? b | return ()
+    if let some (a', h₁) ← getAuxTerm? a then
+      let some (b', h₂) ← getAuxTerm? b | return ()
       /-
       We have
       - `h  : a = b`
       - `h₁ : ↑a = a'`
       - `h₂ : ↑b = b'`
-      where `a'` and `b'` are `NatCast.natCast α inst _` for some type `α`.
       -/
-      if α == Int.mkType then
-        let h := mkApp7 (mkConst ``Grind.Order.of_nat_eq) a b a' b' h₁ h₂ h
-        go a' b' h
-      else
-        let u ← getDecLevel α
-        let inst ← synthInstance (mkApp (mkConst ``NatCast [u]) α)
-        let h := mkApp9 (mkConst ``Grind.Order.of_natCast_eq [u]) α inst a b a' b' h₁ h₂ h
-        go a' b' h
+      let h := mkApp7 (mkConst ``Grind.Order.of_nat_eq) a b a' b' h₁ h₂ h
+      go a' b' h
     else
       go a b h
 where
-  getAuxTerm? (e : Expr) : GoalM (Option TermMapEntry) := do
+  getAuxTerm? (e : Expr) : GoalM (Option (Expr × Expr)) := do
     return (← get').termMap.find? { expr := e }
 
   go (a b h : Expr) : GoalM Unit := do

src/Lean/Meta/Tactic/Grind/Order/Internalize.lean

@@ -166,9 +166,9 @@ def setStructId (e : Expr) : OrderM Unit := do
     exprToStructId := s.exprToStructId.insert { expr := e } structId
   }
 
-def updateTermMap (e eNew h α : Expr) : GoalM Unit := do
+def updateTermMap (e eNew h : Expr) : GoalM Unit := do
   modify' fun s => { s with
-    termMap    := s.termMap.insert { expr := e } { e := eNew, h, α }
+    termMap    := s.termMap.insert { expr := e } (eNew, h)
     termMapInv := s.termMapInv.insert { expr := eNew } (e, h)
   }
 
@@ -198,9 +198,9 @@ where
   getOriginal? (e : Expr) : GoalM (Option Expr) := do
     if let some (e', _) := (← get').termMapInv.find? { expr := e } then
       return some e'
-    let_expr NatCast.natCast α _ a := e | return none
+    let_expr NatCast.natCast _ _ a := e | return none
     if (← alreadyInternalized a) then
-      updateTermMap a e (← mkEqRefl e) α
+      updateTermMap a e (← mkEqRefl e)
       return some a
     else
       return none
@@ -290,7 +290,7 @@ def internalizeTerm (e : Expr) : OrderM Unit := do
 
 open Arith.Cutsat in
 def adaptNat (e : Expr) : GoalM Expr := do
-  if let some { e := eNew, .. } := (← get').termMap.find? { expr := e } then
+  if let some (eNew, _) := (← get').termMap.find? { expr := e } then
     return eNew
   else match_expr e with
     | LE.le _ _ lhs rhs => adaptCnstr lhs rhs (isLT := false)
@@ -307,12 +307,12 @@ where
     let h := mkApp6
         (mkConst (if isLT then ``Nat.ToInt.lt_eq else ``Nat.ToInt.le_eq))
         lhs rhs lhs' rhs' h₁ h₂
-    updateTermMap e eNew h (← getIntExpr)
+    updateTermMap e eNew h
     return eNew
 
   adaptTerm : GoalM Expr := do
     let (eNew, h) ← natToInt e
-    updateTermMap e eNew h (← getIntExpr)
+    updateTermMap e eNew h
     return eNew
 
 def adapt (α : Expr) (e : Expr) : GoalM (Expr × Expr) := do

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

@@ -128,13 +128,6 @@ structure Struct where
   propagate          : List ToPropagate := []
   deriving Inhabited
 
-/-- Entry/Value for the map `termMap` in `State` -/
-structure TermMapEntry where
-  e : Expr
-  h : Expr
-  α : Expr
-deriving Inhabited
-
 /-- State for all order types detected by `grind`. -/
 structure State where
   /-- Order structures detected. -/
@@ -150,7 +143,7 @@ structure State where
   Example: given `x y : Nat`, `x ≤ y + 1` is mapped to `Int.ofNat x ≤ Int.ofNat y + 1`, and proof
   of equivalence.
   -/
-  termMap    : PHashMap ExprPtr TermMapEntry := {}
+  termMap    : PHashMap ExprPtr (Expr × Expr) := {}
   /-- `termMap` inverse -/
   termMapInv : PHashMap ExprPtr (Expr × Expr) := {}
   deriving Inhabited

src/Lean/Meta/Tactic/Rewrite.lean

@@ -82,7 +82,6 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
           postprocessAppMVars `rewrite mvarId newMVars binderInfos
             (synthAssignedInstances := !tactic.skipAssignedInstances.get (← getOptions))
           let newMVarIds ← newMVars.map Expr.mvarId! |>.filterM fun mvarId => not <$> mvarId.isAssigned
-          appendParentTag mvarId newMVars binderInfos
           let otherMVarIds ← getMVarsNoDelayed heqIn
           let otherMVarIds := otherMVarIds.filter (!newMVarIds.contains ·)
           let newMVarIds := newMVarIds ++ otherMVarIds

src/Lean/Meta/WrapInstance.lean

@@ -145,6 +145,7 @@ public partial def wrapInstance (inst expectedType : Expr) (compile : Bool := tr
           else
             let name ← mkAuxDeclName
             let wrapped ← mkAuxDefinition name expectedType inst (compile := false)
+            setReducibilityStatus name .implicitReducible
             if isMeta then modifyEnv (markMeta · name)
             if compile then
               compileDecls (logErrors := logCompileErrors) #[name]

src/Lean/Parser/Do.lean

@@ -273,15 +273,6 @@ with debug assertions enabled (see the `debugAssertions` option).
 @[builtin_doElem_parser] def doDebugAssert := leading_parser:leadPrec
   "debug_assert! " >> termParser
 
-@[builtin_doElem_parser] def doRepeat      := leading_parser
-  "repeat " >> doSeq
-@[builtin_doElem_parser] def doWhileH      := leading_parser
-  "while " >> ident >> " : " >> withForbidden "do" termParser >> " do " >> doSeq
-@[builtin_doElem_parser] def doWhile       := leading_parser
-  "while " >> withForbidden "do" termParser >> " do " >> doSeq
-@[builtin_doElem_parser] def doRepeatUntil := leading_parser
-  "repeat " >> doSeq >> ppDedent ppLine >> "until " >> termParser
-
 /-
 We use `notFollowedBy` to avoid counterintuitive behavior.
 

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -484,7 +484,6 @@ open SubExpr (Pos PosMap)
 open Delaborator (OptionsPerPos topDownAnalyze DelabM getPPOption)
 
 def delabLevel (l : Level) (prec : Nat) : MetaM Syntax.Level := do
-  let l ← if getPPInstantiateMVars (← getOptions) then instantiateLevelMVars l else pure l
   let mvars := getPPMVarsLevels (← getOptions)
   return Level.quote l prec (mvars := mvars) (lIndex? := (← getMCtx).findLevelIndex?)
 

src/Lean/Server/FileWorker.lean

@@ -77,6 +77,8 @@ def OutputMessage.ofMsg (msg : JsonRpc.Message) : OutputMessage where
   msg? := msg
   serialized := toJson msg |>.compress
 
+open Widget in
+
 structure WorkerContext where
   /-- Synchronized output channel for LSP messages. Notifications for outdated versions are
     discarded on read. -/
@@ -87,6 +89,10 @@ structure WorkerContext where
   -/
   maxDocVersionRef         : IO.Ref Int
   freshRequestIdRef        : IO.Ref Int
+  /--
+  Diagnostics that are included in every single `textDocument/publishDiagnostics` notification.
+  -/
+  stickyDiagnosticsRef     : IO.Ref (Array InteractiveDiagnostic)
   partialHandlersRef       : IO.Ref (Std.TreeMap String PartialHandlerInfo)
   pendingServerRequestsRef : IO.Ref (Std.TreeMap RequestID (IO.Promise (ServerRequestResponse Json)))
   hLog                     : FS.Stream
@@ -202,11 +208,19 @@ This option can only be set on the command line, not in the lakefile or via `set
     diags : Array Widget.InteractiveDiagnostic
   deriving TypeName
 
-  /-- Sends a `textDocument/publishDiagnostics` notification to the client. -/
+  /--
+  Sends a `textDocument/publishDiagnostics` notification to the client that contains the diagnostics
+  in `ctx.stickyDiagnosticsRef` and `doc.diagnosticsRef`.
+  -/
   private def publishDiagnostics (ctx : WorkerContext) (doc : EditableDocumentCore)
       : BaseIO Unit := do
-    let supportsIncremental := ctx.initParams.capabilities.incrementalDiagnosticSupport
-    doc.publishDiagnostics supportsIncremental fun notif => ctx.chanOut.sync.send <| .ofMsg notif
+    let stickyInteractiveDiagnostics ← ctx.stickyDiagnosticsRef.get
+    let docInteractiveDiagnostics ← doc.diagnosticsRef.get
+    let diagnostics :=
+      stickyInteractiveDiagnostics ++ docInteractiveDiagnostics
+      |>.map (·.toDiagnostic)
+    let notification := mkPublishDiagnosticsNotification doc.meta diagnostics
+    ctx.chanOut.sync.send <| .ofMsg notification
 
   open Language in
   /--
@@ -307,7 +321,7 @@ This option can only be set on the command line, not in the lakefile or via `set
             if let some cacheRef := node.element.diagnostics.interactiveDiagsRef? then
               cacheRef.set <| some <| .mk { diags : MemorizedInteractiveDiagnostics }
             pure diags
-        doc.appendDiagnostics diags
+        doc.diagnosticsRef.modify (· ++ diags)
         if (← get).hasBlocked then
           publishDiagnostics ctx doc
 
@@ -449,7 +463,7 @@ section Initialization
     let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
     let maxDocVersionRef ← IO.mkRef 0
     let freshRequestIdRef ← IO.mkRef (0 : Int)
-    let stickyDiagsRef ← IO.mkRef {}
+    let stickyDiagnosticsRef ← IO.mkRef ∅
     let pendingServerRequestsRef ← IO.mkRef ∅
     let chanOut ← mkLspOutputChannel maxDocVersionRef
     let timestamp ← IO.monoMsNow
@@ -479,10 +493,11 @@ section Initialization
       maxDocVersionRef
       freshRequestIdRef
       cmdlineOpts := opts
+      stickyDiagnosticsRef
     }
-    let diagnosticsMutex ← Std.Mutex.new { stickyDiagsRef }
     let doc : EditableDocumentCore := {
-      «meta» := doc, initSnap, diagnosticsMutex
+      «meta» := doc, initSnap
+      diagnosticsRef := (← IO.mkRef ∅)
     }
     let reporterCancelTk ← CancelToken.new
     let reporter ← reportSnapshots ctx doc reporterCancelTk
@@ -563,11 +578,14 @@ section Updates
     modify fun st => { st with pendingRequests := map st.pendingRequests }
 
   /-- Given the new document, updates editable doc state. -/
-  def updateDocument («meta» : DocumentMeta) : WorkerM Unit := do
+  def updateDocument (doc : DocumentMeta) : WorkerM Unit := do
     (← get).reporterCancelTk.set
     let ctx ← read
-    let initSnap ← ctx.processor «meta».mkInputContext
-    let doc ← (← get).doc.update «meta» initSnap
+    let initSnap ← ctx.processor doc.mkInputContext
+    let doc : EditableDocumentCore := {
+      «meta» := doc, initSnap
+      diagnosticsRef := (← IO.mkRef ∅)
+    }
     let reporterCancelTk ← CancelToken.new
     let reporter ← reportSnapshots ctx doc reporterCancelTk
     modify fun st => { st with doc := { doc with reporter }, reporterCancelTk }
@@ -619,16 +637,18 @@ section NotificationHandling
     let ctx ← read
     let s ← get
     let text := s.doc.meta.text
-    let importOutOfDateMessage :=
-      .text s!"Imports are out of date and should be rebuilt; \
-        use the \"Restart File\" command in your editor."
+    let importOutOfDataMessage := .text s!"Imports are out of date and should be rebuilt; \
+      use the \"Restart File\" command in your editor."
     let diagnostic := {
       range      := ⟨⟨0, 0⟩, ⟨1, 0⟩⟩
       fullRange? := some ⟨⟨0, 0⟩, text.utf8PosToLspPos text.source.rawEndPos⟩
       severity?  := DiagnosticSeverity.information
-      message := importOutOfDateMessage
+      message := importOutOfDataMessage
     }
-    s.doc.appendStickyDiagnostic diagnostic
+    ctx.stickyDiagnosticsRef.modify fun stickyDiagnostics =>
+      let stickyDiagnostics := stickyDiagnostics.filter
+        (·.message.stripTags != importOutOfDataMessage.stripTags)
+      stickyDiagnostics.push diagnostic
     publishDiagnostics ctx s.doc.toEditableDocumentCore
 
 def handleRpcRelease (p : Lsp.RpcReleaseParams) : WorkerM Unit := do
@@ -739,17 +759,19 @@ section MessageHandling
 
   open Widget RequestM Language in
   def handleGetInteractiveDiagnosticsRequest
-      (doc : EditableDocument)
+      (ctx : WorkerContext)
       (params : GetInteractiveDiagnosticsParams)
       : RequestM (Array InteractiveDiagnostic) := do
+    let doc ← readDoc
     -- NOTE: always uses latest document (which is the only one we can retrieve diagnostics for);
     -- any race should be temporary as the client should re-request interactive diagnostics when
     -- they receive the non-interactive diagnostics for the new document
-    let allDiags ← doc.collectCurrentDiagnostics
+    let stickyDiags ← ctx.stickyDiagnosticsRef.get
+    let diags ← doc.diagnosticsRef.get
     -- NOTE: does not wait for `lineRange?` to be fully elaborated, which would be problematic with
     -- fine-grained incremental reporting anyway; instead, the client is obligated to resend the
     -- request when the non-interactive diagnostics of this range have changed
-    return PersistentArray.toArray <| allDiags.filter fun diag =>
+    return (stickyDiags ++ diags).filter fun diag =>
       let r := diag.fullRange
       let diagStartLine := r.start.line
       let diagEndLine   :=
@@ -762,7 +784,7 @@ section MessageHandling
         s ≤ diagStartLine ∧ diagStartLine < e ∨
         diagStartLine ≤ s ∧ s < diagEndLine
 
-  def handlePreRequestSpecialCases? (st : WorkerState)
+  def handlePreRequestSpecialCases? (ctx : WorkerContext) (st : WorkerState)
       (id : RequestID) (method : String) (params : Json)
       : RequestM (Option (RequestTask SerializedLspResponse)) := do
     match method with
@@ -773,7 +795,7 @@ section MessageHandling
       let some seshRef := st.rpcSessions.get? params.sessionId
         | throw RequestError.rpcNeedsReconnect
       let params ← RequestM.parseRequestParams Widget.GetInteractiveDiagnosticsParams params.params
-      let resp ← handleGetInteractiveDiagnosticsRequest st.doc params
+      let resp ← handleGetInteractiveDiagnosticsRequest ctx params
       let resp ← seshRef.modifyGet fun st =>
         rpcEncode resp st.objects |>.map (·) ({st with objects := ·})
       return some <| .pure { response? := resp, serialized := resp.compress, isComplete := true }
@@ -903,7 +925,7 @@ section MessageHandling
       serverRequestEmitter := sendUntypedServerRequest ctx
     }
     let requestTask? ← EIO.toIO' <| RequestM.run (rc := rc) do
-      if let some response ← handlePreRequestSpecialCases? st id method params then
+      if let some response ← handlePreRequestSpecialCases? ctx st id method params then
         return response
       let task ← handleLspRequest method params
       let task ← handlePostRequestSpecialCases id method params task

src/Lean/Server/FileWorker/Utils.lean

@@ -10,7 +10,6 @@ prelude
 public import Lean.Language.Lean.Types
 public import Lean.Server.Snapshots
 public import Lean.Server.AsyncList
-public import Std.Sync.Mutex
 
 public section
 
@@ -40,26 +39,6 @@ where
         | some next => .delayed <| next.task.asServerTask.bindCheap go
         | none => .nil)
 
-/--
-Tracks diagnostics and incremental diagnostic reporting state for a single document version.
-
-The sticky diagnostics are shared across all document versions via an `IO.Ref`, while per-version
-diagnostics are stored directly. The whole state is wrapped in a `Std.Mutex` on
-`EditableDocumentCore` to ensure atomic updates.
--/
-structure DiagnosticsState where
-  /--
-  Diagnostics that persist across document versions (e.g. stale dependency warnings).
-  Shared across all versions via an `IO.Ref`.
-  -/
-  stickyDiagsRef : IO.Ref (PersistentArray Widget.InteractiveDiagnostic)
-  /-- Diagnostics accumulated during snapshot reporting. -/
-  diags : PersistentArray Widget.InteractiveDiagnostic := {}
-  /-- Whether the next `publishDiagnostics` call should be incremental. -/
-  isIncremental : Bool := false
-  /-- Amount of diagnostics reported in `publishDiagnostics` so far. -/
-  publishedDiagsAmount : Nat := 0
-
 /--
 A document bundled with processing information. Turned into `EditableDocument` as soon as the
 reporter task has been started.
@@ -71,94 +50,11 @@ structure EditableDocumentCore where
   initSnap : Language.Lean.InitialSnapshot
   /-- Old representation for backward compatibility. -/
   cmdSnaps : AsyncList IO.Error Snapshot := private_decl% mkCmdSnaps initSnap
-  /-- Per-version diagnostics state, protected by a mutex. -/
-  diagnosticsMutex : Std.Mutex DiagnosticsState
-
-namespace EditableDocumentCore
-open Widget
-
-/-- Appends new non-sticky diagnostics. -/
-def appendDiagnostics (doc : EditableDocumentCore) (diags : Array InteractiveDiagnostic) :
-    BaseIO Unit :=
-  doc.diagnosticsMutex.atomically do
-    modify fun ds => { ds with diags := diags.foldl (init := ds.diags) fun acc d => acc.push d }
-
-/--
-Appends a sticky diagnostic and marks the next publish as non-incremental.
-Removes any existing sticky diagnostic whose `message.stripTags` matches the new one.
--/
-def appendStickyDiagnostic (doc : EditableDocumentCore) (diagnostic : InteractiveDiagnostic) :
-    BaseIO Unit :=
-  doc.diagnosticsMutex.atomically do
-    let ds ← get
-    ds.stickyDiagsRef.modify fun stickyDiags =>
-      let stickyDiags := stickyDiags.filter
-        (·.message.stripTags != diagnostic.message.stripTags)
-      stickyDiags.push diagnostic
-    set { ds with isIncremental := false }
-
-/-- Returns all current diagnostics (sticky ++ doc). -/
-def collectCurrentDiagnostics (doc : EditableDocumentCore) :
-    BaseIO (PersistentArray InteractiveDiagnostic) :=
-  doc.diagnosticsMutex.atomically do
-    let ds ← get
-    let stickyDiags ← ds.stickyDiagsRef.get
-    return stickyDiags ++ ds.diags
-
-/--
-Creates a new `EditableDocumentCore` for a new document version, sharing the same sticky
-diagnostics with the previous version.
--/
-def update (doc : EditableDocumentCore) (newMeta : DocumentMeta)
-    (newInitSnap : Language.Lean.InitialSnapshot) : BaseIO EditableDocumentCore := do
-  let stickyDiagsRef ← doc.diagnosticsMutex.atomically do
-    return (← get).stickyDiagsRef
-  let diagnosticsMutex ← Std.Mutex.new { stickyDiagsRef }
-  return { «meta» := newMeta, initSnap := newInitSnap, diagnosticsMutex }
-
-/--
-Collects diagnostics for a `textDocument/publishDiagnostics` notification, updates
-the incremental tracking fields and writes the notification to the client.
-
-When `incrementalDiagnosticSupport` is `true` and the state allows it, sends only
-the newly added diagnostics with `isIncremental? := some true`. Otherwise, sends
-all sticky and non-sticky diagnostics non-incrementally.
-
-The state update and the write are performed atomically under the diagnostics mutex
-to prevent reordering between concurrent publishers (the reporter task and the main thread).
--/
-def publishDiagnostics (doc : EditableDocumentCore) (incrementalDiagnosticSupport : Bool)
-    (writeDiagnostics : JsonRpc.Notification Lsp.PublishDiagnosticsParams → BaseIO Unit) :
-    BaseIO Unit := do
-  -- The mutex must be held across both the state update and the write to ensure that concurrent
-  -- publishers (e.g. the reporter task and the main thread) cannot interleave their state reads
-  -- and writes, which would reorder incremental/non-incremental messages and corrupt client state.
-  doc.diagnosticsMutex.atomically do
-    let ds ← get
-    let useIncremental := incrementalDiagnosticSupport && ds.isIncremental
-    let stickyDiags ← ds.stickyDiagsRef.get
-    let diags := ds.diags
-    let publishedDiagsAmount := ds.publishedDiagsAmount
-    set <| { ds with publishedDiagsAmount := diags.size, isIncremental := true }
-    let (diagsToSend, isIncremental) :=
-      if useIncremental then
-        let newDiags := diags.foldl (init := #[]) (start := publishedDiagsAmount) fun acc d =>
-          acc.push d.toDiagnostic
-        (newDiags, true)
-      else
-        let allDiags := stickyDiags.foldl (init := #[]) fun acc d =>
-          acc.push d.toDiagnostic
-        let allDiags := diags.foldl (init := allDiags) fun acc d =>
-          acc.push d.toDiagnostic
-        (allDiags, false)
-    let isIncremental? :=
-      if incrementalDiagnosticSupport then
-        some isIncremental
-      else
-        none
-    writeDiagnostics <| mkPublishDiagnosticsNotification doc.meta diagsToSend isIncremental?
-
-end EditableDocumentCore
+  /--
+  Interactive versions of diagnostics reported so far. Filled by `reportSnapshots` and read by
+  `handleGetInteractiveDiagnosticsRequest`.
+  -/
+  diagnosticsRef : IO.Ref (Array Widget.InteractiveDiagnostic)
 
 /-- `EditableDocumentCore` with reporter task. -/
 structure EditableDocument extends EditableDocumentCore where

src/Lean/Server/ProtocolOverview.lean

@@ -152,9 +152,9 @@ def protocolOverview : Array MessageOverview := #[
   .notification {
     method := "textDocument/publishDiagnostics"
     direction := .serverToClient
-    kinds := #[.extendedParameterType #[``PublishDiagnosticsParams.isIncremental?, ``PublishDiagnosticsParams.diagnostics, ``DiagnosticWith.fullRange?, ``DiagnosticWith.isSilent?, ``DiagnosticWith.leanTags?]]
+    kinds := #[.extendedParameterType #[``PublishDiagnosticsParams.diagnostics, ``DiagnosticWith.fullRange?, ``DiagnosticWith.isSilent?, ``DiagnosticWith.leanTags?]]
     parameterType := PublishDiagnosticsParams
-    description := "Emitted by the language server whenever a new set of diagnostics becomes available for a file. Unlike most language servers, the Lean language server emits this notification incrementally while processing the file, not only when the full file has been processed. If the client sets `LeanClientCapabilities.incrementalDiagnosticSupport` and `isIncremental` is `true`, the diagnostics in the notification should be appended to the existing diagnostics for the same document version rather than replacing them."
+    description := "Emitted by the language server whenever a new set of diagnostics becomes available for a file. Unlike most language servers, the Lean language server emits this notification incrementally while processing the file, not only when the full file has been processed."
   },
   .notification {
     method := "$/lean/fileProgress"

src/Lean/Server/Test/Runner.lean

@@ -723,7 +723,6 @@ partial def main (args : List String) : IO Unit := do
         }
       }
       lean? := some {
-        incrementalDiagnosticSupport? := some true
         silentDiagnosticSupport? := some true
         rpcWireFormat? := some .v1
       }

src/Lean/Server/Utils.lean

@@ -133,14 +133,12 @@ def foldDocumentChanges (changes : Array Lsp.TextDocumentContentChangeEvent) (ol
   changes.foldl applyDocumentChange oldText
 
 /-- Constructs a `textDocument/publishDiagnostics` notification. -/
-def mkPublishDiagnosticsNotification (m : DocumentMeta) (diagnostics : Array Lsp.Diagnostic)
-    (isIncremental : Option Bool := none) :
+def mkPublishDiagnosticsNotification (m : DocumentMeta) (diagnostics : Array Lsp.Diagnostic) :
     JsonRpc.Notification Lsp.PublishDiagnosticsParams where
   method := "textDocument/publishDiagnostics"
   param  := {
     uri         := m.uri
     version?    := some m.version
-    isIncremental? := isIncremental
     diagnostics := diagnostics
   }
 

src/Std/Data/DHashMap/RawDecidableEquiv.lean

@@ -18,7 +18,7 @@ open Std.DHashMap.Internal
 
 namespace Std.DHashMap.Raw
 
-def instDecidableEquiv {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Hashable α] [∀ k, BEq (β k)] [∀ k, LawfulBEq (β k)] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁ ~m m₂) :=
+instance instDecidableEquiv {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Hashable α] [∀ k, BEq (β k)] [∀ k, LawfulBEq (β k)] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁ ~m m₂) :=
   Raw₀.decidableEquiv ⟨m₁, h₁.size_buckets_pos⟩ ⟨m₂, h₂.size_buckets_pos⟩ h₁ h₂
 
 end Std.DHashMap.Raw

src/Std/Data/DTreeMap/Raw/DecidableEquiv.lean

@@ -19,7 +19,7 @@ open Std.DTreeMap.Internal.Impl
 
 namespace Std.DTreeMap.Raw
 
-def instDecidableEquiv {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] [∀ k, BEq (β k)] [∀ k, LawfulBEq (β k)] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) : Decidable (t₁ ~m t₂) :=
+instance instDecidableEquiv {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] [∀ k, BEq (β k)] [∀ k, LawfulBEq (β k)] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) : Decidable (t₁ ~m t₂) :=
   let : Ord α := ⟨cmp⟩;
   let : Decidable (t₁.inner ~m t₂.inner) := decidableEquiv t₁.1 t₂.1 h₁ h₂;
   decidable_of_iff _ ⟨fun h => ⟨h⟩, fun h => h.1⟩

src/Std/Data/HashMap/RawDecidableEquiv.lean

@@ -19,7 +19,7 @@ open Std.DHashMap.Raw
 
 namespace Std.HashMap.Raw
 
-def instDecidableEquiv {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] [Hashable α] [BEq β] [LawfulBEq β] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁ ~m m₂) :=
+instance instDecidableEquiv {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] [Hashable α] [BEq β] [LawfulBEq β] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁ ~m m₂) :=
   let : Decidable (m₁.1 ~m m₂.1) := DHashMap.Raw.instDecidableEquiv h₁.out h₂.out;
   decidable_of_iff _ ⟨fun h => ⟨h⟩, fun h => h.1⟩
 

src/Std/Data/HashSet/RawDecidableEquiv.lean

@@ -19,7 +19,7 @@ open Std.HashMap.Raw
 
 namespace Std.HashSet.Raw
 
-def instDecidableEquiv {α : Type u} [BEq α] [LawfulBEq α] [Hashable α] {m₁ m₂ : Raw α} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁ ~m m₂) :=
+instance instDecidableEquiv {α : Type u} [BEq α] [LawfulBEq α] [Hashable α] {m₁ m₂ : Raw α} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁ ~m m₂) :=
   let : Decidable (m₁.1 ~m m₂.1) := HashMap.Raw.instDecidableEquiv h₁.out h₂.out;
   decidable_of_iff _ ⟨fun h => ⟨h⟩, fun h => h.1⟩
 

src/Std/Data/TreeMap/Raw/DecidableEquiv.lean

@@ -20,7 +20,7 @@ open Std.DTreeMap.Raw
 
 namespace Std.TreeMap.Raw
 
-def instDecidableEquiv {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] [BEq β] [LawfulBEq β] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) : Decidable (t₁ ~m t₂) :=
+instance instDecidableEquiv {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] [BEq β] [LawfulBEq β] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) : Decidable (t₁ ~m t₂) :=
   let : Ord α := ⟨cmp⟩;
   let : Decidable (t₁.inner ~m t₂.inner) := DTreeMap.Raw.instDecidableEquiv h₁ h₂;
   decidable_of_iff _ ⟨fun h => ⟨h⟩, fun h => h.1⟩

src/Std/Data/TreeSet/Raw/DecidableEquiv.lean

@@ -20,7 +20,7 @@ open Std.TreeMap.Raw
 
 namespace Std.TreeSet.Raw
 
-def instDecidableEquiv {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] {t₁ t₂ : Raw α cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) : Decidable (t₁ ~m t₂) :=
+instance instDecidableEquiv {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] {t₁ t₂ : Raw α cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) : Decidable (t₁ ~m t₂) :=
   let : Ord α := ⟨cmp⟩;
   let : Decidable (t₁.inner ~m t₂.inner) := TreeMap.Raw.instDecidableEquiv h₁ h₂;
   decidable_of_iff _ ⟨fun h => ⟨h⟩, fun h => h.1⟩

src/lake/Lake/Build/Common.lean

@@ -235,7 +235,7 @@ public def checkHashUpToDate
 : JobM Bool := (·.isUpToDate) <$> checkHashUpToDate' info depTrace depHash oldTrace
 
 /--
-**For internal use only.**
+**Ror internal use only.**
 Checks whether `info` is up-to-date with the trace.
 If so, replays the log of the trace if available.
 -/
@@ -271,24 +271,20 @@ Returns `true` if the saved trace exists and its hash matches `inputHash`.
 
 If up-to-date, replays the saved log from the trace and sets the current
 build action to `replay`. Otherwise, if the log is empty and trace is synthetic,
-or if the trace is not up-to-date, the build action will be set to `reuse`.
+or if the trace is not up-to-date, the build action will be set to `fetch`.
 -/
-public def SavedTrace.replayCachedIfUpToDate (inputHash : Hash) (self : SavedTrace) : JobM Bool := do
+public def SavedTrace.replayOrFetchIfUpToDate (inputHash : Hash) (self : SavedTrace) : JobM Bool := do
   if let .ok data := self then
     if data.depHash == inputHash then
       if data.synthetic && data.log.isEmpty then
-        updateAction .reuse
+        updateAction .fetch
       else
         updateAction .replay
         data.log.replay
       return true
-  updateAction .reuse
+  updateAction .fetch
   return false
 
-@[deprecated replayCachedIfUpToDate (since := "2026-04-15")]
-public abbrev SavedTrace.replayOrFetchIfUpToDate (inputHash : Hash) (self : SavedTrace) : JobM Bool := do
-  self.replayCachedIfUpToDate inputHash
-
 /-- **For internal use only.** -/
 public class ToOutputJson (α : Type u) where
   toOutputJson (arts : α) : Json
@@ -688,7 +684,7 @@ public def buildArtifactUnlessUpToDate
     let fetchArt? restore := do
       let some (art : XArtifact exe) ← getArtifacts? inputHash savedTrace pkg
         | return none
-      unless (← savedTrace.replayCachedIfUpToDate inputHash) do
+      unless (← savedTrace.replayOrFetchIfUpToDate inputHash) do
         removeFileIfExists file
         writeFetchTrace traceFile inputHash (toJson art.descr)
       if restore then

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

@@ -29,18 +29,11 @@ namespace Lake
 public inductive JobAction
 /-- No information about this job's action is available. -/
 | unknown
-/-- Tried to reuse a cached build (e.g., can be set by `replayCachedIfUpToDate`). -/
-| reuse
-/-- Tried to replay a completed build action (e.g., can be set by `replayIfUpToDate`). -/
+/-- Tried to replay a cached build action (set by `buildFileUnlessUpToDate`) -/
 | replay
-/-- Tried to unpack a build from an archive (e.g., unpacking a module `ltar`). -/
-| unpack
-/--
-Tried to fetch a build from a remote store (e.g., set when downloading an artifact
-on-demand from a cache service in `buildArtifactUnlessUpToDate`).
--/
+/-- Tried to fetch a build from a store (can be set by `buildUnlessUpToDate?`) -/
 | fetch
-/-- Tried to perform a build action (e.g., set by `buildAction`). -/
+/-- Tried to perform a build action (set by `buildUnlessUpToDate?`) -/
 | build
 deriving Inhabited, Repr, DecidableEq, Ord
 
@@ -52,13 +45,11 @@ public instance : Min JobAction := minOfLe
 public instance : Max JobAction := maxOfLe
 
 public def merge (a b : JobAction) : JobAction :=
-  max a b -- inlines `max`
+  max a b
 
-public def verb (failed : Bool) : (self : JobAction) → String
+public def verb (failed : Bool) : JobAction → String
 | .unknown => if failed then "Running" else "Ran"
-| .reuse => if failed then "Reusing" else "Reused"
 | .replay => if failed then "Replaying" else "Replayed"
-| .unpack => if failed then "Unpacking" else "Unpacked"
 | .fetch => if failed then "Fetching" else "Fetched"
 | .build => if failed then "Building" else "Built"
 

src/lake/Lake/Build/Module.lean

@@ -900,9 +900,8 @@ where
     let inputHash := (← getTrace).hash
     let some ltarOrArts ← getArtifacts? inputHash savedTrace mod.pkg
       | return .inr savedTrace
-    match (ltarOrArts : ModuleOutputs) with
+    match (ltarOrArts : ModuleOutputs)  with
     | .ltar ltar =>
-      updateAction .unpack
       mod.clearOutputArtifacts
       mod.unpackLtar ltar.path
       -- Note: This branch implies that only the ltar output is (validly) cached.
@@ -920,7 +919,7 @@ where
       else
         return .inr savedTrace
     | .arts arts =>
-      unless (← savedTrace.replayCachedIfUpToDate inputHash) do
+      unless (← savedTrace.replayOrFetchIfUpToDate inputHash) do
         mod.clearOutputArtifacts
         writeFetchTrace mod.traceFile inputHash (toJson arts.descrs)
       let arts ←

src/lake/Lake/Build/Package.lean

@@ -25,8 +25,12 @@ namespace Lake
 open Lean (Name)
 
 /-- Fetch the package's direct dependencies. -/
-def Package.recFetchDeps (self : Package) : FetchM (Job (Array Package)) := do
-  return Job.pure self.depPkgs
+def Package.recFetchDeps (self : Package) : FetchM (Job (Array Package)) := ensureJob do
+  (pure ·) <$> self.depConfigs.mapM fun cfg => do
+    let some dep ← findPackageByName? cfg.name
+      | error s!"{self.prettyName}: package not found for dependency '{cfg.name}' \
+        (this is likely a bug in Lake)"
+    return dep
 
 /-- The `PackageFacetConfig` for the builtin `depsFacet`. -/
 public def Package.depsFacetConfig : PackageFacetConfig depsFacet :=
@@ -34,7 +38,10 @@ public def Package.depsFacetConfig : PackageFacetConfig depsFacet :=
 
 /-- Compute a topological ordering of the package's transitive dependencies. -/
 def Package.recComputeTransDeps (self : Package) : FetchM (Job (Array Package)) := ensureJob do
-  (pure ·.toArray) <$> self.depPkgs.foldlM (init := OrdPackageSet.empty) fun deps dep => do
+  (pure ·.toArray) <$> self.depConfigs.foldlM (init := OrdPackageSet.empty) fun deps cfg => do
+    let some dep ← findPackageByName? cfg.name
+      | error s!"{self.prettyName}: package not found for dependency '{cfg.name}' \
+        (this is likely a bug in Lake)"
     let depDeps ← (← fetch <| dep.transDeps).await
     return depDeps.foldl (·.insert ·) deps |>.insert dep
 
@@ -146,7 +153,7 @@ def Package.fetchBuildArchive
   let upToDate ← buildUnlessUpToDate? (action := .fetch) archiveFile depTrace traceFile do
     download url archiveFile headers
   unless upToDate && (← self.buildDir.pathExists) do
-    updateAction .unpack
+    updateAction .fetch
     untar archiveFile self.buildDir
 
 @[inline]

src/lake/Lake/Build/Run.lean

@@ -210,7 +210,7 @@ def mkMonitorContext (cfg : BuildConfig) (jobs : JobQueue) : BaseIO MonitorConte
   let failLv := cfg.failLv
   let isVerbose := cfg.verbosity = .verbose
   let showProgress := cfg.showProgress
-  let minAction := if isVerbose then .unknown else .unpack
+  let minAction := if isVerbose then .unknown else .fetch
   let showOptional := isVerbose
   let showTime := isVerbose || !useAnsi
   let updateFrequency := 100

src/lake/Lake/Build/Trace.lean

@@ -9,7 +9,7 @@ prelude
 public import Lean.Data.Json
 import Init.Data.Nat.Fold
 meta import Init.Data.Nat.Fold
-public import Lake.Util.String
+import Lake.Util.String
 public import Init.Data.String.Search
 public import Init.Data.String.Extra
 import Init.Data.Option.Coe
@@ -141,8 +141,8 @@ public def ofHex? (s : String) : Option Hash :=
   if s.utf8ByteSize = 16 && isHex s then ofHex s else none
 
 /-- Returns the hash as 16-digit lowercase hex string. -/
-@[inline] public def hex (self : Hash) : String :=
-  lowerHexUInt64 self.val
+public def hex (self : Hash) : String :=
+  lpad (String.ofList <| Nat.toDigits 16 self.val.toNat) '0' 16
 
 /-- Parse a hash from a string of decimal digits. -/
 public def ofDecimal? (s : String) : Option Hash :=

src/lake/Lake/CLI/Main.lean

@@ -69,7 +69,7 @@ public structure LakeOptions where
   scope? : Option CacheServiceScope := none
   platform? : Option CachePlatform := none
   toolchain? : Option CacheToolchain := none
-  rev? : Option GitRev := none
+  rev? : Option String := none
   maxRevs : Nat := 100
   shake : Shake.Args := {}
 
@@ -563,7 +563,7 @@ private def computePackageRev (pkgDir : FilePath) : CliStateM String := do
   repo.getHeadRevision
 
 private def putCore
-  (rev : GitRev)  (outputs : FilePath) (artDir : FilePath)
+  (rev : String)  (outputs : FilePath) (artDir : FilePath)
   (service : CacheService) (scope : CacheServiceScope)
   (platform := CachePlatform.none) (toolchain := CacheToolchain.none)
 : LoggerIO Unit := do

src/lake/Lake/Config/Cache.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 import Init.Control.Do
-public import Lake.Util.Git
 public import Lake.Util.Log
 public import Lake.Util.Version
 public import Lake.Config.Artifact
@@ -470,7 +469,7 @@ public def readOutputs? (cache : Cache) (scope : String) (inputHash : Hash) : Lo
   cache.dir / "revisions"
 
 /-- Returns path to the input-to-output mappings of a downloaded package revision. -/
-@[inline] public def revisionPath (cache : Cache) (scope : String) (rev : GitRev) : FilePath :=
+@[inline] public def revisionPath (cache : Cache) (scope : String) (rev : String)   : FilePath :=
   cache.revisionDir / scope / s!"{rev}.jsonl"
 
 end Cache
@@ -943,7 +942,7 @@ public def uploadArtifacts
 public def mapContentType : String := "application/vnd.reservoir.outputs+json-lines"
 
 def s3RevisionUrl
-  (rev : GitRev) (service : CacheService) (scope : CacheServiceScope)
+  (rev : String) (service : CacheService) (scope : CacheServiceScope)
   (platform := CachePlatform.none) (toolchain := CacheToolchain.none)
 : String :=
   match scope.impl with
@@ -957,7 +956,7 @@ def s3RevisionUrl
     return s!"{url}/{rev}.jsonl"
 
 public def revisionUrl
-  (rev : GitRev) (service : CacheService) (scope : CacheServiceScope)
+  (rev : String) (service : CacheService) (scope : CacheServiceScope)
   (platform := CachePlatform.none) (toolchain := CacheToolchain.none)
 : String :=
   if service.isReservoir then Id.run do
@@ -975,7 +974,7 @@ public def revisionUrl
     service.s3RevisionUrl rev scope platform toolchain
 
 public def downloadRevisionOutputs?
-  (rev : GitRev) (cache : Cache) (service : CacheService)
+  (rev : String) (cache : Cache) (service : CacheService)
   (localScope : String) (remoteScope : CacheServiceScope)
   (platform := CachePlatform.none) (toolchain := CacheToolchain.none) (force := false)
 : LoggerIO (Option CacheMap) := do
@@ -999,7 +998,7 @@ public def downloadRevisionOutputs?
   CacheMap.load path platform.isNone
 
 public def uploadRevisionOutputs
-  (rev : GitRev) (outputs : FilePath) (service : CacheService) (scope : CacheServiceScope)
+  (rev : String) (outputs : FilePath) (service : CacheService) (scope : CacheServiceScope)
   (platform := CachePlatform.none) (toolchain := CacheToolchain.none)
 : LoggerIO Unit := do
   let url := service.s3RevisionUrl rev scope platform toolchain

src/lake/Lake/Config/Dependency.lean

@@ -9,7 +9,6 @@ prelude
 public import Init.Dynamic
 public import Init.System.FilePath
 public import Lean.Data.NameMap.Basic
-public import Lake.Util.Git
 import Init.Data.ToString.Name
 import Init.Data.ToString.Macro
 
@@ -31,7 +30,7 @@ public inductive DependencySrc where
 /- A package located at a fixed path relative to the dependent package's directory. -/
 | path (dir : FilePath)
 /- A package cloned from a Git repository available at a fixed Git `url`. -/
-| git (url : String) (rev : Option GitRev) (subDir : Option FilePath)
+| git (url : String) (rev : Option String) (subDir : Option FilePath)
 deriving Inhabited, Repr
 
 /--

src/lake/Lake/Config/Package.lean

@@ -52,8 +52,6 @@ public structure Package where
   remoteUrl : String
   /-- Dependency configurations for the package. -/
   depConfigs : Array Dependency := #[]
-  /-- **For internal use only.** Resolved direct dependences of the package. -/
-  depPkgs : Array Package := #[]
   /-- Target configurations in the order declared by the package. -/
   targetDecls : Array (PConfigDecl keyName) := #[]
   /-- Name-declaration map of target configurations in the package. -/

src/lake/Lake/Config/Workspace.lean

@@ -14,8 +14,6 @@ public import Lake.Config.TargetConfig
 public import Lake.Config.LakeConfig
 meta import Lake.Util.OpaqueType
 import Lean.DocString.Syntax
-import Init.Data.Range.Polymorphic.Iterators
-import Init.Data.Range.Polymorphic.Lemmas
 
 set_option doc.verso true
 
@@ -35,12 +33,14 @@ public def computeLakeCache (pkg : Package) (lakeEnv : Lake.Env) : Cache :=
     lakeEnv.lakeCache?.getD ⟨pkg.lakeDir / "cache"⟩
 
 public structure Workspace.Raw : Type where
+  /-- The root package of the workspace. -/
+  root : Package
   /-- The detected {lean}`Lake.Env` of the workspace. -/
   lakeEnv : Lake.Env
   /-- The Lake configuration from the system configuration file. -/
   lakeConfig : LoadedLakeConfig
   /-- The Lake cache. -/
-  lakeCache : Cache
+  lakeCache : Cache := private_decl% computeLakeCache root lakeEnv
   /--
   The CLI arguments Lake was run with.
   Used by {lit}`lake update` to perform a restart of Lake on a toolchain update.
@@ -59,31 +59,18 @@ public structure Workspace.Raw : Type where
   deriving Nonempty
 
 public structure Workspace.Raw.WF (ws : Workspace.Raw) : Prop where
-  size_packages_pos : 0 < ws.packages.size
   packages_wsIdx : ∀ (h : i < ws.packages.size), (ws.packages[i]'h).wsIdx = i
 
 /-- A Lake workspace -- the top-level package directory. -/
 public structure Workspace extends raw : Workspace.Raw, wf : raw.WF
 
-/-- Constructs an arbitrary well-formed workspace with {lean}`n` packages. -/
-noncomputable def Workspace.ofSize (n : Nat) (h : 0 < n) : Workspace := {
+public instance : Nonempty Workspace := .intro {
   lakeEnv := default
   lakeConfig := Classical.ofNonempty
-  lakeCache := Classical.ofNonempty
-  packages := (0...<n).toArray.map fun i =>
-    {(Classical.ofNonempty : Package) with wsIdx := i}
-  size_packages_pos := by
-    simp [Std.Rco.size, Std.Rxo.HasSize.size, Std.Rxc.HasSize.size, h]
-  packages_wsIdx {i} h := by
-    simp [Std.Rco.getElem_toArray_eq, Std.PRange.succMany?]
+  root := Classical.ofNonempty
+  packages_wsIdx h := by simp at h
 }
 
-theorem Workspace.size_packages_ofSize :
-  (ofSize n h).packages.size = n
-:= by simp [ofSize, Std.Rco.size, Std.Rxo.HasSize.size, Std.Rxc.HasSize.size]
-
-public instance : Nonempty Workspace := ⟨.ofSize 1 Nat.zero_lt_one⟩
-
 public hydrate_opaque_type OpaqueWorkspace Workspace
 
 /-- Returns the names of the root modules of the package's default targets. -/
@@ -98,18 +85,9 @@ public def Package.defaultTargetRoots (self : Package) : Array Lean.Name :=
 
 namespace Workspace
 
-/-- The root package of the workspace. -/
-@[inline] public def root (self : Workspace) : Package :=
-  self.packages[0]'self.size_packages_pos
-
-/-- **For internal use only.** -/
-public theorem wsIdx_root_lt {ws : Workspace} :
-  ws.root.wsIdx < ws.packages.size
-:= ws.packages_wsIdx _ ▸ ws.size_packages_pos
-
 /-- **For internal use.** Whether this workspace is Lean itself.  -/
-@[inline] def bootstrap (self : Workspace) : Bool :=
-  self.root.bootstrap
+@[inline] def bootstrap (ws : Workspace) : Bool :=
+  ws.root.bootstrap
 
 /-- The path to the workspace's directory (i.e., the directory of the root package). -/
 @[inline] public def dir (self : Workspace) : FilePath :=
@@ -215,18 +193,12 @@ This is configured through {lit}`cache.service` entries in the system Lake confi
   {self with
     packages := self.packages.push pkg
     packageMap := self.packageMap.insert pkg.keyName pkg
-    size_packages_pos := by simp
     packages_wsIdx {i} i_lt := by
       cases Nat.lt_add_one_iff_lt_or_eq.mp <| Array.size_push .. ▸ i_lt with
       | inl i_lt => simpa [Array.getElem_push_lt i_lt] using self.packages_wsIdx i_lt
       | inr i_eq => simpa [i_eq] using h
   }
 
-/-- **For internal use only.** -/
-public theorem packages_addPackage' :
-  (addPackage' pkg ws h).packages = ws.packages.push pkg
-:= by rfl
-
 /-- Add a package to the workspace. -/
 @[inline] public def addPackage (pkg : Package) (self : Workspace) : Workspace :=
   self.addPackage' {pkg with wsIdx := self.packages.size} rfl
@@ -306,11 +278,6 @@ public def findTargetDecl? (name : Name) (self : Workspace) : Option ((pkg : Pac
 @[inline] public def addFacetConfig {name} (cfg : FacetConfig name) (self : Workspace) : Workspace :=
   {self with facetConfigs := self.facetConfigs.insert cfg}
 
-/-- **For internal use only.** -/
-public theorem packages_addFacetConfig :
-  (addFacetConfig cfg ws).packages = ws.packages
-:= by rfl
-
 /-- Try to find a facet configuration in the workspace with the given name. -/
 @[inline] public def findFacetConfig? (name : Name) (self : Workspace) : Option (FacetConfig name) :=
   self.facetConfigs.get? name

src/lake/Lake/Load/Manifest.lean

@@ -8,7 +8,6 @@ module
 prelude
 public import Lake.Util.Version
 public import Lake.Config.Defaults
-public import Lake.Util.Git
 import Lake.Util.Error
 public import Lake.Util.FilePath
 import Lake.Util.JsonObject
@@ -76,8 +75,8 @@ public inductive PackageEntrySrc
   /-- A remote Git package. -/
   | git
     (url : String)
-    (rev : GitRev)
-    (inputRev? : Option GitRev)
+    (rev : String)
+    (inputRev? : Option String)
     (subDir? : Option FilePath)
   deriving Inhabited
 

src/lake/Lake/Load/Materialize.lean

@@ -13,8 +13,6 @@ import Lake.Util.Git
 import Lake.Util.IO
 import Lake.Reservoir
 
-set_option doc.verso true
-
 open System Lean
 
 /-! # Dependency Materialization
@@ -25,12 +23,9 @@ or resolve a local path dependency.
 
 namespace Lake
 
-/--
-Update the Git package in {lean}`repo` to the revision {lean}`rev?` if not already at it.
-IF no revision is specified (i.e., {lean}`rev? = none`), then uses the latest {lit}`master`.
--/
+/-- Update the Git package in `repo` to `rev` if not already at it. -/
 def updateGitPkg
-  (name : String) (repo : GitRepo) (rev? : Option GitRev)
+  (name : String) (repo : GitRepo) (rev? : Option String)
 : LoggerIO PUnit := do
   let rev ← repo.findRemoteRevision rev?
   if (← repo.getHeadRevision) = rev then
@@ -45,9 +40,9 @@ def updateGitPkg
     -- so stale ones from the previous revision cause incorrect trace computations.
     repo.clean
 
-/-- Clone the Git package as {lean}`repo`. -/
+/-- Clone the Git package as `repo`. -/
 def cloneGitPkg
-  (name : String) (repo : GitRepo) (url : String) (rev? : Option GitRev)
+  (name : String) (repo : GitRepo) (url : String) (rev? : Option String)
 : LoggerIO PUnit := do
   logInfo s!"{name}: cloning {url}"
   repo.clone url
@@ -57,9 +52,9 @@ def cloneGitPkg
     repo.checkoutDetach rev
 
 /--
-Update the Git repository from {lean}`url` in {lean}`repo` to {lean}`rev?`.
-If {lean}`repo` is already from {lean}`url`, just checkout the new revision.
-Otherwise, delete the local repository and clone a fresh copy from {lean}`url`.
+Update the Git repository from `url` in `repo` to `rev?`.
+If `repo` is already from `url`, just checkout the new revision.
+Otherwise, delete the local repository and clone a fresh copy from `url`.
 -/
 def updateGitRepo
   (name : String) (repo : GitRepo) (url : String) (rev? : Option String)
@@ -80,9 +75,8 @@ def updateGitRepo
       IO.FS.removeDirAll repo.dir
       cloneGitPkg name repo url rev?
 
-
 /--
-Materialize the Git repository from {lean}`url` into {lean}`repo` at {lean}`rev?`.
+Materialize the Git repository from `url` into `repo` at `rev?`.
 Clone it if no local copy exists, otherwise update it.
 -/
 def materializeGitRepo
@@ -120,11 +114,11 @@ namespace MaterializedDep
 @[inline] public def scope (self : MaterializedDep) : String :=
   self.manifestEntry.scope
 
-/-- Path to the dependency's manfiest file (relative to {lean}`relPkgDir`). -/
+/-- Path to the dependency's manfiest file (relative to `relPkgDir`). -/
 @[inline] public def relManifestFile? (self : MaterializedDep) : Option FilePath :=
   self.manifestEntry.manifestFile?
 
-/-- Path to the dependency's manfiest file (relative to {lean}`relPkgDir`). -/
+/-- Path to the dependency's manfiest file (relative to `relPkgDir`). -/
 @[inline] public def relManifestFile (self : MaterializedDep) : FilePath :=
   self.relManifestFile?.getD defaultManifestFile
 
@@ -132,7 +126,7 @@ namespace MaterializedDep
 @[inline] public def manifestFile (self : MaterializedDep) : FilePath :=
   self.pkgDir / self.relManifestFile
 
-/-- Path to the dependency's configuration file (relative to {lean}`relPkgDir`). -/
+/-- Path to the dependency's configuration file (relative to `relPkgDir`). -/
 @[inline] public def relConfigFile (self : MaterializedDep) : FilePath :=
   self.manifestEntry.configFile
 
@@ -149,7 +143,7 @@ end MaterializedDep
 
 inductive InputVer
 | none
-| git (rev : GitRev)
+| git (rev : String)
 | ver (ver : VerRange)
 
 def pkgNotIndexed (scope name : String) (ver : InputVer) : String :=

src/lake/Lake/Load/Resolve.lean

@@ -11,12 +11,10 @@ public import Lake.Load.Manifest
 import Lake.Util.IO
 import Lake.Util.StoreInsts
 import Lake.Config.Monad
+import Lake.Build.Topological
 import Lake.Load.Materialize
 import Lake.Load.Lean.Eval
 import Lake.Load.Package
-import Init.Data.Range.Polymorphic.Iterators
-import Init.TacticsExtra
-import Lean.Runtime
 
 open System Lean
 
@@ -47,108 +45,63 @@ namespace Lake
 def Workspace.addFacetDecls (decls : Array FacetDecl) (self : Workspace) : Workspace :=
   decls.foldl (·.addFacetConfig ·.config) self
 
-theorem Workspace.packages_addFacetDecls :
-  (addFacetDecls decls ws).packages = ws.packages
-:= by
-  simp only [addFacetDecls]
-  apply Array.foldl_induction (fun _ (s : Workspace) => s.packages = ws.packages) rfl
-  intro i s h
-  simp only [packages_addFacetConfig, h]
-
 /--
 Loads the package configuration of a materialized dependency.
 Adds the package and the facets defined within it to the `Workspace`.
 -/
-def Workspace.addDepPackage'
-  (ws : Workspace) (dep : MaterializedDep)
-  (lakeOpts : NameMap String) (leanOpts : Options) (reconfigure : Bool)
-: LogIO {ws' : Workspace // ws'.packages.size = ws.packages.size + 1} := do
+def addDepPackage
+  (dep : MaterializedDep)
+  (lakeOpts : NameMap String)
+  (leanOpts : Options) (reconfigure : Bool)
+: StateT Workspace LogIO Package := fun ws => do
   let wsIdx := ws.packages.size
   let loadCfg := mkDepLoadConfig ws dep lakeOpts leanOpts reconfigure
   let ⟨loadCfg, h⟩ ← resolveConfigFile dep.prettyName loadCfg
   let fileCfg ← loadConfigFile loadCfg h
   let pkg := mkPackage loadCfg fileCfg wsIdx
-  let ws := ws.addPackage' pkg wsIdx_mkPackage |>.addFacetDecls fileCfg.facetDecls
-  return ⟨ws, by simp [ws, packages_addFacetDecls, packages_addPackage']⟩
-
-
-def Workspace.setDepPkgs
-  (self : Workspace) (pkg : Package) (depPkgs : Array Package)
-  (h : pkg.wsIdx < self.packages.size)
-: Workspace :=
-  let pkg := {pkg with depPkgs}
-  {self with
-    packages := self.packages.set pkg.wsIdx pkg h
-    packageMap := self.packageMap.insert pkg.keyName pkg
-    size_packages_pos := by simp [self.size_packages_pos]
-    packages_wsIdx {i} := by
-      intro hi
-      rw [Array.size_set] at hi
-      rw [self.packages.getElem_set]
-      split
-      · assumption
-      · rw [self.packages_wsIdx]
-  }
-
-theorem Workspace.size_packages_setDepPkgs :
-  (setDepPkgs ws pkg depPkgs h).packages.size = ws.packages.size
-:= by simp [setDepPkgs]
-
-structure ResolveState (start : Nat) where
-  ws : Workspace
-  depIdxs : Array Nat
-  lt_of_mem : ∀ i ∈ depIdxs, i < ws.packages.size
-  start_le : start ≤ ws.packages.size
-
-namespace ResolveState
-
-@[inline] def init (ws : Workspace) (size : Nat) : ResolveState ws.packages.size :=
-  {ws, depIdxs := Array.mkEmpty size, lt_of_mem := by simp, start_le := Nat.le_refl ..}
-
-@[inline] def reuseDep (s : ResolveState n) (wsIdx : Fin s.ws.packages.size) : ResolveState n :=
-  have lt_of_mem := by
-    intro i i_mem
-    cases Array.mem_push.mp i_mem with
-    | inl i_mem => exact s.lt_of_mem i i_mem
-    | inr i_eq => simp only [i_eq, wsIdx.isLt]
-  {s with depIdxs := s.depIdxs.push wsIdx, lt_of_mem}
-
-@[inline] def newDep
-  (s : ResolveState n) (dep : MaterializedDep)
-  (lakeOpts : NameMap String) (leanOpts : Options) (reconfigure : Bool)
-: LogIO (ResolveState n) := do
-  let {ws, depIdxs, lt_of_mem, start_le} := s
-  let wsIdx := ws.packages.size
-  let ⟨ws', h⟩ ← ws.addDepPackage' dep lakeOpts leanOpts reconfigure
-  have lt_of_mem := by
-    intro i i_mem
-    cases Array.mem_push.mp i_mem with
-    | inl i_mem => exact h ▸ Nat.lt_add_one_of_lt (lt_of_mem i i_mem)
-    | inr i_eq => simp only [wsIdx, i_eq, h, Nat.lt_add_one]
-  have start_le := Nat.le_trans start_le <| h ▸ Nat.le_add_right ..
-  return ⟨ws', depIdxs.push wsIdx, lt_of_mem, start_le⟩
-
-end ResolveState
-
-abbrev MinWorkspace (ws : Workspace) :=
-  {ws' : Workspace // ws.packages.size ≤ ws'.packages.size}
-
-instance : Nonempty (MinWorkspace ws) := ⟨⟨ws, Nat.le_refl ..⟩⟩
-
-@[inline] unsafe def guardBySizeImpl [Pure m] [MonadError m] (as : Array α) : m (PLift (as.size ≤ Lean.maxSmallNat)) :=
-  pure ⟨lcProof⟩
+  let ws := ws.addPackage' pkg wsIdx_mkPackage
+  let ws := ws.addFacetDecls fileCfg.facetDecls
+  return (pkg, ws)
 
 /--
-Returns a proof that the size of an `Array` is at most `Lean.maxSmallNat`.
-
-This is modelled to fail via `MonadError` if this property does not hold. However, when compiled,
-this is implemented by a no-op, because this is a fixed property of the Lean runtime.
-
-This function can be used to prove that Array-bounded recursion terminates.
+The resolver's call stack of dependencies.
+That is, the dependency currently being resolved plus its parents.
 -/
-@[implemented_by guardBySizeImpl]
-def guardBySize! [Pure m] [MonadError m] (as : Array α) : m (PLift (as.size ≤ Lean.maxSmallNat)) :=
-  if h : as.size ≤ Lean.maxSmallNat then pure ⟨h⟩ else error "Array-bounded termination"
+abbrev DepStack := CallStack Name
+
+/--
+A monad transformer for recursive dependency resolution.
+It equips the monad with the stack of dependencies currently being resolved.
+-/
+abbrev DepStackT m := CallStackT Name m
+
+@[inline] nonrec def DepStackT.run
+  (x : DepStackT m α) (stack : DepStack := {})
+: m α := x.run stack
+
+/-- Log dependency cycle and error. -/
+@[specialize] def depCycleError [MonadError m] (cycle : Cycle Name) : m α :=
+  error s!"dependency cycle detected:\n{formatCycle cycle}"
+
+instance [Monad m] [MonadError m] : MonadCycleOf Name (DepStackT m) where
+  throwCycle := depCycleError
+
+/-- The monad of the dependency resolver. -/
+abbrev ResolveT m := DepStackT <| StateT Workspace m
+
+@[inline] nonrec def ResolveT.run
+  (ws : Workspace) (x : ResolveT m α) (stack : DepStack := {})
+: m (α × Workspace) := x.run stack |>.run ws
+
+/-- Recursively run a `ResolveT` monad starting from the workspace's root. -/
+@[specialize] def Workspace.runResolveT
+  [Monad m] [MonadError m] (ws : Workspace)
+  (go : RecFetchFn Package PUnit (ResolveT m))
+  (root := ws.root) (stack : DepStack  := {})
+: m Workspace := do
+  let (_, ws) ← ResolveT.run ws (stack := stack) do
+    recFetchAcyclic (·.baseName) go root
+  return ws
 
 /-
 Recursively visits each node in a package's dependency graph, starting from
@@ -163,51 +116,24 @@ See `Workspace.updateAndMaterializeCore` for more details.
 @[inline] def Workspace.resolveDepsCore
   [Monad m] [MonadError m] [MonadLiftT LogIO m] (ws : Workspace)
   (resolve : Package → Dependency → Workspace → m MaterializedDep)
-  (root : Nat := 0) (h : root < ws.packages.size := by exact ws.size_packages_pos)
+  (root : Package := ws.root) (stack : DepStack := {})
   (leanOpts : Options := {}) (reconfigure := true)
-: m (MinWorkspace ws) := do
-  go ws root h
+: m Workspace := do
+  ws.runResolveT go root stack
 where
-  @[specialize] go
-    (ws : Workspace) (wsIdx : Nat) (h : wsIdx < ws.packages.size)
-  : m (MinWorkspace ws) := do
-    let start := ws.packages.size
-    let pkg : Package := ws.packages[wsIdx]
-    have lt_start : pkg.wsIdx < start := ws.packages_wsIdx _ ▸ h
+  @[specialize] go pkg recurse : ResolveT m Unit := do
+    let start := (← getWorkspace).packages.size
     -- Materialize and load the missing direct dependencies of `pkg`
-    let s := ResolveState.init ws pkg.depConfigs.size
-    let ⟨ws, depIdxs, lt_of_mem, start_le⟩ ← pkg.depConfigs.foldrM (m := m) (init := s) fun dep s => do
-      if let some wsIdx := s.ws.packages.findFinIdx? (·.baseName == dep.name) then
-        return s.reuseDep wsIdx -- already handled in another branch
+    pkg.depConfigs.forRevM fun dep => do
+      let ws ← getWorkspace
+      if ws.packages.any (·.baseName == dep.name) then
+        return -- already handled in another branch
       if pkg.baseName = dep.name then
         error s!"{pkg.prettyName}: package requires itself (or a package with the same name)"
-      let matDep ← resolve pkg dep s.ws
-      s.newDep matDep dep.opts leanOpts reconfigure
+      let matDep ← resolve pkg dep (← getWorkspace)
+      discard <| addDepPackage matDep dep.opts leanOpts reconfigure
     -- Recursively load the dependencies' dependencies
-    let stop := ws.packages.size
-    let ⟨le_maxSmallNat⟩ ← guardBySize! ws.packages
-    let ⟨ws, stop_le⟩ ← id do
-      let mut ws' : {ws' : Workspace // stop ≤ ws'.packages.size} := ⟨ws, Nat.le_refl _⟩
-      for h_rco : wsIdx in (start...<stop) do
-        let ⟨ws, stop_le⟩ := ws'
-        have lt_stop := Std.Rco.lt_upper_of_mem h_rco
-        let ⟨ws, h⟩ ← go ws wsIdx <| Nat.lt_of_lt_of_le lt_stop stop_le
-        ws' := ⟨ws, Nat.le_trans stop_le h⟩
-      return ws'
-    have start_le := Nat.le_trans start_le stop_le
-    -- Add the package's dependencies to the package
-    let depPkgs := depIdxs.attach.map fun ⟨wsIdx, h_mem⟩ =>
-      ws.packages[wsIdx]'(Nat.lt_of_lt_of_le (lt_of_mem wsIdx h_mem) stop_le)
-    let ws := ws.setDepPkgs pkg depPkgs <| Nat.lt_of_lt_of_le lt_start start_le
-    have start_le := Nat.le_trans start_le <| by
-      simp [ws, Workspace.size_packages_setDepPkgs]
-    return ⟨ws, start_le⟩
-  termination_by Lean.maxSmallNat - wsIdx
-  decreasing_by
-    have start_le := Std.Rco.lower_le_of_mem h_rco
-    have lt_wsIdx := Nat.lt_of_lt_of_le h start_le
-    refine Nat.sub_lt_sub_left (Nat.lt_of_lt_of_le lt_wsIdx ?_) lt_wsIdx
-    exact Nat.le_trans (Nat.le_of_lt lt_stop) le_maxSmallNat
+    (← getWorkspace).packages.forM recurse start
 
 /--
 Adds monad state used to update the manifest.
@@ -438,40 +364,18 @@ def Workspace.updateAndMaterializeCore
 : LoggerIO (Workspace × NameMap PackageEntry) := UpdateT.run do
   reuseManifest ws toUpdate
   if updateToolchain then
-    let numDeps := ws.root.depConfigs.size
-    -- Update and materialize the top-level dependenciess
-    let deps : Vector _ numDeps := Vector.mk ws.root.depConfigs.reverse (by simp [numDeps])
+    let deps := ws.root.depConfigs.reverse
     let matDeps ← deps.mapM fun dep => do
       logVerbose s!"{ws.root.prettyName}: updating '{dep.name}' with {toJson dep.opts}"
       updateAndMaterializeDep ws ws.root dep
-    -- Update the toolchain based on the top-level dependenciess
-    ws.updateToolchain matDeps.toArray
-    -- Load the top-level dependenciess
+    ws.updateToolchain matDeps
     let start := ws.packages.size
-    let ⟨ws, h⟩ ← id do
-      let mut ws' : {ws : Workspace // start ≤ ws.packages.size} := ⟨ws, Nat.le_refl _⟩
-      for h : i in 0...<numDeps do
-        let matDep := matDeps[i]
-        addDependencyEntries matDep
-        let lakeOpts := deps[i].opts
-        let ⟨ws, h⟩ ← ws'.val.addDepPackage' matDep lakeOpts leanOpts true
-        ws' := ⟨ws, Nat.le_trans ws'.property <| by simp [h]⟩
-      return ws'
-    let stop := ws.packages.size
-    have start_le_stop : start ≤ stop := h
-    -- Resolve the top-level dependencies' dependencies'
-    let ⟨ws, _⟩ ← id do
-      let mut ws' : {ws : Workspace // stop ≤ ws.packages.size} := ⟨ws, Nat.le_refl _⟩
-      for h : wsIdx in start...<stop do
-        let ⟨ws, stop_le⟩ := ws'
-        have h := Nat.lt_of_lt_of_le (Std.Rco.lt_upper_of_mem h) stop_le
-        let ⟨ws, h⟩ ← ws.resolveDepsCore updateAndAddDep wsIdx h
-          (leanOpts := leanOpts) (reconfigure := true)
-        ws' := ⟨ws, Nat.le_trans stop_le h⟩
-      return ws'
-    -- Set dependency packages after `resolveDepsCore` so
-    -- that the dependencies' dependencies are also properly set
-    return ws.setDepPkgs ws.root ws.packages[start...<stop] ws.wsIdx_root_lt
+    let ws ← (deps.zip matDeps).foldlM (init := ws) fun ws (dep, matDep) => do
+      addDependencyEntries matDep
+      let (_, ws) ← addDepPackage matDep dep.opts leanOpts true ws
+      return ws
+    ws.packages.foldlM (init := ws) (start := start) fun ws pkg =>
+      ws.resolveDepsCore updateAndAddDep pkg [ws.root.baseName] leanOpts true
   else
     ws.resolveDepsCore updateAndAddDep (leanOpts := leanOpts) (reconfigure := true)
 where

src/lake/Lake/Load/Workspace.lean

@@ -35,22 +35,17 @@ public def loadWorkspaceRoot (config : LoadConfig) : LogIO Workspace := do
   let ⟨config, h⟩ ← resolveConfigFile "[root]" config
   let fileCfg ← loadConfigFile config h
   let root := mkPackage config fileCfg 0
-  have wsIdx_root : root.wsIdx = 0 := wsIdx_mkPackage
   let facetConfigs := fileCfg.facetDecls.foldl (·.insert ·.config) initFacetConfigs
-  return {
+  let ws : Workspace := {
+    root
     lakeEnv := config.lakeEnv
-    lakeCache := computeLakeCache root config.lakeEnv
     lakeConfig
     lakeArgs? := config.lakeArgs?
     facetConfigs
-    packages := #[root]
-    packageMap := DNameMap.empty.insert root.keyName root
-    size_packages_pos := by simp
-    packages_wsIdx {i} h := by
-      cases i with
-      | zero => simp [wsIdx_root]
-      | succ => simp at h
+    packages_wsIdx h := by simp at h
   }
+  let ws := ws.addPackage' root wsIdx_mkPackage
+  return ws
 
 /--
 Load a `Workspace` for a Lake package by

src/lake/Lake/Util/Git.lean

@@ -10,7 +10,6 @@ public import Init.Data.ToString
 public import Lake.Util.Proc
 import Init.Data.String.TakeDrop
 import Init.Data.String.Search
-import Lake.Util.String
 
 open System
 namespace Lake
@@ -37,48 +36,18 @@ public def filterUrl? (url : String) : Option String :=
     some url
 
 public def isFullObjectName (rev : String) : Bool :=
-  rev.utf8ByteSize == 40 && isHex rev
+  rev.length == 40 && rev.all fun c => c.isDigit || ('a' <= c && c <= 'f')
 
 end Git
 
 public structure GitRepo where
   dir : FilePath
 
-
-/--
-A commit-ish [Git revision][1].
-
-This can be SHA1 commit hash, a branch name, or one of Git's more complex specifiers.
-
-[1]: https://git-scm.com/docs/gitrevisions#_specifying_revisions
--/
-public abbrev GitRev := String
-
-namespace GitRev
-
-/-- The head revision (i.e., `HEAD`). -/
-@[expose] public def head : GitRev := "HEAD"
-
-/-- The revision fetched during the last `git fetch` (i.e., `FETCH_HEAD`). -/
-@[expose] public def fetchHead : GitRev := "FETCH_HEAD"
-
-/-- Returns whether this revision is a 40-digit hexadecimal (SHA1) commit hash. -/
-public def isFullSha1 (rev : GitRev) : Bool :=
-  rev.utf8ByteSize == 40 && isHex rev
-
-attribute [deprecated GitRev.isFullSha1 (since := "2026-04-17")] Git.isFullObjectName
-
-/-- Scopes the revision by the remote. -/
-@[inline] public def withRemote (remote : String) (rev : GitRev) : GitRev :=
-  s!"{remote}/{rev}"
-
-end GitRev
-
-namespace GitRepo
-
 public instance : Coe FilePath GitRepo := ⟨(⟨·⟩)⟩
 public instance : ToString GitRepo := ⟨(·.dir.toString)⟩
 
+namespace GitRepo
+
 public def cwd : GitRepo := ⟨"."⟩
 
 @[inline] public def dirExists (repo : GitRepo) : BaseIO Bool :=
@@ -102,18 +71,12 @@ public def clone (url : String) (repo : GitRepo) : LogIO PUnit  :=
 public def quietInit (repo : GitRepo) : LogIO PUnit  :=
   repo.execGit #["init", "-q"]
 
-public def bareInit (repo : GitRepo) : LogIO PUnit  :=
-  repo.execGit #["init", "--bare", "-q"]
-
 public def insideWorkTree (repo : GitRepo) : BaseIO Bool := do
   repo.testGit #["rev-parse", "--is-inside-work-tree"]
 
 public def fetch (repo : GitRepo) (remote := Git.defaultRemote) : LogIO PUnit  :=
   repo.execGit #["fetch", "--tags", "--force", remote]
 
-public def addWorktreeDetach (path : FilePath) (rev : GitRev) (repo : GitRepo) : LogIO PUnit :=
-  repo.execGit #["worktree", "add", "--detach", path.toString, rev]
-
 public def checkoutBranch (branch : String) (repo : GitRepo) : LogIO PUnit :=
   repo.execGit #["checkout", "-B", branch]
 
@@ -124,80 +87,60 @@ public def checkoutDetach (hash : String) (repo : GitRepo) : LogIO PUnit  :=
 public def clean (repo : GitRepo) : LogIO PUnit :=
   repo.execGit #["clean", "-xf"]
 
-/-- Resolves the revision to a Git object name (SHA1 hash) which or may not exist in the repository. -/
-public def resolveRevision? (rev : GitRev) (repo : GitRepo) : BaseIO (Option GitRev) := do
+public def resolveRevision? (rev : String) (repo : GitRepo) : BaseIO (Option String) := do
   repo.captureGit? #["rev-parse", "--verify", "--end-of-options", rev]
 
-/-- Resolves the revision to a valid commit hash within the repository. -/
-public def findCommit? (rev : GitRev) (repo : GitRepo) : BaseIO  (Option GitRev) := do
-  repo.captureGit? #["rev-parse", "--verify", "--end-of-options", rev ++ "^{commit}"]
-
-public def resolveRevision (rev : GitRev) (repo : GitRepo) : LogIO GitRev := do
-  if rev.isFullSha1 then return rev
+public def resolveRevision (rev : String) (repo : GitRepo) : LogIO String := do
+  if Git.isFullObjectName rev then return rev
   if let some rev ← repo.resolveRevision? rev then return rev
   error s!"{repo}: revision not found '{rev}'"
 
-@[inline] public def getHeadRevision? (repo : GitRepo) : BaseIO (Option GitRev) :=
-  repo.resolveRevision? .head
+@[inline] public def getHeadRevision? (repo : GitRepo) : BaseIO (Option String) :=
+  repo.resolveRevision? "HEAD"
 
-public def getHeadRevision (repo : GitRepo) : LogIO GitRev := do
+public def getHeadRevision (repo : GitRepo) : LogIO String := do
   if let some rev ← repo.getHeadRevision? then return rev
   error s!"{repo}: could not resolve 'HEAD' to a commit; \
     the repository may be corrupt, so you may need to remove it and try again"
 
-public def fetchRevision? (repo : GitRepo) (remote : String) (rev : GitRev) : LogIO (Option GitRev) := do
-  if (← repo.testGit #["fetch", "--tags", "--force", "--refetch", "--filter=tree:0", remote, rev]) then
-    let some rev ← repo.resolveRevision? .fetchHead
-      | error s!"{repo}: could not resolve 'FETCH_HEAD' to a commit after fetching; \
-          this may be an issue with Lake; please report it"
-    return rev
-  else
-    return none
-
-public def getHeadRevisions (repo : GitRepo) (n : Nat := 0) : LogIO (Array GitRev) := do
+public def getHeadRevisions (repo : GitRepo) (n : Nat := 0) : LogIO (Array String) := do
   let args := #["rev-list", "HEAD"]
   let args := if n != 0 then args ++ #["-n", toString n] else args
   let revs ← repo.captureGit args
   return revs.split '\n' |>.toStringArray
 
-public def resolveRemoteRevision (rev : GitRev) (remote := Git.defaultRemote) (repo : GitRepo) : LogIO GitRev := do
-  if rev.isFullSha1 then return rev
-  if let some rev ← repo.resolveRevision? (rev.withRemote remote) then return rev
+public def resolveRemoteRevision (rev : String) (remote := Git.defaultRemote) (repo : GitRepo) : LogIO String := do
+  if Git.isFullObjectName rev then return rev
+  if let some rev ← repo.resolveRevision? s!"{remote}/{rev}"  then return rev
   if let some rev ← repo.resolveRevision? rev then return rev
   error s!"{repo}: revision not found '{rev}'"
 
-public def findRemoteRevision (repo : GitRepo) (rev? : Option GitRev := none) (remote := Git.defaultRemote) : LogIO String := do
+public def findRemoteRevision (repo : GitRepo) (rev? : Option String := none) (remote := Git.defaultRemote) : LogIO String := do
   repo.fetch remote; repo.resolveRemoteRevision (rev?.getD Git.upstreamBranch) remote
 
-public def branchExists (rev : GitRev) (repo : GitRepo) : BaseIO Bool := do
+public def branchExists (rev : String) (repo : GitRepo) : BaseIO Bool := do
   repo.testGit #["show-ref", "--verify", s!"refs/heads/{rev}"]
 
-public def revisionExists (rev : GitRev) (repo : GitRepo) : BaseIO Bool := do
+public def revisionExists (rev : String) (repo : GitRepo) : BaseIO Bool := do
   repo.testGit #["rev-parse", "--verify", rev ++ "^{commit}"]
 
 public def getTags (repo : GitRepo) : BaseIO (List String) := do
   let some out ← repo.captureGit? #["tag"] | return []
   return out.split '\n' |>.toStringList
 
-public def findTag? (rev : GitRev := .head) (repo : GitRepo) : BaseIO (Option String) := do
+public def findTag? (rev : String := "HEAD") (repo : GitRepo) : BaseIO (Option String) := do
   repo.captureGit? #["describe", "--tags", "--exact-match", rev]
 
 public def getRemoteUrl?
   (remote := Git.defaultRemote) (repo : GitRepo)
-: BaseIO (Option String) := repo.captureGit? #["remote", "get-url", remote]
-
-public def addRemote (remote : String) (url : String) (repo : GitRepo) : LogIO Unit :=
-  repo.execGit #["remote", "add", remote, url]
-
-public def setRemoteUrl (remote : String) (url : String) (repo : GitRepo) : LogIO Unit :=
-  repo.execGit #["remote", "set-url", remote, url]
+: BaseIO (Option String) := do repo.captureGit? #["remote", "get-url", remote]
 
 public def getFilteredRemoteUrl?
   (remote := Git.defaultRemote) (repo : GitRepo)
 : BaseIO (Option String) := OptionT.run do Git.filterUrl? (← repo.getRemoteUrl? remote)
 
 public def hasNoDiff (repo : GitRepo) : BaseIO Bool := do
-  repo.testGit #["diff", "--exit-code", "HEAD"]
+  repo.testGit #["diff", "HEAD", "--exit-code"]
 
 @[inline] public def hasDiff (repo : GitRepo) : BaseIO Bool := do
   not <$> repo.hasNoDiff

src/lake/Lake/Util/String.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Data.ToString.Basic
-import Init.Data.UInt.Lemmas
 import Init.Data.String.Basic
 import Init.Data.Nat.Fold
 
@@ -34,38 +33,3 @@ public def isHex (s : String) : Bool :=
       65 ≤ c -- 'A'
     else
       false
-
-def lowerHexByte (n : UInt8) : UInt8 :=
-  if n ≤ 9 then
-    n + 48 -- + '0'
-  else
-    n + 87 -- + ('a' - 10)
-
-theorem isValidChar_of_lt_256 (h : n < 256) : isValidChar n :=
-  Or.inl <| Nat.lt_trans h (by decide)
-
-def lowerHexChar (n : UInt8) : Char :=
-  ⟨lowerHexByte n |>.toUInt32, isValidChar_of_lt_256 <|
-     UInt32.lt_iff_toNat_lt.mpr <| (lowerHexByte n).toNat_lt⟩
-
-public def lowerHexUInt64 (n : UInt64) : String :=
-  String.ofByteArray (ByteArray.emptyWithCapacity 16) ByteArray.isValidUTF8_empty
-  |>.push (lowerHexChar (n >>> 60 &&& 0xf).toUInt8)
-  |>.push (lowerHexChar (n >>> 56 &&& 0xf).toUInt8)
-  |>.push (lowerHexChar (n >>> 52 &&& 0xf).toUInt8)
-  |>.push (lowerHexChar (n >>> 48 &&& 0xf).toUInt8)
-  |>.push (lowerHexChar (n >>> 44 &&& 0xf).toUInt8)
-  |>.push (lowerHexChar (n >>> 40 &&& 0xf).toUInt8)
-  |>.push (lowerHexChar (n >>> 36 &&& 0xf).toUInt8)
-  |>.push (lowerHexChar (n >>> 32 &&& 0xf).toUInt8)
-  |>.push (lowerHexChar (n >>> 28 &&& 0xf).toUInt8)
-  |>.push (lowerHexChar (n >>> 24 &&& 0xf).toUInt8)
-  |>.push (lowerHexChar (n >>> 20 &&& 0xf).toUInt8)
-  |>.push (lowerHexChar (n >>> 16 &&& 0xf).toUInt8)
-  |>.push (lowerHexChar (n >>> 12 &&& 0xf).toUInt8)
-  |>.push (lowerHexChar (n >>> 8 &&& 0xf).toUInt8)
-  |>.push (lowerHexChar (n >>> 4 &&& 0xf).toUInt8)
-  |>.push (lowerHexChar (n &&& 0xf).toUInt8)
-
--- sanity check
-example : "0123456789abcdef" = lowerHexUInt64 0x0123456789abcdef := by decide