fix: case tactic in macros

We must erase macro scopes for tags in `case` as we do in `cases
.. with ..` and `induction .. with ..`.

RELEASES.md

@@ -8,7 +8,6 @@ This file contains work-in-progress notes for the upcoming release, as well as p
 Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status
 of each version.
 
-v4.8.0
 v4.9.0 (development in progress)
 ---------
 

doc/examples/test_single.sh

@@ -1,4 +1,4 @@
 #!/usr/bin/env bash
 source ../../tests/common.sh
 
-exec_check lean -Dlinter.all=false "$f"
+exec_check lean -j 0 -Dlinter.all=false "$f"

nix/bootstrap.nix

@@ -170,7 +170,7 @@ rec {
           ln -sf ${lean-all}/* .
         '';
         buildPhase = ''
-          ctest --output-junit test-results.xml --output-on-failure -E 'leancomptest_(doc_example|foreign)|leanlaketest_init' -j$NIX_BUILD_CORES
+          ctest --output-junit test-results.xml --output-on-failure -E 'leancomptest_(doc_example|foreign)' -j$NIX_BUILD_CORES
         '';
         installPhase = ''
           mkdir $out

src/CMakeLists.txt

@@ -11,7 +11,7 @@ project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
 set(LEAN_VERSION_MINOR 9)
 set(LEAN_VERSION_PATCH 0)
-set(LEAN_VERSION_IS_RELEASE 1)  # This number is 1 in the release revision, and 0 otherwise.
+set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
 set(LEAN_VERSION_STRING "${LEAN_VERSION_MAJOR}.${LEAN_VERSION_MINOR}.${LEAN_VERSION_PATCH}")
 if (LEAN_SPECIAL_VERSION_DESC)

src/Init/Data/BitVec/Lemmas.lean

@@ -9,7 +9,6 @@ import Init.Data.Bool
 import Init.Data.BitVec.Basic
 import Init.Data.Fin.Lemmas
 import Init.Data.Nat.Lemmas
-import Init.Data.Nat.Mod
 
 namespace BitVec
 
@@ -223,21 +222,9 @@ theorem toInt_eq_toNat_cond (i : BitVec n) :
       if 2*i.toNat < 2^n then
         (i.toNat : Int)
       else
-        (i.toNat : Int) - (2^n : Nat) :=
-  rfl
-
-theorem msb_eq_false_iff_two_mul_lt (x : BitVec w) : x.msb = false ↔ 2 * x.toNat < 2^w := by
-  cases w <;> simp [Nat.pow_succ, Nat.mul_comm _ 2, msb_eq_decide]
-
-theorem msb_eq_true_iff_two_mul_ge (x : BitVec w) : x.msb = true ↔ 2 * x.toNat ≥ 2^w := by
-  simp [← Bool.ne_false_iff, msb_eq_false_iff_two_mul_lt]
-
-/-- Characterize `x.toInt` in terms of `x.msb`. -/
-theorem toInt_eq_msb_cond (x : BitVec w) :
-    x.toInt = if x.msb then (x.toNat : Int) - (2^w : Nat) else (x.toNat : Int) := by
-  simp only [BitVec.toInt, ← msb_eq_false_iff_two_mul_lt]
-  cases x.msb <;> rfl
-
+        (i.toNat : Int) - (2^n : Nat) := by
+  unfold BitVec.toInt
+  split <;> omega
 
 theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) := by
   simp only [toInt_eq_toNat_cond]

src/Init/Data/String/Basic.lean

@@ -951,10 +951,6 @@ def beq (ss1 ss2 : Substring) : Bool :=
 
 instance hasBeq : BEq Substring := ⟨beq⟩
 
-/-- Checks whether two substrings have the same position and content. -/
-def sameAs (ss1 ss2 : Substring) : Bool :=
-  ss1.startPos == ss2.startPos && ss1 == ss2
-
 end Substring
 
 namespace String

src/Init/Prelude.lean

@@ -3644,17 +3644,6 @@ def getPos? (info : SourceInfo) (canonicalOnly := false) : Option String.Pos :=
   | synthetic (pos := pos) .., false => some pos
   | _,                         _     => none
 
-/--
-Gets the end position information from a `SourceInfo`, if available.
-If `originalOnly` is true, then `.synthetic` syntax will also return `none`.
--/
-def getTailPos? (info : SourceInfo) (canonicalOnly := false) : Option String.Pos :=
-  match info, canonicalOnly with
-  | original (endPos := endPos) ..,  _
-  | synthetic (endPos := endPos) (canonical := true) .., _
-  | synthetic (endPos := endPos) .., false => some endPos
-  | _,                               _     => none
-
 end SourceInfo
 
 /--

src/Init/System/IO.lean

@@ -264,13 +264,6 @@ local macro "nonempty_list" : tactic =>
 /-- Helper method for implementing "deterministic" timeouts. It is the number of "small" memory allocations performed by the current execution thread. -/
 @[extern "lean_io_get_num_heartbeats"] opaque getNumHeartbeats : BaseIO Nat
 
-/--
-Adjusts the heartbeat counter of the current thread by the given amount. This can be useful to give
-allocation-avoiding code additional "weight" and is also used to adjust the counter after resuming
-from a snapshot.
--/
-@[extern "lean_io_add_heartbeats"] opaque addHeartbeats (count : UInt64) : BaseIO Unit
-
 /--
 The mode of a file handle (i.e., a set of `open` flags and an `fdopen` mode).
 
@@ -793,32 +786,6 @@ instance : MonadLift (ST IO.RealWorld) BaseIO := ⟨id⟩
 def mkRef (a : α) : BaseIO (IO.Ref α) :=
   ST.mkRef a
 
-/--
-Mutable cell that can be passed around for purposes of cooperative task cancellation: request
-cancellation with `CancelToken.set` and check for it with `CancelToken.isSet`.
-
-This is a more flexible alternative to `Task.cancel` as the token can be shared between multiple
-tasks.
--/
-structure CancelToken where
-  private ref : IO.Ref Bool
-
-namespace CancelToken
-
-/-- Creates a new cancellation token. -/
-def new : BaseIO CancelToken :=
-  CancelToken.mk <$> IO.mkRef false
-
-/-- Activates a cancellation token. Idempotent. -/
-def set (tk : CancelToken) : BaseIO Unit :=
-  tk.ref.set true
-
-/-- Checks whether the cancellation token has been activated. -/
-def isSet (tk : CancelToken) : BaseIO Bool :=
-  tk.ref.get
-
-end CancelToken
-
 namespace FS
 namespace Stream
 

src/Lean/CoreM.lean

@@ -11,7 +11,6 @@ import Lean.Eval
 import Lean.ResolveName
 import Lean.Elab.InfoTree.Types
 import Lean.MonadEnv
-import Lean.Elab.Exception
 
 namespace Lean
 register_builtin_option diagnostics : Bool := {
@@ -86,13 +85,6 @@ structure Context where
   Use the `set_option diag true` to set it to true.
   -/
   diag           : Bool := false
-  /-- If set, used to cancel elaboration from outside when results are not needed anymore. -/
-  cancelTk?      : Option IO.CancelToken := none
-  /--
-  If set (when `showPartialSyntaxErrors` is not set and parsing failed), suppresses most elaboration
-  errors; see also `logMessage` below.
-  -/
-  suppressElabErrors : Bool := false
   deriving Nonempty
 
 /-- CoreM is a monad for manipulating the Lean environment.
@@ -209,45 +201,16 @@ instance : MonadTrace CoreM where
   getTraceState := return (← get).traceState
   modifyTraceState f := modify fun s => { s with traceState := f s.traceState }
 
-structure SavedState extends State where
-  /-- Number of heartbeats passed inside `withRestoreOrSaveFull`, not used otherwise. -/
-  passedHearbeats : Nat
-deriving Nonempty
-
-def saveState : CoreM SavedState := do
-  let s ← get
-  return { toState := s, passedHearbeats := 0 }
+/-- Restore backtrackable parts of the state. -/
+def restore (b : State) : CoreM Unit :=
+  modify fun s => { s with env := b.env, messages := b.messages, infoState := b.infoState }
 
 /--
-Incremental reuse primitive: if `reusableResult?` is `none`, runs `cont` with an action `save` that
-on execution returns the saved monadic state at this point including the heartbeats used by `cont`
-so far. If `reusableResult?` on the other hand is `some (a, state)`, restores full `state` including
-heartbeats used and returns `a`.
-
-The intention is for steps that support incremental reuse to initially pass `none` as
-`reusableResult?` and call `save` as late as possible in `cont`. In a further run, if reuse is
-possible, `reusableResult?` should be set to the previous state and result, ensuring that the state
-after running `withRestoreOrSaveFull` is identical in both runs. Note however that necessarily this
-is only an approximation in the case of heartbeats as heartbeats used by `withRestoreOrSaveFull`, by
-the remainder of `cont` after calling `save`, as well as by reuse-handling code such as the one
-supplying `reusableResult?` are not accounted for.
+Restores full state including sources for unique identifiers. Only intended for incremental reuse
+between elaboration runs, not for backtracking within a single run.
 -/
-@[specialize] def withRestoreOrSaveFull (reusableResult? : Option (α × SavedState))
-    (cont : (save : CoreM SavedState) → CoreM α) : CoreM α := do
-  if let some (val, state) := reusableResult? then
-    set state.toState
-    IO.addHeartbeats state.passedHearbeats.toUInt64
-    return val
-
-  let startHeartbeats ← IO.getNumHeartbeats
-  cont (do
-    let s ← get
-    let stopHeartbeats ← IO.getNumHeartbeats
-    return { toState := s, passedHearbeats := stopHeartbeats - startHeartbeats })
-
-/-- Restore backtrackable parts of the state. -/
-def SavedState.restore (b : SavedState) : CoreM Unit :=
-  modify fun s => { s with env := b.env, messages := b.messages, infoState := b.infoState }
+def restoreFull (b : State) : CoreM Unit :=
+  set b
 
 private def mkFreshNameImp (n : Name) : CoreM Name := do
   let fresh ← modifyGet fun s => (s.nextMacroScope, { s with nextMacroScope := s.nextMacroScope + 1 })
@@ -278,18 +241,10 @@ instance [MetaEval α] : MetaEval (CoreM α) where
 protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m α :=
   controlAt CoreM fun runInBase => withIncRecDepth (runInBase x)
 
-builtin_initialize interruptExceptionId : InternalExceptionId ← registerInternalExceptionId `interrupt
-
-/--
-Throws an internal interrupt exception if cancellation has been requested. The exception is not
-caught by `try catch` but is intended to be caught by `Command.withLoggingExceptions` at the top
-level of elaboration. In particular, we want to skip producing further incremental snapshots after
-the exception has been thrown.
- -/
 @[inline] def checkInterrupted : CoreM Unit := do
-  if let some tk := (← read).cancelTk? then
-    if (← tk.isSet) then
-      throw <| .internal interruptExceptionId
+  if (← IO.checkCanceled) then
+    -- should never be visible to users!
+    throw <| Exception.error .missing "elaboration interrupted"
 
 register_builtin_option debug.moduleNameAtTimeout : Bool := {
   defValue := true
@@ -334,13 +289,11 @@ def getMessageLog : CoreM MessageLog :=
   return (← get).messages
 
 /--
-Returns the current log and then resets its messages while adjusting `MessageLog.hadErrors`. Used
+Returns the current log and then resets its messages but does NOT reset `MessageLog.hadErrors`. Used
 for incremental reporting during elaboration of a single command.
 -/
 def getAndEmptyMessageLog : CoreM MessageLog :=
-  modifyGet fun s => (s.messages, { s with
-    messages.unreported := {}
-    messages.hadErrors  := s.messages.hasErrors })
+  modifyGet fun log => ({ log with msgs := {} }, log)
 
 instance : MonadLog CoreM where
   getRef      := getRef
@@ -348,12 +301,6 @@ instance : MonadLog CoreM where
   getFileName := return (← read).fileName
   hasErrors   := return (← get).messages.hasErrors
   logMessage msg := do
-    if (← read).suppressElabErrors then
-      -- discard elaboration errors, except for a few important and unlikely misleading ones, on
-      -- parse error
-      unless msg.data.hasTag (· matches `Elab.synthPlaceholder | `Tactic.unsolvedGoals) do
-        return
-
     let ctx ← read
     let msg := { msg with data := MessageData.withNamingContext { currNamespace := ctx.currNamespace, openDecls := ctx.openDecls } msg.data };
     modify fun s => { s with messages := s.messages.add msg }
@@ -461,26 +408,19 @@ def ImportM.runCoreM (x : CoreM α) : ImportM α := do
   let (a, _) ← (withOptions (fun _ => ctx.opts) x).toIO { fileName := "<ImportM>", fileMap := default } { env := ctx.env }
   return a
 
-/-- Return `true` if the exception was generated by one of our resource limits. -/
+/-- Return `true` if the exception was generated by one our resource limits. -/
 def Exception.isRuntime (ex : Exception) : Bool :=
   ex.isMaxHeartbeat || ex.isMaxRecDepth
 
-/-- Returns `true` if the exception is an interrupt generated by `checkInterrupted`. -/
-def Exception.isInterrupt : Exception → Bool
-  | Exception.internal id _ => id == Core.interruptExceptionId
-  | _ => false
-
 /--
-Custom `try-catch` for all monads based on `CoreM`. We usually don't want to catch "runtime
-exceptions" these monads, but on `CommandElabM`. See issues #2775 and #2744 as well as
-`MonadAlwaysExcept`. Also, we never want to catch interrupt exceptions inside the elaborator.
+Custom `try-catch` for all monads based on `CoreM`. We don't want to catch "runtime exceptions"
+in these monads, but on `CommandElabM`. See issues #2775 and #2744 as well as `MonadAlwayExcept`.
 -/
 @[inline] protected def Core.tryCatch (x : CoreM α) (h : Exception → CoreM α) : CoreM α := do
   try
     x
   catch ex =>
-    if ex.isInterrupt || ex.isRuntime then
-
+    if ex.isRuntime then
       throw ex -- We should use `tryCatchRuntimeEx` for catching runtime exceptions
     else
       h ex

src/Lean/Elab/Command.lean

@@ -47,9 +47,8 @@ structure Context where
   ref            : Syntax := Syntax.missing
   tacticCache?   : Option (IO.Ref Tactic.Cache)
   /--
-  Snapshot for incremental reuse and reporting of command elaboration. Currently only used for
-  (mutual) defs and contained tactics, in which case the `DynamicSnapshot` is a
-  `HeadersParsedSnapshot`.
+  Snapshot for incremental reuse and reporting of command elaboration. Currently unused in Lean
+  itself.
 
   Definitely resolved in `Language.Lean.process.doElab`.
 
@@ -57,13 +56,6 @@ structure Context where
   old elaboration are identical.
   -/
   snap?          : Option (Language.SnapshotBundle Language.DynamicSnapshot)
-  /-- Cancellation token forwarded to `Core.cancelTk?`. -/
-  cancelTk?      : Option IO.CancelToken
-  /--
-  If set (when `showPartialSyntaxErrors` is not set and parsing failed), suppresses most elaboration
-  errors; see also `logMessage` below.
-  -/
-  suppressElabErrors : Bool := false
 
 abbrev CommandElabCoreM (ε) := ReaderT Context $ StateRefT State $ EIO ε
 abbrev CommandElabM := CommandElabCoreM Exception
@@ -81,21 +73,6 @@ Remark: see comment at TermElabM
 @[always_inline]
 instance : Monad CommandElabM := let i := inferInstanceAs (Monad CommandElabM); { pure := i.pure, bind := i.bind }
 
-/-- Like `Core.tryCatch` but do catch runtime exceptions. -/
-@[inline] protected def tryCatch (x : CommandElabM α) (h : Exception → CommandElabM α) :
-    CommandElabM α := do
-  try
-    x
-  catch ex =>
-    if ex.isInterrupt then
-      throw ex
-    else
-      h ex
-
-instance : MonadExceptOf Exception CommandElabM where
-  throw    := throw
-  tryCatch := Command.tryCatch
-
 def mkState (env : Environment) (messages : MessageLog := {}) (opts : Options := {}) : State := {
   env         := env
   messages    := messages
@@ -183,18 +160,17 @@ private def runCore (x : CoreM α) : CommandElabM α := do
   let env := Kernel.resetDiag s.env
   let scope := s.scopes.head!
   let coreCtx : Core.Context := {
-    fileName           := ctx.fileName
-    fileMap            := ctx.fileMap
-    currRecDepth       := ctx.currRecDepth
-    maxRecDepth        := s.maxRecDepth
-    ref                := ctx.ref
-    currNamespace      := scope.currNamespace
-    openDecls          := scope.openDecls
-    initHeartbeats     := heartbeats
-    currMacroScope     := ctx.currMacroScope
-    options            := scope.opts
-    cancelTk?          := ctx.cancelTk?
-    suppressElabErrors := ctx.suppressElabErrors }
+    fileName       := ctx.fileName
+    fileMap        := ctx.fileMap
+    currRecDepth   := ctx.currRecDepth
+    maxRecDepth    := s.maxRecDepth
+    ref            := ctx.ref
+    currNamespace  := scope.currNamespace
+    openDecls      := scope.openDecls
+    initHeartbeats := heartbeats
+    currMacroScope := ctx.currMacroScope
+    options        := scope.opts
+  }
   let x : EIO _ _ := x.run coreCtx {
     env
     ngen := s.ngen
@@ -239,11 +215,6 @@ instance : MonadLog CommandElabM where
   getFileName := return (← read).fileName
   hasErrors   := return (← get).messages.hasErrors
   logMessage msg := do
-    if (← read).suppressElabErrors then
-      -- discard elaboration errors on parse error
-      -- NOTE: unlike `CoreM`'s `logMessage`, we do not currently have any command-level errors that
-      -- we want to allowlist
-      return
     let currNamespace ← getCurrNamespace
     let openDecls ← getOpenDecls
     let msg := { msg with data := MessageData.withNamingContext { currNamespace := currNamespace, openDecls := openDecls } msg.data }
@@ -350,19 +321,11 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
 
 builtin_initialize registerTraceClass `Elab.input
 
-/-- Option for showing elaboration errors from partial syntax errors. -/
-register_builtin_option showPartialSyntaxErrors : Bool := {
-  defValue := false
-  descr    := "show elaboration errors from partial syntax trees (i.e. after parser recovery)"
-}
-
 /--
 `elabCommand` wrapper that should be used for the initial invocation, not for recursive calls after
 macro expansion etc.
 -/
 def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do profileitM Exception "elaboration" (← getOptions) do
-  withReader ({ · with suppressElabErrors :=
-    stx.hasMissing && !showPartialSyntaxErrors.get (← getOptions) }) do
   let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
   let initInfoTrees ← getResetInfoTrees
   try
@@ -499,12 +462,7 @@ def runTermElabM (elabFn : Array Expr → TermElabM α) : CommandElabM α := do
           Term.addAutoBoundImplicits' xs someType fun xs _ =>
             Term.withoutAutoBoundImplicit <| elabFn xs
 
-/--
-Catches and logs exceptions occurring in `x`. Unlike `try catch` in `CommandElabM`, this function
-catches interrupt exceptions as well and thus is intended for use at the top level of elaboration.
-Interrupt and abort exceptions are caught but not logged.
--/
-@[inline] def withLoggingExceptions (x : CommandElabM Unit) : CommandElabCoreM Empty Unit := fun ctx ref =>
+@[inline] def catchExceptions (x : CommandElabM Unit) : CommandElabCoreM Empty Unit := fun ctx ref =>
   EIO.catchExceptions (withLogging x ctx ref) (fun _ => pure ())
 
 private def liftAttrM {α} (x : AttrM α) : CommandElabM α := do
@@ -570,7 +528,6 @@ def liftCommandElabM (cmd : CommandElabM α) : CoreM α := do
       ref := ← getRef
       tacticCache? := none
       snap? := none
-      cancelTk? := (← read).cancelTk?
     } |>.run {
       env := ← getEnv
       maxRecDepth := ← getMaxRecDepth
@@ -580,7 +537,7 @@ def liftCommandElabM (cmd : CommandElabM α) : CoreM α := do
     traceState.traces := coreState.traceState.traces ++ commandState.traceState.traces
     env := commandState.env
   }
-  if let some err := commandState.messages.toArray.find? (·.severity matches .error) then
+  if let some err := commandState.messages.msgs.toArray.find? (·.severity matches .error) then
     throwError err.data
   pure a
 

src/Lean/Elab/DefView.lean

@@ -28,81 +28,6 @@ def DefKind.isExample : DefKind → Bool
   | .example => true
   | _        => false
 
-/-- Header elaboration data of a `DefView`. -/
-structure DefViewElabHeaderData where
-  /--
-    Short name. Recall that all declarations in Lean 4 are potentially recursive. We use `shortDeclName` to refer
-    to them at `valueStx`, and other declarations in the same mutual block. -/
-  shortDeclName : Name
-  /-- Full name for this declaration. This is the name that will be added to the `Environment`. -/
-  declName      : Name
-  /-- Universe level parameter names explicitly provided by the user. -/
-  levelNames    : List Name
-  /-- Syntax objects for the binders occurring before `:`, we use them to populate the `InfoTree` when elaborating `valueStx`. -/
-  binderIds     : Array Syntax
-  /-- Number of parameters before `:`, it also includes auto-implicit parameters automatically added by Lean. -/
-  numParams     : Nat
-  /-- Type including parameters. -/
-  type          : Expr
-deriving Inhabited
-
-section Snapshots
-open Language
-
-/-- Snapshot after processing of a definition body.  -/
-structure BodyProcessedSnapshot extends Language.Snapshot where
-  /-- State after elaboration. -/
-  state : Term.SavedState
-  /-- Elaboration result. -/
-  value : Expr
-deriving Nonempty
-instance : Language.ToSnapshotTree BodyProcessedSnapshot where
-  toSnapshotTree s := ⟨s.toSnapshot, #[]⟩
-
-/-- Snapshot after elaboration of a definition header. -/
-structure HeaderProcessedSnapshot extends Language.Snapshot where
-  /-- Elaboration results. -/
-  view : DefViewElabHeaderData
-  /-- Resulting elaboration state, including any environment additions. -/
-  state : Term.SavedState
-  /-- Syntax of top-level tactic block if any, for checking reuse of `tacSnap?`. -/
-  tacStx? : Option Syntax
-  /-- Incremental execution of main tactic block, if any. -/
-  tacSnap? : Option (SnapshotTask Tactic.TacticParsedSnapshot)
-  /-- Syntax of definition body, for checking reuse of `bodySnap`. -/
-  bodyStx : Syntax
-  /-- Result of body elaboration. -/
-  bodySnap : SnapshotTask (Option BodyProcessedSnapshot)
-deriving Nonempty
-instance : Language.ToSnapshotTree HeaderProcessedSnapshot where
-  toSnapshotTree s := ⟨s.toSnapshot,
-    (match s.tacSnap? with
-      | some tac => #[tac.map (sync := true) toSnapshotTree]
-      | none     => #[]) ++
-    #[s.bodySnap.map (sync := true) toSnapshotTree]⟩
-
-/-- State before elaboration of a mutual definition. -/
-structure DefParsed where
-  /--
-  Input substring uniquely identifying header elaboration result given the same `Environment`.
-  If missing, results should never be reused.
-  -/
-  headerSubstr? : Option Substring
-  /-- Elaboration result, unless fatal exception occurred. -/
-  headerProcessedSnap : SnapshotTask (Option HeaderProcessedSnapshot)
-deriving Nonempty
-
-/-- Snapshot after syntax tree has been split into separate mutual def headers. -/
-structure DefsParsedSnapshot extends Language.Snapshot where
-  /-- Definitions of this mutual block. -/
-  defs : Array DefParsed
-deriving Nonempty, TypeName
-instance : Language.ToSnapshotTree DefsParsedSnapshot where
-  toSnapshotTree s := ⟨s.toSnapshot,
-    s.defs.map (·.headerProcessedSnap.map (sync := true) toSnapshotTree)⟩
-
-end Snapshots
-
 structure DefView where
   kind          : DefKind
   ref           : Syntax
@@ -111,13 +36,6 @@ structure DefView where
   binders       : Syntax
   type?         : Option Syntax
   value         : Syntax
-  /--
-  Snapshot for incremental processing of this definition.
-
-  Invariant: If the bundle's `old?` is set, then elaboration of the header is guaranteed to result
-  in the same elaboration result and state, i.e. reuse is possible.
-  -/
-  headerSnap?   : Option (Language.SnapshotBundle (Option HeaderProcessedSnapshot)) := none
   deriving?     : Option (Array Syntax) := none
   deriving Inhabited
 

src/Lean/Elab/Exception.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.InternalExceptionId
-import Lean.Exception
+import Lean.Meta.Basic
 
 namespace Lean.Elab
 

src/Lean/Elab/Frontend.lean

@@ -16,7 +16,6 @@ structure State where
   parserState  : Parser.ModuleParserState
   cmdPos       : String.Pos
   commands     : Array Syntax := #[]
-deriving Nonempty
 
 structure Context where
   inputCtx : Parser.InputContext
@@ -35,7 +34,6 @@ def setCommandState (commandState : Command.State) : FrontendM Unit :=
     fileMap      := ctx.inputCtx.fileMap
     tacticCache? := none
     snap?        := none
-    cancelTk?    := none
   }
   match (← liftM <| EIO.toIO' <| (x cmdCtx).run s.commandState) with
   | Except.error e      => throw <| IO.Error.userError s!"unexpected internal error: {← e.toMessageData.toString}"
@@ -46,6 +44,15 @@ def elabCommandAtFrontend (stx : Syntax) : FrontendM Unit := do
     let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
     Command.elabCommandTopLevel stx
     let mut msgs := (← get).messages
+    -- `stx.hasMissing` should imply `initMsgs.hasErrors`, but the latter should be cheaper to check
+    -- in general
+    if !Language.Lean.showPartialSyntaxErrors.get (← getOptions) && initMsgs.hasErrors &&
+        stx.hasMissing then
+      -- discard elaboration errors, except for a few important and unlikely misleading ones, on
+      -- parse error
+      msgs := ⟨msgs.msgs.filter fun msg =>
+        msg.data.hasTag (fun tag => tag == `Elab.synthPlaceholder ||
+          tag == `Tactic.unsolvedGoals || (`_traceMsg).isSuffixOf tag)⟩
     modify ({ · with messages := initMsgs ++ msgs })
 
 def updateCmdPos : FrontendM Unit := do
@@ -85,47 +92,6 @@ def IO.processCommands (inputCtx : Parser.InputContext) (parserState : Parser.Mo
   let (_, s) ← (Frontend.processCommands.run { inputCtx := inputCtx }).run { commandState := commandState, parserState := parserState, cmdPos := parserState.pos }
   pure s
 
-structure IncrementalState extends State where
-  inputCtx    : Parser.InputContext
-  initialSnap : Language.Lean.CommandParsedSnapshot
-deriving Nonempty
-
-open Language in
-/--
-Variant of `IO.processCommands` that uses the new Lean language processor implementation for
-potential incremental reuse. Pass in result of a previous invocation done with the same state
-(but usually different input context) to allow for reuse.
--/
--- `IO.processCommands` can be reimplemented on top of this as soon as the additional tasks speed up
--- things instead of slowing them down
-partial def IO.processCommandsIncrementally (inputCtx : Parser.InputContext)
-    (parserState : Parser.ModuleParserState) (commandState : Command.State)
-    (old? : Option IncrementalState) :
-    BaseIO IncrementalState := do
-  let task ← Language.Lean.processCommands inputCtx parserState commandState
-    (old?.map fun old => (old.inputCtx, old.initialSnap))
-  go task.get task #[]
-where
-  go initialSnap t commands :=
-    let snap := t.get
-    let commands := commands.push snap.data.stx
-    if let some next := snap.nextCmdSnap? then
-      go initialSnap next commands
-    else
-      -- Opting into reuse also enables incremental reporting, so make sure to collect messages from
-      -- all snapshots
-      let messages := toSnapshotTree initialSnap
-        |>.getAll.map (·.diagnostics.msgLog)
-        |>.foldl (· ++ ·) {}
-      let trees := toSnapshotTree initialSnap
-        |>.getAll.map (·.infoTree?) |>.filterMap id |>.toPArray'
-      return {
-        commandState := { snap.data.finishedSnap.get.cmdState with messages, infoState.trees := trees }
-        parserState := snap.data.parserState
-        cmdPos := snap.data.parserState.pos
-        inputCtx, initialSnap, commands
-      }
-
 def process (input : String) (env : Environment) (opts : Options) (fileName : Option String := none) : IO (Environment × MessageLog) := do
   let fileName   := fileName.getD "<input>"
   let inputCtx   := Parser.mkInputContext input fileName
@@ -147,7 +113,8 @@ def runFrontend
     : IO (Environment × Bool) := do
   let startTime := (← IO.monoNanosNow).toFloat / 1000000000
   let inputCtx := Parser.mkInputContext input fileName
-  if true then
+  -- TODO: replace with `#lang` processing
+  if /- Lean #lang? -/ true then
     -- Temporarily keep alive old cmdline driver for the Lean language so that we don't pay the
     -- overhead of passing the environment between snapshots until we actually make good use of it
     -- outside the server

src/Lean/Elab/MutualDef.lean

@@ -20,24 +20,28 @@ import Lean.Elab.DeclarationRange
 namespace Lean.Elab
 open Lean.Parser.Term
 
-open Language
-
-/-- `DefView` plus header elaboration data and snapshot. -/
-structure DefViewElabHeader extends DefView, DefViewElabHeaderData where
+/-- `DefView` after elaborating the header. -/
+structure DefViewElabHeader where
+  ref           : Syntax
+  modifiers     : Modifiers
+  /-- Stores whether this is the header of a definition, theorem, ... -/
+  kind          : DefKind
   /--
-  Snapshot for incremental processing of top-level tactic block, if any.
-
-  Invariant: if the bundle's `old?` is set, then the state *up to the start* of the tactic block is
-  unchanged, i.e. reuse is possible.
-  -/
-  tacSnap? : Option (Language.SnapshotBundle Tactic.TacticParsedSnapshot)
-  /--
-  Snapshot for incremental processing of definition body.
-
-  Invariant: if the bundle's `old?` is set, then elaboration of the body is guaranteed to result in
-  the same elaboration result and state, i.e. reuse is possible.
-  -/
-  bodySnap? : Option (Language.SnapshotBundle (Option BodyProcessedSnapshot))
+    Short name. Recall that all declarations in Lean 4 are potentially recursive. We use `shortDeclName` to refer
+    to them at `valueStx`, and other declarations in the same mutual block. -/
+  shortDeclName : Name
+  /-- Full name for this declaration. This is the name that will be added to the `Environment`. -/
+  declName      : Name
+  /-- Universe level parameter names explicitly provided by the user. -/
+  levelNames    : List Name
+  /-- Syntax objects for the binders occurring before `:`, we use them to populate the `InfoTree` when elaborating `valueStx`. -/
+  binderIds     : Array Syntax
+  /-- Number of parameters before `:`, it also includes auto-implicit parameters automatically added by Lean. -/
+  numParams     : Nat
+  /-- Type including parameters. -/
+  type          : Expr
+  /-- `Syntax` object the body/value of the definition. -/
+  valueStx      : Syntax
   deriving Inhabited
 
 namespace Term
@@ -123,65 +127,14 @@ private def cleanupOfNat (type : Expr) : MetaM Expr := do
     let eNew := mkApp e.appFn! argArgs[1]!
     return .done eNew
 
-/--
-Elaborates only the declaration view headers. We have to elaborate the headers first because we
-support mutually recursive declarations in Lean 4.
--/
-private def elabHeaders (views : Array DefView)
-    (bodyPromises : Array (IO.Promise (Option BodyProcessedSnapshot)))
-    (tacPromises : Array (IO.Promise Tactic.TacticParsedSnapshot)) :
-    TermElabM (Array DefViewElabHeader) := do
+/-- Elaborate only the declaration headers. We have to elaborate the headers first because we support mutually recursive declarations in Lean 4. -/
+private def elabHeaders (views : Array DefView) : TermElabM (Array DefViewElabHeader) := do
   let expandedDeclIds ← views.mapM fun view => withRef view.ref do
     Term.expandDeclId (← getCurrNamespace) (← getLevelNames) view.declId view.modifiers
   withAutoBoundImplicitForbiddenPred (fun n => expandedDeclIds.any (·.shortName == n)) do
     let mut headers := #[]
-    -- Can we reuse the result for a body? For starters, all headers (even those below the body)
-    -- must be reusable
-    let mut reuseBody := views.all (·.headerSnap?.any (·.old?.isSome))
-    for view in views, ⟨shortDeclName, declName, levelNames⟩ in expandedDeclIds,
-        tacPromise in tacPromises, bodyPromise in bodyPromises do
-      let mut reusableResult? := none
-      if let some snap := view.headerSnap? then
-        -- by the `DefView.headerSnap?` invariant, safe to reuse results at this point, so let's
-        -- wait for them!
-        if let some old := snap.old?.bind (·.val.get) then
-          let (tacStx?, newTacTask?) ← mkTacTask view.value tacPromise
-          snap.new.resolve <| some { old with
-            tacStx?
-            tacSnap? := newTacTask?
-            bodyStx := view.value
-            bodySnap := mkBodyTask view.value bodyPromise
-          }
-          -- Transition from `DefView.snap?` to `DefViewElabHeader.tacSnap?` invariant: if all
-          -- headers and all previous bodies could be reused, then the state at the *start* of the
-          -- top-level tactic block (if any) is unchanged
-          let reuseTac := reuseBody
-          -- Transition from `DefView.snap?` to `DefViewElabHeader.bodySnap?` invariant: if all
-          -- headers and all previous bodies could be reused and this body syntax is unchanged, then
-          -- we can reuse the result
-          reuseBody := reuseBody &&
-            view.value.structRangeEqWithTraceReuse (← getOptions) old.bodyStx
-          let header := { old.view, view with
-            -- We should only forward the promise if we are actually waiting on the corresponding
-            -- task; otherwise, diagnostics assigned to it will be lost
-            tacSnap? := guard newTacTask?.isSome *> some {
-              old? := do
-                guard reuseTac
-                some ⟨(← old.tacStx?), (← old.tacSnap?)⟩
-              new := tacPromise
-            }
-            bodySnap? := some {
-              -- no syntax guard to store, we already did the necessary checks
-              old? := guard reuseBody *> pure ⟨.missing, old.bodySnap⟩
-              new := bodyPromise
-            }
-          }
-          reusableResult? := some (header, old.state)
-        else
-          reuseBody := false
-
-      let header ← withRestoreOrSaveFull reusableResult? fun save => do
-        withRef view.ref do
+    for view in views, ⟨shortDeclName, declName, levelNames⟩ in expandedDeclIds do
+      let newHeader ← withRef view.ref do
         addDeclarationRanges declName view.ref
         applyAttributesAt declName view.modifiers.attrs .beforeElaboration
         withDeclName declName <| withAutoBoundImplicit <| withLevelNames levelNames <|
@@ -211,62 +164,21 @@ private def elabHeaders (views : Array DefView)
               let pendingMVarIds ← getMVars type
               discard <| logUnassignedUsingErrorInfos pendingMVarIds <|
                 getPendindMVarErrorMessage views
-            let newHeader : DefViewElabHeaderData := {
-              declName, shortDeclName, type, levelNames, binderIds
-              numParams := xs.size
-            }
-            let mut newHeader : DefViewElabHeader := { view, newHeader with
-              bodySnap? := none, tacSnap? := none }
-            if let some snap := view.headerSnap? then
-              let (tacStx?, newTacTask?) ← mkTacTask view.value tacPromise
-              snap.new.resolve <| some {
-                diagnostics :=
-                  (← Language.Snapshot.Diagnostics.ofMessageLog (← Core.getAndEmptyMessageLog))
-                view := newHeader.toDefViewElabHeaderData
-                state := (← save)
-                tacStx?
-                tacSnap? := newTacTask?
-                bodyStx := view.value
-                bodySnap := mkBodyTask view.value bodyPromise
-              }
-              newHeader := { newHeader with
-                -- We should only forward the promise if we are actually waiting on the
-                -- corresponding task; otherwise, diagnostics assigned to it will be lost
-                tacSnap? := guard newTacTask?.isSome *> some { old? := none, new := tacPromise }
-                bodySnap? := some { old? := none, new := bodyPromise }
-              }
+            let newHeader := {
+              ref           := view.ref
+              modifiers     := view.modifiers
+              kind          := view.kind
+              shortDeclName := shortDeclName
+              declName, type, levelNames, binderIds
+              numParams     := xs.size
+              valueStx      := view.value : DefViewElabHeader }
             check headers newHeader
             return newHeader
-      headers := headers.push header
+      headers := headers.push newHeader
     return headers
-where
-  getBodyTerm? (stx : Syntax) : Option Syntax :=
-    -- TODO: does not work with partial syntax
-    --| `(Parser.Command.declVal| := $body $_suffix:suffix $[$_where]?) => body
-    guard (stx.isOfKind ``Parser.Command.declValSimple) *> some stx[1]
-
-  /-- Creates snapshot task with appropriate range from body syntax and promise. -/
-  mkBodyTask (body : Syntax) (new : IO.Promise (Option BodyProcessedSnapshot)) :
-      Language.SnapshotTask (Option BodyProcessedSnapshot) :=
-    let rangeStx := getBodyTerm? body |>.getD body
-    { range? := rangeStx.getRange?, task := new.result }
-
-  /--
-  If `body` allows for incremental tactic reporting and reuse, creates a snapshot task out of the
-  passed promise with appropriate range, otherwise immediately resolves the promise to a dummy
-  value.
-  -/
-  mkTacTask (body : Syntax) (tacPromise : IO.Promise Tactic.TacticParsedSnapshot) :
-      TermElabM (Option Syntax × Option (Language.SnapshotTask Tactic.TacticParsedSnapshot))
-   := do
-    if let some e := getBodyTerm? body then
-      if let `(by $tacs*) := e then
-        return (e, some { range? := mkNullNode tacs |>.getRange?, task := tacPromise.result })
-    tacPromise.resolve default
-    return (none, none)
 
 /--
-  Create auxiliary local declarations `fs` for the given headers using their `shortDeclName` and `type`, given headers, and execute `k fs`.
+  Create auxiliary local declarations `fs` for the given hearders using their `shortDeclName` and `type`, given hearders, and execute `k fs`.
   The new free variables are tagged as `auxDecl`.
   Remark: `fs.size = headers.size`.
 -/
@@ -338,44 +250,15 @@ private def declValToTerminationHint (declVal : Syntax) : TermElabM WF.Terminati
     return .none
 
 private def elabFunValues (headers : Array DefViewElabHeader) : TermElabM (Array Expr) :=
-  headers.mapM fun header => do
-    let mut reusableResult? := none
-    if let some snap := header.bodySnap? then
-      if let some old := snap.old? then
-        -- guaranteed reusable as by the `bodySnap?` invariant, so let's wait on the previous
-        -- elaboration
-        if let some old := old.val.get then
-          snap.new.resolve <| some old
-          -- also make sure to reuse tactic snapshots if present so that body reuse does not lead to
-          -- missed tactic reuse on further changes
-          if let some tacSnap := header.tacSnap? then
-            if let some oldTacSnap := tacSnap.old? then
-              tacSnap.new.resolve oldTacSnap.val.get
-          reusableResult? := some (old.value, old.state)
-
-    withRestoreOrSaveFull reusableResult? fun save => do
-      withDeclName header.declName <| withLevelNames header.levelNames do
-      let valStx ← liftMacroM <| declValToTerm header.value
-      forallBoundedTelescope header.type header.numParams fun xs type => do
-        -- Add new info nodes for new fvars. The server will detect all fvars of a binder by the binder's source location.
-        for i in [0:header.binderIds.size] do
-          -- skip auto-bound prefix in `xs`
-          addLocalVarInfo header.binderIds[i]! xs[header.numParams - header.binderIds.size + i]!
-        let val ← withReader ({ · with tacSnap? := header.tacSnap? }) do
-          -- synthesize mvars here to force the top-level tactic block (if any) to run
-          elabTermEnsuringType valStx type <* synthesizeSyntheticMVarsNoPostponing
-        -- NOTE: without this `instantiatedMVars`, `mkLambdaFVars` may leave around a redex that
-        -- leads to more section variables being included than necessary
-        let val ← instantiateMVars val
-        let val ← mkLambdaFVars xs val
-        if let some snap := header.bodySnap? then
-          snap.new.resolve <| some {
-            diagnostics :=
-              (← Language.Snapshot.Diagnostics.ofMessageLog (← Core.getAndEmptyMessageLog))
-            state := (← save)
-            value := val
-          }
-        return val
+  headers.mapM fun header => withDeclName header.declName <| withLevelNames header.levelNames do
+    let valStx ← liftMacroM <| declValToTerm header.valueStx
+    forallBoundedTelescope header.type header.numParams fun xs type => do
+      -- Add new info nodes for new fvars. The server will detect all fvars of a binder by the binder's source location.
+      for i in [0:header.binderIds.size] do
+        -- skip auto-bound prefix in `xs`
+        addLocalVarInfo header.binderIds[i]! xs[header.numParams - header.binderIds.size + i]!
+      let val ← elabTermEnsuringType valStx type
+      mkLambdaFVars xs val
 
 private def collectUsed (headers : Array DefViewElabHeader) (values : Array Expr) (toLift : List LetRecToLift)
     : StateRefT CollectFVars.State MetaM Unit := do
@@ -757,7 +640,7 @@ def pushMain (preDefs : Array PreDefinition) (sectionVars : Array Expr) (mainHea
     : TermElabM (Array PreDefinition) :=
   mainHeaders.size.foldM (init := preDefs) fun i preDefs => do
     let header := mainHeaders[i]!
-    let termination ← declValToTerminationHint header.value
+    let termination ← declValToTerminationHint header.valueStx
     let termination := termination.rememberExtraParams header.numParams mainVals[i]!
     let value ← mkLambdaFVars sectionVars mainVals[i]!
     let type ← mkForallFVars sectionVars header.type
@@ -913,40 +796,38 @@ def elabMutualDef (vars : Array Expr) (views : Array DefView) : TermElabM Unit :
   else
     go
 where
-  go :=
-    withAlwaysResolvedPromises views.size fun bodyPromises =>
-    withAlwaysResolvedPromises views.size fun tacPromises => do
-      let scopeLevelNames ← getLevelNames
-      let headers ← elabHeaders views bodyPromises tacPromises
-      let headers ← levelMVarToParamHeaders views headers
-      let allUserLevelNames := getAllUserLevelNames headers
-      withFunLocalDecls headers fun funFVars => do
-        for view in views, funFVar in funFVars do
-          addLocalVarInfo view.declId funFVar
-        let values ←
-          try
-            let values ← elabFunValues headers
-            Term.synthesizeSyntheticMVarsNoPostponing
-            values.mapM (instantiateMVars ·)
-          catch ex =>
-            logException ex
-            headers.mapM fun header => mkSorry header.type (synthetic := true)
-        let headers ← headers.mapM instantiateMVarsAtHeader
-        let letRecsToLift ← getLetRecsToLift
-        let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift
-        checkLetRecsToLiftTypes funFVars letRecsToLift
-        withUsed vars headers values letRecsToLift fun vars => do
-          let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift
-          for preDef in preDefs do
-            trace[Elab.definition] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
-          let preDefs ← withLevelNames allUserLevelNames <| levelMVarToParamPreDecls preDefs
-          let preDefs ← instantiateMVarsAtPreDecls preDefs
-          let preDefs ← fixLevelParams preDefs scopeLevelNames allUserLevelNames
-          for preDef in preDefs do
-            trace[Elab.definition] "after eraseAuxDiscr, {preDef.declName} : {preDef.type} :=\n{preDef.value}"
-          checkForHiddenUnivLevels allUserLevelNames preDefs
-          addPreDefinitions preDefs
-          processDeriving headers
+  go := do
+    let scopeLevelNames ← getLevelNames
+    let headers ← elabHeaders views
+    let headers ← levelMVarToParamHeaders views headers
+    let allUserLevelNames := getAllUserLevelNames headers
+    withFunLocalDecls headers fun funFVars => do
+      for view in views, funFVar in funFVars do
+        addLocalVarInfo view.declId funFVar
+      let values ←
+        try
+          let values ← elabFunValues headers
+          Term.synthesizeSyntheticMVarsNoPostponing
+          values.mapM (instantiateMVars ·)
+        catch ex =>
+          logException ex
+          headers.mapM fun header => mkSorry header.type (synthetic := true)
+      let headers ← headers.mapM instantiateMVarsAtHeader
+      let letRecsToLift ← getLetRecsToLift
+      let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift
+      checkLetRecsToLiftTypes funFVars letRecsToLift
+      withUsed vars headers values letRecsToLift fun vars => do
+        let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift
+        for preDef in preDefs do
+          trace[Elab.definition] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
+        let preDefs ← withLevelNames allUserLevelNames <| levelMVarToParamPreDecls preDefs
+        let preDefs ← instantiateMVarsAtPreDecls preDefs
+        let preDefs ← fixLevelParams preDefs scopeLevelNames allUserLevelNames
+        for preDef in preDefs do
+          trace[Elab.definition] "after eraseAuxDiscr, {preDef.declName} : {preDef.type} :=\n{preDef.value}"
+        checkForHiddenUnivLevels allUserLevelNames preDefs
+        addPreDefinitions preDefs
+        processDeriving headers
 
   processDeriving (headers : Array DefViewElabHeader) := do
     for header in headers, view in views do
@@ -961,45 +842,12 @@ end Term
 namespace Command
 
 def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
-  withAlwaysResolvedPromises ds.size fun headerPromises => do
-    let substr? := (mkNullNode ds).getSubstring?
-    let snap? := (← read).snap?
-    let mut views := #[]
-    let mut defs := #[]
-    for h : i in [0:ds.size], headerPromise in headerPromises do
-      let d := ds[i]
-      let modifiers ← elabModifiers d[0]
-      if ds.size > 1 && modifiers.isNonrec then
-        throwErrorAt d "invalid use of 'nonrec' modifier in 'mutual' block"
-      let mut view ← mkDefView modifiers d[1]
-      if let some snap := snap? then
-        -- overapproximation: includes previous bodies as well
-        let headerSubstr? := return { (← substr?) with stopPos := (← view.value.getPos?) }
-        view := { view with headerSnap? := some {
-          old? := do
-            -- transitioning from `Context.snap?` to `DefView.snap?` invariant: if the elaboration
-            -- context and state are unchanged, and the substring from the beginning of the first
-            -- header to the beginning of the current body is unchanged, then the elaboration result for
-            -- this header (which includes state from elaboration of previous headers!) should be
-            -- unchanged.
-            let old ← snap.old?
-            -- blocking wait, `HeadersParsedSnapshot` (and hopefully others) should be quick
-            let old ← old.val.get.toTyped? DefsParsedSnapshot
-            let oldParsed ← old.defs[i]?
-            guard <| (← headerSubstr?).sameAs (← oldParsed.headerSubstr?)
-            -- no syntax guard to store, we already did the necessary checks
-            return ⟨.missing, oldParsed.headerProcessedSnap⟩
-          new := headerPromise
-        } }
-        defs := defs.push {
-          headerSubstr?
-          headerProcessedSnap := { range? := d.getRange?, task := headerPromise.result }
-        }
-      views := views.push view
-    if let some snap := snap? then
-      -- no non-fatal diagnostics at this point
-      snap.new.resolve <| .ofTyped { defs, diagnostics := .empty : DefsParsedSnapshot }
-    runTermElabM fun vars => Term.elabMutualDef vars views
+  let views ← ds.mapM fun d => do
+    let modifiers ← elabModifiers d[0]
+    if ds.size > 1 && modifiers.isNonrec then
+      throwErrorAt d "invalid use of 'nonrec' modifier in 'mutual' block"
+    mkDefView modifiers d[1]
+  runTermElabM fun vars => Term.elabMutualDef vars views
 
 end Command
 end Lean.Elab

src/Lean/Elab/SyntheticMVars.lean

@@ -324,6 +324,7 @@ mutual
   If `report := false`, then `runTactic` will not capture exceptions nor will report unsolved goals. Unsolved goals become exceptions.
   -/
   partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) (report := true) : TermElabM Unit := withoutAutoBoundImplicit do
+    let code := tacticCode[1]
     instantiateMVarDeclMVars mvarId
     /-
     TODO: consider using `runPendingTacticsAt` at `mvarId` local context and target type.
@@ -345,7 +346,7 @@ mutual
               -- also put an info node on the `by` keyword specifically -- the token may be `canonical` and thus shown in the info
               -- view even though it is synthetic while a node like `tacticCode` never is (#1990)
               withTacticInfoContext tacticCode[0] do
-                withNarrowedArgTacticReuse (argIdx := 1) (evalTactic ·) tacticCode
+                evalTactic code
             synthesizeSyntheticMVars (postpone := .no)
           unless remainingGoals.isEmpty do
             if report then

src/Lean/Elab/Tactic/Basic.lean

@@ -34,6 +34,10 @@ structure Context where
   -/
   recover    : Bool := true
 
+structure SavedState where
+  term   : Term.SavedState
+  tactic : State
+
 abbrev TacticM := ReaderT Context $ StateRefT State TermElabM
 abbrev Tactic  := Syntax → TacticM Unit
 
@@ -96,16 +100,6 @@ def SavedState.restore (b : SavedState) (restoreInfo := false) : TacticM Unit :=
   b.term.restore restoreInfo
   set b.tactic
 
-@[specialize, inherit_doc Core.withRestoreOrSaveFull]
-def withRestoreOrSaveFull (reusableResult? : Option (α × SavedState))
-    (cont : TacticM SavedState → TacticM α) : TacticM α := do
-  if let some (_, state) := reusableResult? then
-    set state.tactic
-  let reusableResult? := reusableResult?.map (fun (val, state) => (val, state.term))
-  controlAt TermElabM fun runInBase =>
-    Term.withRestoreOrSaveFull reusableResult? fun restore =>
-      runInBase <| cont (return { term := (← restore), tactic := (← get) })
-
 protected def getCurrMacroScope : TacticM MacroScope := do pure (← readThe Core.Context).currMacroScope
 protected def getMainModule     : TacticM Name       := do pure (← getEnv).mainModule
 
@@ -438,12 +432,6 @@ def getNameOfIdent' (id : Syntax) : Name :=
 def withCaseRef [Monad m] [MonadRef m] (arrow body : Syntax) (x : m α) : m α :=
   withRef (mkNullNode #[arrow, body]) x
 
--- TODO: attribute(s)
-builtin_initialize builtinIncrementalTactics : IO.Ref NameSet ← IO.mkRef {}
-
-def registerBuiltinIncrementalTactic (kind : Name) : IO Unit := do
-  builtinIncrementalTactics.modify fun s => s.insert kind
-
 builtin_initialize registerTraceClass `Elab.tactic
 builtin_initialize registerTraceClass `Elab.tactic.backtrack
 

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -29,95 +29,13 @@ open Parser.Tactic
 @[builtin_tactic Lean.Parser.Tactic.«done»] def evalDone : Tactic := fun _ =>
   done
 
-open Language in
-/--
-Evaluates a tactic script in form of a syntax node with alternating tactics and separators as
-children.
- -/
-partial def evalSepTactics : Tactic := goEven
-where
-  -- `stx[0]` is the next tactic step, if any
-  goEven stx := do
-    if stx.getNumArgs == 0 then
-      return
-    let tac := stx[0]
-    /-
-    Each `goEven` step creates three promises under incrementality and reuses their older versions
-    where possible:
-    * `finished` is resolved when `tac` finishes execution; if `tac` is wholly unchanged from the
-      previous version, its state is reused and `tac` execution is skipped. Note that this promise
-      is never turned into a `SnapshotTask` and added to the snapshot tree as incremental reporting
-      is already covered by the next two promises.
-    * `inner` is passed to `tac` if it is marked as supporting incrementality and can be used for
-      reporting and partial reuse inside of it; if the tactic is unsupported or `finished` is wholly
-      reused, it is ignored.
-    * `next` is used as the context when invoking `goOdd` and thus eventually used for the next
-      `goEven` step. Thus, the incremental state of a tactic script is ultimately represented as a
-      chain of `next` snapshots. Its reuse is disabled if `tac` or its following separator are
-      changed in any way.
-    -/
-    let mut oldInner? := none
-    if let some snap := (← readThe Term.Context).tacSnap? then
-      if let some old := snap.old? then
-        let oldParsed := old.val.get
-        oldInner? := oldParsed.next.get? 0 |>.map (⟨oldParsed.data.stx, ·⟩)
-    -- compare `stx[0]` for `finished`/`next` reuse, focus on remainder of script
-    Term.withNarrowedTacticReuse (stx := stx) (fun stx => (stx[0], mkNullNode stx.getArgs[1:])) fun stxs => do
-      let some snap := (← readThe Term.Context).tacSnap?
-        | do evalTactic tac; goOdd stxs
-      let mut reusableResult? := none
-      let mut oldNext? := none
-      if let some old := snap.old? then
-        -- `tac` must be unchanged given the narrow above; let's reuse `finished`'s state!
-        let oldParsed := old.val.get
-        if let some state := oldParsed.data.finished.get.state? then
-          reusableResult? := some (state, state)
-          -- only allow `next` reuse in this case
-          oldNext? := oldParsed.next.get? 1 |>.map (⟨old.stx, ·⟩)
-
-      withAlwaysResolvedPromise fun next => do
-        withAlwaysResolvedPromise fun finished => do
-          withAlwaysResolvedPromise fun inner => do
-            snap.new.resolve <| .mk {
-              stx := tac
-              diagnostics := (← Language.Snapshot.Diagnostics.ofMessageLog
-                (← Core.getAndEmptyMessageLog))
-              finished := finished.result
-            } #[
-              {
-                range? := tac.getRange?
-                task := inner.result },
-              {
-                range? := stxs |>.getRange?
-                task := next.result }]
-            let state ← withRestoreOrSaveFull reusableResult? fun save => do
-              -- allow nested reuse for allowlisted tactics
-              withTheReader Term.Context ({ · with
-                  tacSnap? :=
-                    guard ((← builtinIncrementalTactics.get).contains tac.getKind) *>
-                    some {
-                      old? := oldInner?
-                      new := inner
-                    } }) do
-                evalTactic tac
-              save
-            finished.resolve { state? := state }
-
-        withTheReader Term.Context ({ · with tacSnap? := some {
-          new := next
-          old? := oldNext?
-        } }) do
-          goOdd stxs
-  -- `stx[0]` is the next separator, if any
-  goOdd stx := do
-    if stx.getNumArgs == 0 then
-      return
-    saveTacticInfoForToken stx[0] -- add `TacticInfo` node for `;`
-    -- disable further reuse on separator change as to not reuse wrong `TacticInfo`
-    Term.withNarrowedTacticReuse (fun stx => (stx[0], mkNullNode stx.getArgs[1:])) goEven stx
-
-@[builtin_tactic seq1] def evalSeq1 : Tactic := fun stx =>
-  evalSepTactics stx[0]
+@[builtin_tactic seq1] def evalSeq1 : Tactic := fun stx => do
+  let args := stx[0].getArgs
+  for i in [:args.size] do
+    if i % 2 == 0 then
+      evalTactic args[i]!
+    else
+      saveTacticInfoForToken args[i]! -- add `TacticInfo` node for `;`
 
 @[builtin_tactic paren] def evalParen : Tactic := fun stx =>
   evalTactic stx[1]
@@ -186,19 +104,25 @@ def addCheckpoints (stx : Syntax) : TacticM Syntax := do
   output := output ++ currentCheckpointBlock
   return stx.setArgs output
 
-builtin_initialize registerBuiltinIncrementalTactic ``tacticSeq1Indented
-@[builtin_tactic tacticSeq1Indented] def evalTacticSeq1Indented : Tactic :=
-  Term.withNarrowedArgTacticReuse (argIdx := 0) evalSepTactics
+/-- Evaluate `sepByIndent tactic "; " -/
+def evalSepByIndentTactic (stx : Syntax) : TacticM Unit := do
+  let stx ← addCheckpoints stx
+  for arg in stx.getArgs, i in [:stx.getArgs.size] do
+    if i % 2 == 0 then
+      evalTactic arg
+    else
+      saveTacticInfoForToken arg
+
+@[builtin_tactic tacticSeq1Indented] def evalTacticSeq1Indented : Tactic := fun stx =>
+  evalSepByIndentTactic stx[0]
 
-builtin_initialize registerBuiltinIncrementalTactic ``tacticSeqBracketed
 @[builtin_tactic tacticSeqBracketed] def evalTacticSeqBracketed : Tactic := fun stx => do
   let initInfo ← mkInitialTacticInfo stx[0]
   withRef stx[2] <| closeUsingOrAdmit do
     -- save state before/after entering focus on `{`
     withInfoContext (pure ()) initInfo
-    Term.withNarrowedArgTacticReuse (argIdx := 1) evalSepTactics stx
+    evalSepByIndentTactic stx[1]
 
-builtin_initialize registerBuiltinIncrementalTactic ``cdot
 @[builtin_tactic Lean.cdot] def evalTacticCDot : Tactic := fun stx => do
   -- adjusted copy of `evalTacticSeqBracketed`; we used to use the macro
   -- ``| `(tactic| $cdot:cdotTk $tacs) => `(tactic| {%$cdot ($tacs) }%$cdot)``
@@ -208,7 +132,7 @@ builtin_initialize registerBuiltinIncrementalTactic ``cdot
   withRef stx[0] <| closeUsingOrAdmit do
     -- save state before/after entering focus on `·`
     withInfoContext (pure ()) initInfo
-    Term.withNarrowedArgTacticReuse (argIdx := 1) evalTactic stx
+    evalSepByIndentTactic stx[1]
 
 @[builtin_tactic Parser.Tactic.focus] def evalFocus : Tactic := fun stx => do
   let mkInfo ← mkInitialTacticInfo stx[0]
@@ -281,9 +205,8 @@ private def getOptRotation (stx : Syntax) : Nat :=
     throwError "failed on all goals"
   setGoals mvarIdsNew.toList
 
-builtin_initialize registerBuiltinIncrementalTactic ``tacticSeq
-@[builtin_tactic tacticSeq] def evalTacticSeq : Tactic :=
-  Term.withNarrowedArgTacticReuse (argIdx := 0) evalTactic
+@[builtin_tactic tacticSeq] def evalTacticSeq : Tactic := fun stx =>
+  evalTactic stx[0]
 
 partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit :=
   if h : i < tactics.size then
@@ -503,16 +426,16 @@ where
     .group <| .nest 2 <|
     .ofFormat .line ++ .joinSep items sep
 
-builtin_initialize registerBuiltinIncrementalTactic ``case
+
 @[builtin_tactic «case»] def evalCase : Tactic
-  | stx@`(tactic| case $[$tag $hs*]|* =>%$arr $tac:tacticSeq1Indented) =>
+  | stx@`(tactic| case $[$tag $hs*]|* =>%$arr $tac:tacticSeq) =>
     for tag in tag, hs in hs do
       let (g, gs) ← getCaseGoals tag
       let g ← renameInaccessibles g hs
       setGoals [g]
       g.setTag Name.anonymous
-      withCaseRef arr tac <| closeUsingOrAdmit <| withTacticInfoContext stx <|
-        Term.withNarrowedArgTacticReuse (argIdx := 3) (evalTactic ·) stx
+      withCaseRef arr tac do
+        closeUsingOrAdmit (withTacticInfoContext stx (evalTactic tac))
       setGoals gs
   | _ => throwUnsupportedSyntax
 

src/Lean/Elab/Tactic/Induction.lean

@@ -54,25 +54,23 @@ private def getAltDArrow (alt : Syntax) : Syntax :=
 def isHoleRHS (rhs : Syntax) : Bool :=
   rhs.isOfKind ``Parser.Term.syntheticHole || rhs.isOfKind ``Parser.Term.hole
 
-def evalAlt (mvarId : MVarId) (alt : Syntax) (addInfo : TermElabM Unit) : TacticM Unit :=
+def evalAlt (mvarId : MVarId) (alt : Syntax) (addInfo : TermElabM Unit) (remainingGoals : Array MVarId) : TacticM (Array MVarId) :=
   let rhs := getAltRHS alt
   withCaseRef (getAltDArrow alt) rhs do
     if isHoleRHS rhs then
       addInfo
-      mvarId.withContext <| withTacticInfoContext rhs do
+      let gs' ← mvarId.withContext <| withTacticInfoContext rhs do
         let mvarDecl ← mvarId.getDecl
         let val ← elabTermEnsuringType rhs mvarDecl.type
         mvarId.assign val
         let gs' ← getMVarsNoDelayed val
         tagUntaggedGoals mvarDecl.userName `induction gs'.toList
-        setGoals <| (← getGoals) ++ gs'.toList
+        pure gs'
+      return remainingGoals ++ gs'
     else
-      let goals ← getGoals
-      try
-        setGoals [mvarId]
-        closeUsingOrAdmit (withTacticInfoContext alt (addInfo *> evalTactic rhs))
-      finally
-        setGoals goals
+      setGoals [mvarId]
+      closeUsingOrAdmit (withTacticInfoContext alt (addInfo *> evalTactic rhs))
+      return remainingGoals
 
 /-!
   Helper method for creating an user-defined eliminator/recursor application.
@@ -201,9 +199,6 @@ private def getAltNumFields (elimInfo : ElimInfo) (altName : Name) : TermElabM N
       return altInfo.numFields
   throwError "unknown alternative name '{altName}'"
 
-private def isWildcard (altStx : Syntax) : Bool :=
-  getAltName altStx == `_
-
 private def checkAltNames (alts : Array Alt) (altsSyntax : Array Syntax) : TacticM Unit :=
   for i in [:altsSyntax.size] do
     let altStx := altsSyntax[i]!
@@ -234,184 +229,151 @@ private def saveAltVarsInfo (altMVarId : MVarId) (altStx : Syntax) (fvarIds : Ar
           Term.addLocalVarInfo altVars[i]! (mkFVar fvarId)
           i := i + 1
 
-open Language in
-def evalAlts (elimInfo : ElimInfo) (alts : Array Alt) (optPreTac : Syntax) (altStxs : Array Syntax)
+/--
+  If `altsSyntax` is not empty we reorder `alts` using the order the alternatives have been provided
+  in `altsSyntax`. Motivations:
+
+  1- It improves the effectiveness of the `checkpoint` and `save` tactics. Consider the following example:
+  ```lean
+  example (h₁ : p ∨ q) (h₂ : p → x = 0) (h₃ : q → y = 0) : x * y = 0 := by
+    cases h₁ with
+    | inr h =>
+      sleep 5000 -- sleeps for 5 seconds
+      save
+      have : y = 0 := h₃ h
+      -- We can confortably work here
+    | inl h => stop ...
+  ```
+  If we do reorder, the `inl` alternative will be executed first. Moreover, as we type in the `inr` alternative,
+  type errors will "swallow" the `inl` alternative and affect the tactic state at `save` making it ineffective.
+
+  2- The errors are produced in the same order the appear in the code above. This is not super important when using IDEs.
+-/
+def reorderAlts (alts : Array Alt) (altsSyntax : Array Syntax) : Array Alt := Id.run do
+  if altsSyntax.isEmpty then
+    return alts
+  else
+    let mut alts := alts
+    let mut result := #[]
+    for altStx in altsSyntax do
+      let altName := getAltName altStx
+      let some i := alts.findIdx? (·.1 == altName) | return result ++ alts
+      result := result.push alts[i]!
+      alts := alts.eraseIdx i
+    return result ++ alts
+
+def evalAlts (elimInfo : ElimInfo) (alts : Array Alt) (optPreTac : Syntax) (altsSyntax : Array Syntax)
     (initialInfo : Info)
     (numEqs : Nat := 0) (numGeneralized : Nat := 0) (toClear : Array FVarId := #[])
     (toTag : Array (Ident × FVarId) := #[]) : TacticM Unit := do
-  let hasAlts := altStxs.size > 0
+  let hasAlts := altsSyntax.size > 0
   if hasAlts then
     -- default to initial state outside of alts
     -- HACK: because this node has the same span as the original tactic,
     -- we need to take all the info trees we have produced so far and re-nest them
     -- inside this node as well
     let treesSaved ← getResetInfoTrees
-    withInfoContext ((modifyInfoState fun s => { s with trees := treesSaved }) *> goWithInfo) (pure initialInfo)
-  else goWithInfo
+    withInfoContext ((modifyInfoState fun s => { s with trees := treesSaved }) *> go) (pure initialInfo)
+  else go
 where
-  -- continuation in the correct info context
-  goWithInfo := do
-    let hasAlts := altStxs.size > 0
-
-    if hasAlts then
-      if let some tacSnap := (← readThe Term.Context).tacSnap? then
-        -- incrementality: create a new promise for each alternative, resolve current snapshot to
-        -- them, eventually put each of them back in `Context.tacSnap?` in `applyAltStx`
-        withAlwaysResolvedPromise fun finished => do
-          withAlwaysResolvedPromises altStxs.size fun altPromises => do
-            tacSnap.new.resolve <| .mk {
-              -- save all relevant syntax here for comparison with next document version
-              stx := mkNullNode altStxs
-              diagnostics := .empty
-              finished := finished.result
-            } (altStxs.zipWith altPromises fun stx prom =>
-                { range? := stx.getRange?, task := prom.result })
-            goWithIncremental <| altPromises.mapIdx fun i prom => {
-              old? := do
-                let old ← tacSnap.old?
-                -- waiting is fine here: this is the old version of the snapshot resolved above
-                -- immediately at the beginning of the tactic
-                let old := old.val.get
-                -- use old version of `mkNullNode altsSyntax` as guard, will be compared with new
-                -- version and picked apart in `applyAltStx`
-                return ⟨old.data.stx, (← old.next[i]?)⟩
-              new := prom
-            }
-            finished.resolve { state? := (← saveState) }
-        return
-
-    goWithIncremental #[]
-
-  -- continuation in the correct incrementality context
-  goWithIncremental (tacSnaps : Array (SnapshotBundle TacticParsedSnapshot)) := do
-    let hasAlts := altStxs.size > 0
-    let mut alts := alts
-
-    -- initial sanity checks: named cases should be known, wildcards should be last
-    checkAltNames alts altStxs
-
-    /-
-    First process `altsSyntax` in order, removing covered alternatives from `alts`. Previously we
-    did one loop through `alts`, looking up suitable alternatives from `altsSyntax`.
-    Motivations for the change:
-
-    1- It improves the effectiveness of incremental reuse. Consider the following example:
-    ```lean
-    example (h₁ : p ∨ q) (h₂ : p → x = 0) (h₃ : q → y = 0) : x * y = 0 := by
-      cases h₁ with
-      | inr h =>
-        sleep 5000 -- sleeps for 5 seconds
-        save
-        have : y = 0 := h₃ h
-        -- We can comfortably work here
-      | inl h => stop ...
-    ```
-    If we iterated through `alts` instead of `altsSyntax`, the `inl` alternative would be executed
-    first, making partial reuse in `inr` impossible (without support for reuse with position
-    adjustments).
-
-    2- The errors are produced in the same order the appear in the code above. This is not super
-    important when using IDEs.
-    -/
-    for altStxIdx in [0:altStxs.size] do
-      let altStx := altStxs[altStxIdx]!
-      let altName := getAltName altStx
-      if let some i := alts.findIdx? (·.1 == altName) then
-        -- cover named alternative
-        applyAltStx tacSnaps altStxIdx altStx alts[i]!
-        alts := alts.eraseIdx i
-      else if !alts.isEmpty && isWildcard altStx then
-        -- cover all alternatives
-        for alt in alts do
-          applyAltStx tacSnaps altStxIdx altStx alt
-        alts := #[]
-      else
-        throwErrorAt altStx "unused alternative '{altName}'"
-
-    -- now process remaining alternatives; these might either be unreachable or we're in `induction`
-    -- without `with`. In all other cases, remaining alternatives are flagged as errors.
+  go := do
+    checkAltNames alts altsSyntax
+    let alts := reorderAlts alts altsSyntax
+    let hasAlts := altsSyntax.size > 0
+    let mut usedWildcard := false
+    let mut subgoals := #[] -- when alternatives are not provided, we accumulate subgoals here
+    let mut altsSyntax := altsSyntax
     for { name := altName, info, mvarId := altMVarId } in alts do
       let numFields ← getAltNumFields elimInfo altName
-      let mut (_, altMVarId) ← altMVarId.introN numFields
-      let some (altMVarId', subst) ← Cases.unifyEqs? numEqs altMVarId {}
-        | continue  -- alternative is not reachable
-      altMVarId ← if info.provesMotive then
-        (_, altMVarId) ← altMVarId'.introNP numGeneralized
-        pure altMVarId
-      else
-        pure altMVarId'
-      for fvarId in toClear do
-        altMVarId ← altMVarId.tryClear fvarId
-      altMVarId.withContext do
-        for (stx, fvar) in toTag do
-          Term.addLocalVarInfo stx (subst.get fvar)
-      let altMVarIds ← applyPreTac altMVarId
-      if !hasAlts then
-        -- User did not provide alternatives using `|`
-        setGoals <| (← getGoals) ++ altMVarIds
-      else if !altMVarIds.isEmpty then
-        logError m!"alternative '{altName}' has not been provided"
-        altMVarIds.forM fun mvarId => admitGoal mvarId
-
-  /-- Applies syntactic alternative to alternative goal. -/
-  applyAltStx tacSnaps altStxIdx altStx alt := withRef altStx do
-    let { name := altName, info, mvarId := altMVarId } := alt
-    -- also checks for unknown alternatives
-    let numFields ← getAltNumFields elimInfo altName
-    let altVars := getAltVars altStx
-    let numFieldsToName ← if altHasExplicitModifier altStx then pure numFields else getNumExplicitFields altMVarId numFields
-    if altVars.size > numFieldsToName then
-      logError m!"too many variable names provided at alternative '{altName}', #{altVars.size} provided, but #{numFieldsToName} expected"
-    let mut (fvarIds, altMVarId) ← altMVarId.introN numFields (altVars.toList.map getNameOfIdent') (useNamesForExplicitOnly := !altHasExplicitModifier altStx)
-    -- Delay adding the infos for the pattern LHS because we want them to nest
-    -- inside tacticInfo for the current alternative (in `evalAlt`)
-    let addInfo : TermElabM Unit := do
-      if (← getInfoState).enabled then
-        if let some declName := info.declName? then
-          addConstInfo (getAltNameStx altStx) declName
-        saveAltVarsInfo altMVarId altStx fvarIds
-    let unusedAlt := do
-      addInfo
-      if !isWildcard altStx then
-        throwError "alternative '{altName}' is not needed"
-    let some (altMVarId', subst) ← Cases.unifyEqs? numEqs altMVarId {}
-      | unusedAlt
-    altMVarId ← if info.provesMotive then
-      (_, altMVarId) ← altMVarId'.introNP numGeneralized
-      pure altMVarId
-    else
-      pure altMVarId'
-    for fvarId in toClear do
-      altMVarId ← altMVarId.tryClear fvarId
-    altMVarId.withContext do
-      for (stx, fvar) in toTag do
-        Term.addLocalVarInfo stx (subst.get fvar)
-    let altMVarIds ← applyPreTac altMVarId
-    if altMVarIds.isEmpty then
-      return (← unusedAlt)
-
-    -- select corresponding snapshot bundle for incrementality of this alternative
-    -- note that `tacSnaps[altStxIdx]?` is `none` if `tacSnap?` was `none` to begin with
-    withTheReader Term.Context ({ · with tacSnap? := tacSnaps[altStxIdx]? }) do
-    -- all previous alternatives have to be unchanged for reuse
-    Term.withNarrowedArgTacticReuse (stx := mkNullNode altStxs) (argIdx := altStxIdx) fun altStx => do
-    -- everything up to rhs has to be unchanged for reuse
-    Term.withNarrowedArgTacticReuse (stx := altStx) (argIdx := 2) fun _rhs => do
-    -- disable reuse if rhs is run multiple times
-    Term.withoutTacticIncrementality (altMVarIds.length != 1 || isWildcard altStx) do
-      for altMVarId' in altMVarIds do
-        evalAlt altMVarId' altStx addInfo
-
-  /-- Applies `induction .. with $preTac | ..`, if any, to an alternative goal. -/
+      let mut isWildcard := false
+      let altStx? ←
+        match altsSyntax.findIdx? (fun alt => getAltName alt == altName) with
+        | some idx =>
+          let altStx := altsSyntax[idx]!
+          altsSyntax := altsSyntax.eraseIdx idx
+          pure (some altStx)
+        | none => match altsSyntax.findIdx? (fun alt => getAltName alt == `_) with
+          | some idx =>
+            isWildcard := true
+            pure (some altsSyntax[idx]!)
+          | none =>
+            pure none
+      match altStx? with
+      | none =>
+        let mut (_, altMVarId) ← altMVarId.introN numFields
+        match (← Cases.unifyEqs? numEqs altMVarId {}) with
+        | none   => pure () -- alternative is not reachable
+        | some (altMVarId', subst) =>
+          altMVarId ← if info.provesMotive then
+            (_, altMVarId) ← altMVarId'.introNP numGeneralized
+            pure altMVarId
+          else
+            pure altMVarId'
+          for fvarId in toClear do
+            altMVarId ← altMVarId.tryClear fvarId
+          altMVarId.withContext do
+            for (stx, fvar) in toTag do
+              Term.addLocalVarInfo stx (subst.get fvar)
+          let altMVarIds ← applyPreTac altMVarId
+          if !hasAlts then
+            -- User did not provide alternatives using `|`
+            subgoals := subgoals ++ altMVarIds.toArray
+          else if altMVarIds.isEmpty then
+            pure ()
+          else
+            logError m!"alternative '{altName}' has not been provided"
+            altMVarIds.forM fun mvarId => admitGoal mvarId
+      | some altStx =>
+        (subgoals, usedWildcard) ← withRef altStx do
+          let altVars := getAltVars altStx
+          let numFieldsToName ← if altHasExplicitModifier altStx then pure numFields else getNumExplicitFields altMVarId numFields
+          if altVars.size > numFieldsToName then
+            logError m!"too many variable names provided at alternative '{altName}', #{altVars.size} provided, but #{numFieldsToName} expected"
+          let mut (fvarIds, altMVarId) ← altMVarId.introN numFields (altVars.toList.map getNameOfIdent') (useNamesForExplicitOnly := !altHasExplicitModifier altStx)
+          -- Delay adding the infos for the pattern LHS because we want them to nest
+          -- inside tacticInfo for the current alternative (in `evalAlt`)
+          let addInfo : TermElabM Unit := do
+            if (← getInfoState).enabled then
+              if let some declName := info.declName? then
+                addConstInfo (getAltNameStx altStx) declName
+              saveAltVarsInfo altMVarId altStx fvarIds
+          let unusedAlt := do
+            addInfo
+            if isWildcard then
+              pure (#[], usedWildcard)
+            else
+              throwError "alternative '{altName}' is not needed"
+          match (← Cases.unifyEqs? numEqs altMVarId {}) with
+          | none => unusedAlt
+          | some (altMVarId', subst) =>
+            altMVarId ← if info.provesMotive then
+              (_, altMVarId) ← altMVarId'.introNP numGeneralized
+              pure altMVarId
+            else
+              pure altMVarId'
+            for fvarId in toClear do
+              altMVarId ← altMVarId.tryClear fvarId
+            altMVarId.withContext do
+              for (stx, fvar) in toTag do
+                Term.addLocalVarInfo stx (subst.get fvar)
+            let altMVarIds ← applyPreTac altMVarId
+            if altMVarIds.isEmpty then
+              unusedAlt
+            else
+              let mut subgoals := subgoals
+              for altMVarId' in altMVarIds do
+                subgoals ← evalAlt altMVarId' altStx addInfo subgoals
+              pure (subgoals, usedWildcard || isWildcard)
+    if usedWildcard then
+      altsSyntax := altsSyntax.filter fun alt => getAltName alt != `_
+    unless altsSyntax.isEmpty do
+      logErrorAt altsSyntax[0]! "unused alternative"
+    setGoals subgoals.toList
   applyPreTac (mvarId : MVarId) : TacticM (List MVarId) :=
     if optPreTac.isNone then
       return [mvarId]
     else
-      -- disable incrementality for the pre-tactic to avoid non-monotonic progress reporting; it
-      -- would be possible to include a custom task around the pre-tac with an appropriate range in
-      -- the snapshot such that it is cached as well if it turns out that this is valuable
-      Term.withoutTacticIncrementality true do
-        evalTacticAt optPreTac[0] mvarId
+      evalTacticAt optPreTac[0] mvarId
 
 end ElimApp
 
@@ -458,24 +420,8 @@ Return an array containing its alternatives.
 private def getAltsOfInductionAlts (inductionAlts : Syntax) : Array Syntax :=
   inductionAlts[2].getArgs
 
-/--
-Given `inductionAlts` of the form
-```
-syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)+)
-```
-runs `cont alts` where `alts` is an array containing all `inductionAlt`s while disabling incremental
-reuse if any other syntax changed.
--/
-private def withAltsOfOptInductionAlts (optInductionAlts : Syntax)
-    (cont : Array Syntax → TacticM α) : TacticM α :=
-  Term.withNarrowedTacticReuse (stx := optInductionAlts) (fun optInductionAlts =>
-    if optInductionAlts.isNone then
-      -- if there are no alternatives, what to compare is irrelevant as there will be no reuse
-      (mkNullNode #[], mkNullNode #[])
-    else
-      -- `with` and tactic applied to all branches must be unchanged for reuse
-      (mkNullNode optInductionAlts[0].getArgs[:2], optInductionAlts[0].getArg 2))
-    (fun alts => cont alts.getArgs)
+private def getAltsOfOptInductionAlts (optInductionAlts : Syntax) : Array Syntax :=
+  if optInductionAlts.isNone then #[] else getAltsOfInductionAlts optInductionAlts[0]
 
 private def getOptPreTacOfOptInductionAlts (optInductionAlts : Syntax) : Syntax :=
   if optInductionAlts.isNone then mkNullNode else optInductionAlts[0][1]
@@ -636,11 +582,12 @@ private def generalizeTargets (exprs : Array Expr) : TacticM (Array Expr) := do
   else
     return exprs
 
-builtin_initialize registerBuiltinIncrementalTactic ``Lean.Parser.Tactic.induction
 @[builtin_tactic Lean.Parser.Tactic.induction] def evalInduction : Tactic := fun stx =>
   match expandInduction? stx with
   | some stxNew => withMacroExpansion stx stxNew <| evalTactic stxNew
   | _ => focus do
+    let optInductionAlts := stx[4]
+    let alts := getAltsOfOptInductionAlts optInductionAlts
     let targets ← withMainContext <| stx[1].getSepArgs.mapM (elabTerm · none)
     let targets ← generalizeTargets targets
     let elimInfo ← withMainContext <| getElimNameInfo stx[2] targets (induction := true)
@@ -658,15 +605,10 @@ builtin_initialize registerBuiltinIncrementalTactic ``Lean.Parser.Tactic.inducti
           ElimApp.mkElimApp elimInfo targets tag
         trace[Elab.induction] "elimApp: {result.elimApp}"
         ElimApp.setMotiveArg mvarId result.motive targetFVarIds
-        -- drill down into old and new syntax: allow reuse of an rhs only if everything before it is
-        -- unchanged
-        -- everything up to the alternatives must be unchanged for reuse
-        Term.withNarrowedArgTacticReuse (stx := stx) (argIdx := 4) fun optInductionAlts => do
-        withAltsOfOptInductionAlts optInductionAlts fun alts => do
-          let optPreTac := getOptPreTacOfOptInductionAlts optInductionAlts
-          mvarId.assign result.elimApp
-          ElimApp.evalAlts elimInfo result.alts optPreTac alts initInfo (numGeneralized := n) (toClear := targetFVarIds)
-          appendGoals result.others.toList
+        let optPreTac := getOptPreTacOfOptInductionAlts optInductionAlts
+        mvarId.assign result.elimApp
+        ElimApp.evalAlts elimInfo result.alts optPreTac alts initInfo (numGeneralized := n) (toClear := targetFVarIds)
+        appendGoals result.others.toList
 where
   checkTargets (targets : Array Expr) : MetaM Unit := do
     let mut foundFVars : FVarIdSet := {}
@@ -708,13 +650,15 @@ def elabCasesTargets (targets : Array Syntax) : TacticM (Array Expr × Array (Id
     else
       return (args.map (·.expr), #[])
 
-builtin_initialize registerBuiltinIncrementalTactic ``Lean.Parser.Tactic.cases
 @[builtin_tactic Lean.Parser.Tactic.cases] def evalCases : Tactic := fun stx =>
   match expandCases? stx with
   | some stxNew => withMacroExpansion stx stxNew <| evalTactic stxNew
   | _ => focus do
     -- leading_parser nonReservedSymbol "cases " >> sepBy1 (group majorPremise) ", " >> usingRec >> optInductionAlts
     let (targets, toTag) ← elabCasesTargets stx[1].getSepArgs
+    let optInductionAlts := stx[3]
+    let optPreTac := getOptPreTacOfOptInductionAlts optInductionAlts
+    let alts :=  getAltsOfOptInductionAlts optInductionAlts
     let targetRef := stx[1]
     let elimInfo ← withMainContext <| getElimNameInfo stx[2] targets (induction := false)
     let mvarId ← getMainGoal
@@ -732,14 +676,8 @@ builtin_initialize registerBuiltinIncrementalTactic ``Lean.Parser.Tactic.cases
       mvarId.withContext do
         ElimApp.setMotiveArg mvarId elimArgs[elimInfo.motivePos]!.mvarId! targetsNew
         mvarId.assign result.elimApp
-        -- drill down into old and new syntax: allow reuse of an rhs only if everything before it is
-        -- unchanged
-        -- everything up to the alternatives must be unchanged for reuse
-        Term.withNarrowedArgTacticReuse (stx := stx) (argIdx := 3) fun optInductionAlts => do
-        withAltsOfOptInductionAlts optInductionAlts fun alts => do
-          let optPreTac := getOptPreTacOfOptInductionAlts optInductionAlts
-          ElimApp.evalAlts elimInfo result.alts optPreTac alts initInfo
-            (numEqs := targets.size) (toClear := targetsNew) (toTag := toTag)
+        ElimApp.evalAlts elimInfo result.alts optPreTac alts initInfo
+          (numEqs := targets.size) (toClear := targetsNew) (toTag := toTag)
 
 builtin_initialize
   registerTraceClass `Elab.cases

src/Lean/Elab/Term.lean

@@ -13,7 +13,6 @@ import Lean.Elab.Config
 import Lean.Elab.Level
 import Lean.Elab.DeclModifiers
 import Lean.Elab.PreDefinition.WF.TerminationHint
-import Lean.Language.Basic
 
 namespace Lean.Elab
 
@@ -113,14 +112,6 @@ structure State where
   letRecsToLift     : List LetRecToLift := []
   deriving Inhabited
 
-/--
-  Backtrackable state for the `TermElabM` monad.
--/
-structure SavedState where
-  meta   : Meta.SavedState
-  «elab» : State
-  deriving Nonempty
-
 end Term
 
 namespace Tactic
@@ -161,42 +152,6 @@ structure Cache where
    post : PHashMap CacheKey Snapshot := {}
    deriving Inhabited
 
-section Snapshot
-open Language
-
-structure SavedState where
-  term   : Term.SavedState
-  tactic : State
-
-/-- State after finishing execution of a tactic. -/
-structure TacticFinished where
-  /-- Reusable state, if no fatal exception occurred. -/
-  state? : Option SavedState
-deriving Inhabited
-
-/-- Snapshot just before execution of a tactic. -/
-structure TacticParsedSnapshotData extends Language.Snapshot where
-  /-- Syntax tree of the tactic, stored and compared for incremental reuse. -/
-  stx      : Syntax
-  /-- Task for state after tactic execution. -/
-  finished : Task TacticFinished
-deriving Inhabited
-
-/-- State after execution of a single synchronous tactic step. -/
-inductive TacticParsedSnapshot where
-  | mk (data : TacticParsedSnapshotData) (next : Array (SnapshotTask TacticParsedSnapshot))
-deriving Inhabited
-abbrev TacticParsedSnapshot.data : TacticParsedSnapshot → TacticParsedSnapshotData
-  | .mk data _ => data
-/-- Potential, potentially parallel, follow-up tactic executions. -/
--- In the first, non-parallel version, each task will depend on its predecessor
-abbrev TacticParsedSnapshot.next : TacticParsedSnapshot → Array (SnapshotTask TacticParsedSnapshot)
-  | .mk _ next => next
-partial instance : ToSnapshotTree TacticParsedSnapshot where
-  toSnapshotTree := go where
-    go := fun ⟨s, next⟩ => ⟨s.toSnapshot, next.map (·.map (sync := true) go)⟩
-
-end Snapshot
 end Tactic
 
 namespace Term
@@ -256,13 +211,6 @@ structure Context where
   /-- Cache for the `save` tactic. It is only `some` in the LSP server. -/
   tacticCache?     : Option (IO.Ref Tactic.Cache) := none
   /--
-  Snapshot for incremental processing of current tactic, if any.
-
-  Invariant: if the bundle's `old?` is set, then the state *up to the start* of the tactic is
-  unchanged, i.e. reuse is possible.
-  -/
-  tacSnap?         : Option (Language.SnapshotBundle Tactic.TacticParsedSnapshot) := none
-  /--
   If `true`, we store in the `Expr` the `Syntax` for recursive applications (i.e., applications
   of free variables tagged with `isAuxDecl`). We store the `Syntax` using `mkRecAppWithSyntax`.
   We use the `Syntax` object to produce better error messages at `Structural.lean` and `WF.lean`. -/
@@ -293,6 +241,14 @@ open Meta
 instance : Inhabited (TermElabM α) where
   default := throw default
 
+/--
+  Backtrackable state for the `TermElabM` monad.
+-/
+structure SavedState where
+  meta   : Meta.SavedState
+  «elab» : State
+  deriving Nonempty
+
 protected def saveState : TermElabM SavedState :=
   return { meta := (← Meta.saveState), «elab» := (← get) }
 
@@ -305,87 +261,18 @@ def SavedState.restore (s : SavedState) (restoreInfo : Bool := false) : TermElab
   unless restoreInfo do
     setInfoState infoState
 
-@[specialize, inherit_doc Core.withRestoreOrSaveFull]
-def withRestoreOrSaveFull (reusableResult? : Option (α × SavedState))
-    (cont : TermElabM SavedState → TermElabM α) : TermElabM α := do
-  if let some (_, state) := reusableResult? then
-    set state.elab
-  let reusableResult? := reusableResult?.map (fun (val, state) => (val, state.meta))
-  controlAt MetaM fun runInBase =>
-    Meta.withRestoreOrSaveFull reusableResult? fun restore =>
-      runInBase <| cont (return { meta := (← restore), «elab» := (← get) })
+/--
+Restores full state including sources for unique identifiers. Only intended for incremental reuse
+between elaboration runs, not for backtracking within a single run.
+-/
+def SavedState.restoreFull (s : SavedState) : TermElabM Unit := do
+  s.meta.restoreFull
+  set s.elab
 
 instance : MonadBacktrack SavedState TermElabM where
   saveState      := Term.saveState
   restoreState b := b.restore
 
-/--
-Manages reuse information for nested tactics by `split`ting given syntax into an outer and inner
-part. `act` is then run on the inner part but with reuse information adjusted as following:
-* If the old (from `tacSnap?`'s `SyntaxGuarded.stx`) and new (from `stx`) outer syntax are not
-  identical according to `Syntax.structRangeEq`, reuse is disabled.
-* Otherwise, the old syntax as stored in `tacSnap?` is updated to the old *inner* syntax.
-* In any case, we also use `withRef` on the inner syntax to avoid leakage of the outer syntax into
-  `act` via this route.
-
-For any tactic that participates in reuse, `withNarrowedTacticReuse` should be applied to the
-tactic's syntax and `act` should be used to do recursive tactic evaluation of nested parts.
--/
-def withNarrowedTacticReuse [Monad m] [MonadExceptOf Exception m] [MonadWithReaderOf Context m]
-    [MonadOptions m] [MonadRef m] (split : Syntax → Syntax × Syntax) (act : Syntax → m α)
-    (stx : Syntax) : m α := do
-  let (outer, inner) := split stx
-  let opts ← getOptions
-  withTheReader Term.Context (fun ctx => { ctx with tacSnap? := ctx.tacSnap?.map fun tacSnap =>
-    { tacSnap with old? := tacSnap.old?.bind fun old => do
-      let (oldOuter, oldInner) := split old.stx
-      guard <| outer.structRangeEqWithTraceReuse opts oldOuter
-      return { old with stx := oldInner }
-    }
-  }) do
-    withRef inner do
-      act inner
-
-/--
-A variant of `withNarrowedTacticReuse` that uses `stx[argIdx]` as the inner syntax and all `stx`
-child nodes before that as the outer syntax, i.e. reuse is disabled if there was any change before
-`argIdx`.
-
-NOTE: child nodes after `argIdx` are not tested (which would almost always disable reuse as they are
-necessarily shifted by changes at `argIdx`) so it must be ensured that the result of `arg` does not
-depend on them (i.e. they should not be inspected beforehand).
--/
-def withNarrowedArgTacticReuse [Monad m] [MonadExceptOf Exception m] [MonadWithReaderOf Context m]
-    [MonadOptions m] [MonadRef m] (argIdx : Nat) (act : Syntax → m α) (stx : Syntax) : m α :=
-  withNarrowedTacticReuse (fun stx => (mkNullNode stx.getArgs[:argIdx], stx[argIdx])) act stx
-
-/--
-Disables incremental tactic reuse *and* reporting for `act` if `cond` is true by setting `tacSnap?`
-to `none`. This should be done for tactic blocks that are run multiple times as otherwise the
-reported progress will jump back and forth (and partial reuse for these kinds of tact blocks is
-similarly questionable).
--/
-def withoutTacticIncrementality [Monad m] [MonadWithReaderOf Context m] [MonadOptions m] [MonadRef m]
-    (cond : Bool) (act : m α) : m α := do
-  let opts ← getOptions
-  withTheReader Term.Context (fun ctx => { ctx with tacSnap? := ctx.tacSnap?.filter fun tacSnap => Id.run do
-    if let some old := tacSnap.old? then
-      if cond && opts.getBool `trace.Elab.reuse then
-        dbg_trace "reuse stopped: guard failed at {old.stx}"
-    return !cond
-  }) act
-
-/-- Disables incremental tactic reuse for `act` if `cond` is true. -/
-def withoutTacticReuse [Monad m] [MonadWithReaderOf Context m] [MonadOptions m] [MonadRef m]
-    (cond : Bool) (act : m α) : m α := do
-  let opts ← getOptions
-  withTheReader Term.Context (fun ctx => { ctx with tacSnap? := ctx.tacSnap?.map fun tacSnap =>
-    { tacSnap with old? := tacSnap.old?.filter fun old => Id.run do
-      if cond && opts.getBool `trace.Elab.reuse then
-        dbg_trace "reuse stopped: guard failed at {old.stx}"
-      return !cond }
-  }) act
-
 abbrev TermElabResult (α : Type) := EStateM.Result Exception SavedState α
 
 /--

src/Lean/Elab/Util.lean

@@ -205,7 +205,7 @@ def logException [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [
   match ex with
   | Exception.error ref msg => logErrorAt ref msg
   | Exception.internal id _ =>
-    unless isAbortExceptionId id || id == Core.interruptExceptionId do
+    unless isAbortExceptionId id do
       let name ← id.getName
       logError m!"internal exception: {name}"
 

src/Lean/Language/Basic.lean

@@ -17,13 +17,8 @@ set_option linter.missingDocs true
 
 namespace Lean.Language
 
-/--
-`MessageLog` with interactive diagnostics.
-
-Can be created using `Diagnostics.empty` or `Diagnostics.ofMessageLog`.
--/
+/-- `MessageLog` with interactive diagnostics. -/
 structure Snapshot.Diagnostics where
-  private mk ::
   /-- Non-interactive message log. -/
   msgLog : MessageLog
   /--
@@ -138,7 +133,8 @@ checking if we can reuse `old?` if set or else redoing the corresponding elabora
 case, we derive new bundles for nested snapshots, if any, and finally `resolve` `new` to the result.
 
 Note that failing to `resolve` a created promise will block the language server indefinitely!
-We use `withAlwaysResolvedPromise`/`withAlwaysResolvedPromises` to ensure this doesn't happen.
+Corresponding `IO.Promise.new` calls should come with a "definitely resolved in ..." comment
+explaining how this is avoided in each case.
 
 In the future, the 1-element history `old?` may be replaced with a global cache indexed by strong
 hashes but the promise will still need to be passed through the elaborator.
@@ -155,36 +151,6 @@ structure SnapshotBundle (α : Type) where
   -/
   new  : IO.Promise α
 
-/--
-Runs `act` with a newly created promise and finally resolves it to `default` if not done by `act`.
-
-Always resolving promises involved in the snapshot tree is important to avoid deadlocking the
-language server.
--/
-def withAlwaysResolvedPromise [Monad m] [MonadLiftT BaseIO m] [MonadFinally m] [Inhabited α]
-    (act : IO.Promise α → m Unit) : m Unit := do
-  let p ← IO.Promise.new
-  try
-    act p
-  finally
-    p.resolve default
-
-/--
-Runs `act` with `count` newly created promises and finally resolves them to `default` if not done by
-`act`.
-
-Always resolving promises involved in the snapshot tree is important to avoid deadlocking the
-language server.
--/
-def withAlwaysResolvedPromises [Monad m] [MonadLiftT BaseIO m] [MonadFinally m] [Inhabited α]
-    (count : Nat) (act : Array (IO.Promise α) → m Unit) : m Unit := do
-  let ps ← List.iota count |>.toArray.mapM fun _ => IO.Promise.new
-  try
-    act ps
-  finally
-    for p in ps do
-      p.resolve default
-
 /--
   Tree of snapshots where each snapshot comes with an array of asynchronous further subtrees. Used
   for asynchronously collecting information about the entirety of snapshots in the language server.

src/Lean/Language/Lean.lean

@@ -63,61 +63,36 @@ we remain at "go two commands up" at this point.
 
 Because of Lean's use of persistent data structures, incremental reuse of fully elaborated commands
 is easy because we can simply snapshot the entire state after each command and then restart
-elaboration using the stored state at the next command above the point of change. However,
-incrementality *within* elaboration of a single command such as between tactic steps is much harder
-because the existing control flow does not allow us to simply return from those points to the
-language processor in a way that we can later resume from there. Instead, we exchange the need for
-continuations with some limited mutability: by allocating an `IO.Promise` "cell" in the language
-processor, we can both pass it to the elaborator to eventually fill it using `Promise.resolve` as
-well as convert it to a `Task` that will wait on that resolution using `Promise.result` and return
-it as part of the command snapshot created by the language processor. The elaborator can then in
-turn create new promises itself and store their `result` when resolving an outer promise to create
-an arbitrary tree of promise-backed snapshot tasks. Thus, we can enable incremental reporting and
-reuse inside the elaborator using the same snapshot tree data structures as outside without having
-to change the elaborator's control flow.
+elaboration using the stored state at the point of change. However, incrementality within
+elaboration of a single command such as between tactic steps is much harder because we cannot simply
+return from those points to the language processor in a way that we can later resume from there.
+Instead, we exchange the need for continuations with some limited mutability: by allocating an
+`IO.Promise` "cell" in the language processor, we can both pass it to the elaborator to eventually
+fill it using `Promise.resolve` as well as convert it to a `Task` that will wait on that resolution
+using `Promise.result` and return it as part of the command snapshot created by the language
+processor. The elaborator can then create new promises itself and store their `result` when
+resolving an outer promise to create an arbitrary tree of promise-backed snapshot tasks. Thus, we
+can enable incremental reporting and reuse inside the elaborator using the same snapshot tree data
+structures as outside without having to change the elaborator's control flow.
 
 While ideally we would decide what can be reused during command elaboration using strong hashes over
-the full state and inputs, currently we rely on simpler syntactic checks: if all the syntax
-inspected up to a certain point is unchanged, we can assume that the old state can be reused. The
-central `SnapshotBundle` type passed inwards through the elaborator for this purpose combines the
-following data:
+the state and inputs, currently we rely on simpler syntactic checks: if all the syntax inspected up
+to a certain point is unchanged, we can assume that the old state can be reused.  The central
+`SnapshotBundle` type passed inwards through the elaborator for this purpose combines the following
+data:
 * the `IO.Promise` to be resolved to an elaborator snapshot (whose type depends on the specific
-  elaborator part we're in, e.g. `TacticParsedSnapshot`, `BodyProcessedSnapshot`)
+  elaborator part we're in, e.g. `)
 * if there was a previous run:
   * a `SnapshotTask` holding the corresponding snapshot of the run
   * the relevant `Syntax` of the previous run to be compared before any reuse
 
 Note that as we do not wait for the previous run to finish before starting to elaborate the next
-one, the old `SnapshotTask` task may not be finished yet. Indeed, if we do find that we can reuse
-the contained state because of a successful syntax comparison, we always want to explicitly wait for
-the task instead of redoing the work. On the other hand, the `Syntax` is not surrounded by a task so
-that we can immediately access it for comparisons, even if the snapshot task may, eventually, give
-access to the same syntax tree.
+one, the `SnapshotTask` task may not be finished yet. Indeed, if we do find that we can reuse the
+contained state, we will want to explicitly wait for it instead of redoing the work. On the other
+hand, the `Syntax` is not surrounded by a task so that we can immediately access it for comparisons,
+even if the snapshot task may, eventually, give access to the same syntax tree.
 
-For the most part, inside an elaborator participating in incrementality, we just have to ensure that
-we stop forwarding the old run's data as soon as we notice a relevant difference between old and new
-syntax tree. For example, allowing incrementality inside the cdot tactic combinator is as simple as
-```
-builtin_initialize registerBuiltinIncrementalTactic ``cdot
-@[builtin_tactic cdot] def evalTacticCDot : Tactic := fun stx => do
-  ...
-  closeUsingOrAdmit do
-    -- save state before/after entering focus on `·`
-    ...
-    Term.withNarrowedArgTacticReuse (argIdx := 1) evalTactic stx
-```
-The `Term.withNarrowedArgTacticReuse` combinator will focus on the given argument of `stx`, which in
-this case is the nested tactic sequence, and run `evalTactic` on it. But crucially, it will first
-compare all preceding arguments, in this case the cdot token itself, with the old syntax in the
-current snapshot bundle, which in the case of tactics is stored in `Term.Context.tacSnap?`. Indeed
-it is important here to check if the cdot token is identical because its position has been saved in
-the info tree, so it would be bad if we later restored some old state that uses a different position
-for it even if everything else is unchanged.  If there is any mismatch, the bundle's old value is
-set to `none` in order to prevent reuse from this point on. Note that in any case we still want to
-forward the "new" promise in order to provide incremental reporting as well as to construct a
-snapshot tree for reuse in future document versions! Note also that we explicitly opted into
-incrementality using `registerBuiltinIncrementalTactic` as any tactic combinator not written with
-these concerns in mind would likely misbehave under incremental reuse.
+TODO: tactic examples
 
 While it is generally true that we can provide incremental reporting even without reuse, we
 generally want to avoid that when it would be confusing/annoying, e.g. when a tactic block is run
@@ -126,24 +101,12 @@ purpose, we can disable both incremental modes using `Term.withoutTacticIncremen
 opted into incrementality because of other parts of the combinator. `induction` is an example of
 this because there are some induction alternatives that are run multiple times, so we disable all of
 incrementality for them.
-
-Using `induction` as a more complex example than `cdot` as it calls into `evalTactic` multiple
-times, here is a summary of what it has to do to implement incrementality:
-* `Narrow` down to the syntax of alternatives, disabling reuse if anything before them changed
-* allocate one new promise for each given alternative, immediately resolve passed promise to a new
-  snapshot tree node holding them so that the language server can wait on them
-* when executing an alternative,
-  * we put the corresponding promise into the context
-  * we disable reuse if anything in front of the contained tactic block has changed, including
-    previous alternatives
-  * we disable reuse *and reporting* if the tactic block is run multiple times, e.g. in the case of
-    a wildcard pattern
 -/
 
 set_option linter.missingDocs true
 
 namespace Lean.Language.Lean
-open Lean.Elab Command
+open Lean.Elab
 open Lean.Parser
 
 private def pushOpt (a? : Option α) (as : Array α) : Array α :=
@@ -158,6 +121,12 @@ register_builtin_option stderrAsMessages : Bool := {
   descr    := "(server) capture output to the Lean stderr channel (such as from `dbg_trace`) during elaboration of a command as a diagnostic message"
 }
 
+/-- Option for showing elaboration errors from partial syntax errors. -/
+register_builtin_option showPartialSyntaxErrors : Bool := {
+  defValue := false
+  descr    := "show elaboration errors from partial syntax trees (i.e. after parser recovery)"
+}
+
 /-! The hierarchy of Lean snapshot types -/
 
 /-- Snapshot after elaboration of the entire command. -/
@@ -196,7 +165,7 @@ deriving Nonempty
 abbrev CommandParsedSnapshot.data : CommandParsedSnapshot → CommandParsedSnapshotData
   | mk data _ => data
 /-- Next command, unless this is a terminal command. -/
-abbrev CommandParsedSnapshot.nextCmdSnap? : CommandParsedSnapshot →
+abbrev CommandParsedSnapshot.next? : CommandParsedSnapshot →
     Option (SnapshotTask CommandParsedSnapshot)
   | mk _ next? => next?
 partial instance : ToSnapshotTree CommandParsedSnapshot where
@@ -204,7 +173,18 @@ partial instance : ToSnapshotTree CommandParsedSnapshot where
     go s := ⟨s.data.toSnapshot,
       #[s.data.elabSnap.map (sync := true) toSnapshotTree,
         s.data.finishedSnap.map (sync := true) toSnapshotTree] |>
-        pushOpt (s.nextCmdSnap?.map (·.map (sync := true) go))⟩
+        pushOpt (s.next?.map (·.map (sync := true) go))⟩
+
+
+/-- Cancels all significant computations from this snapshot onwards. -/
+partial def CommandParsedSnapshot.cancel (snap : CommandParsedSnapshot) : BaseIO Unit := do
+  -- This is the only relevant computation right now, everything else is promises
+  -- TODO: cancel additional elaboration tasks (which will be tricky with `DynamicSnapshot`) if we
+  -- add them without switching to implicit cancellation
+  snap.data.finishedSnap.cancel
+  if let some next := snap.next? then
+    -- recurse on next command (which may have been spawned just before we cancelled above)
+    let _ ← IO.mapTask (sync := true) (·.cancel) next.task
 
 /-- State after successful importing. -/
 structure HeaderProcessedState where
@@ -238,8 +218,6 @@ structure HeaderParsedSnapshot extends Snapshot where
   /-- State after successful parsing. -/
   result? : Option HeaderParsedState
   isFatal := result?.isNone
-  /-- Cancellation token for interrupting processing of this run. -/
-  cancelTk? : Option IO.CancelToken
 
 instance : ToSnapshotTree HeaderParsedSnapshot where
   toSnapshotTree s := ⟨s.toSnapshot,
@@ -257,10 +235,6 @@ abbrev InitialSnapshot := HeaderParsedSnapshot
 structure LeanProcessingContext extends ProcessingContext where
   /-- Position of the first file difference if there was a previous invocation. -/
   firstDiffPos? : Option String.Pos
-  /-- Cancellation token of the previous invocation, if any. -/
-  oldCancelTk? : Option IO.CancelToken
-  /-- Cancellation token of the current run. -/
-  newCancelTk : IO.CancelToken
 
 /-- Monad transformer holding all relevant data for Lean processing. -/
 abbrev LeanProcessingT m := ReaderT LeanProcessingContext m
@@ -273,18 +247,6 @@ instance : MonadLift LeanProcessingM (LeanProcessingT IO) where
 instance : MonadLift (ProcessingT m) (LeanProcessingT m) where
   monadLift := fun act ctx => act ctx.toProcessingContext
 
-/--
-Embeds a `LeanProcessingM` action into `ProcessingM`, optionally using the old input string to speed
-up reuse analysis and supplying a cancellation token that should be triggered as soon as reuse is
-ruled out.
--/
-def LeanProcessingM.run (act : LeanProcessingM α) (oldInputCtx? : Option InputContext)
-    (oldCancelTk? : Option IO.CancelToken := none) : ProcessingM α := do
-  -- compute position of syntactic change once
-  let firstDiffPos? := oldInputCtx?.map (·.input.firstDiffPos (← read).input)
-  let newCancelTk ← IO.CancelToken.new
-  ReaderT.adapt ({ · with firstDiffPos?, oldCancelTk?, newCancelTk }) act
-
 /--
 Returns true if there was a previous run and the given position is before any textual change
 compared to it.
@@ -329,7 +291,8 @@ General notes:
   state. As there is no cheap way to check whether the `Environment` is unchanged, i.e. *semantic*
   change detection is currently not possible, we must make sure to pass `none` as all follow-up
   "previous states" from the first *syntactic* change onwards.
-* We must make sure to trigger `oldCancelTk?` as soon as discarding `old?`.
+* We must make sure to use `CommandParsedSnapshot.cancel` on such tasks when discarding them, i.e.
+  when not passing them along in `old?`.
 * Control flow up to finding the last still-valid snapshot (which should be quick) is synchronous so
   as not to report this "fast forwarding" to the user as well as to make sure the next run sees all
   fast-forwarded snapshots without having to wait on tasks.
@@ -337,47 +300,40 @@ General notes:
 partial def process
     (setupImports : Syntax → ProcessingT IO (Except HeaderProcessedSnapshot SetupImportsResult))
     (old? : Option InitialSnapshot) : ProcessingM InitialSnapshot := do
-  parseHeader old? |>.run (old?.map (·.ictx)) (old?.bind (·.cancelTk?))
+  -- compute position of syntactic change once
+  let firstDiffPos? := old?.map (·.ictx.input.firstDiffPos (← read).input)
+  ReaderT.adapt ({ · with firstDiffPos? }) do
+    parseHeader old?
 where
   parseHeader (old? : Option HeaderParsedSnapshot) : LeanProcessingM HeaderParsedSnapshot := do
     let ctx ← read
     let ictx := ctx.toInputContext
-    let unchanged old newParserState :=
+    let unchanged old :=
       -- when header syntax is unchanged, reuse import processing task as is and continue with
       -- parsing the first command, synchronously if possible
-      -- NOTE: even if the syntax tree is functionally unchanged, the new parser state may still
-      -- have changed because of trailing whitespace and comments etc., so it is passed separately
-      -- from `old`
       if let some oldSuccess := old.result? then
-        return {
-          ictx
-          stx := old.stx
-          diagnostics := old.diagnostics
-          cancelTk? := ctx.newCancelTk
-          result? := some { oldSuccess with
-            processedSnap := (← oldSuccess.processedSnap.bindIO (sync := true) fun oldProcessed => do
-              if let some oldProcSuccess := oldProcessed.result? then
-                -- also wait on old command parse snapshot as parsing is cheap and may allow for
-                -- elaboration reuse
-                oldProcSuccess.firstCmdSnap.bindIO (sync := true) fun oldCmd =>
-                  return .pure { oldProcessed with result? := some { oldProcSuccess with
-                    firstCmdSnap := (← parseCmd oldCmd newParserState oldProcSuccess.cmdState ctx) } }
-              else
-                return .pure oldProcessed) } }
+        return { old with ictx, result? := some { oldSuccess with
+          processedSnap := (← oldSuccess.processedSnap.bindIO (sync := true) fun oldProcessed => do
+            if let some oldProcSuccess := oldProcessed.result? then
+              -- also wait on old command parse snapshot as parsing is cheap and may allow for
+              -- elaboration reuse
+              oldProcSuccess.firstCmdSnap.bindIO (sync := true) fun oldCmd =>
+                return .pure { oldProcessed with result? := some { oldProcSuccess with
+                  firstCmdSnap := (← parseCmd oldCmd oldSuccess.parserState oldProcSuccess.cmdState ctx) } }
+            else
+              return .pure oldProcessed) } }
       else return old
 
     -- fast path: if we have parsed the header successfully...
     if let some old := old? then
-      if let some oldSuccess := old.result? then
-        if let some (some processed) ← old.processedResult.get? then
-          -- ...and the edit location is after the next command (see note [Incremental Parsing])...
-          if let some nextCom ← processed.firstCmdSnap.get? then
-            if (← isBeforeEditPos nextCom.data.parserState.pos) then
-              -- ...go immediately to next snapshot
-              return (← unchanged old oldSuccess.parserState)
+      if let some (some processed) ← old.processedResult.get? then
+        -- ...and the edit location is after the next command (see note [Incremental Parsing])...
+        if let some nextCom ← processed.firstCmdSnap.get? then
+          if (← isBeforeEditPos nextCom.data.parserState.pos) then
+            -- ...go immediately to next snapshot
+            return (← unchanged old)
 
-    withHeaderExceptions ({ · with
-        ictx, stx := .missing, result? := none, cancelTk? := none }) do
+    withHeaderExceptions ({ · with ictx, stx := .missing, result? := none }) do
       -- parsing the header should be cheap enough to do synchronously
       let (stx, parserState, msgLog) ← Parser.parseHeader ictx
       if msgLog.hasErrors then
@@ -385,7 +341,6 @@ where
           ictx, stx
           diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog)
           result? := none
-          cancelTk? := none
         }
 
       -- semi-fast path: go to next snapshot if syntax tree is unchanged AND we're still in front
@@ -396,11 +351,14 @@ where
       -- influence the range of error messages such as from a trailing `exact`
       if let some old := old? then
         if (← isBeforeEditPos parserState.pos) && old.stx == stx then
-          -- Here we must make sure to pass the *new* parser state; see NOTE in `unchanged`
-          return (← unchanged old parserState)
-        -- on first change, make sure to cancel old invocation
-        if let some tk := ctx.oldCancelTk? then
-          tk.set
+          return (← unchanged old)
+        -- on first change, make sure to cancel all further old tasks
+        if let some oldSuccess := old.result? then
+          oldSuccess.processedSnap.cancel
+          let _ ← BaseIO.mapTask (t := oldSuccess.processedSnap.task) fun processed => do
+            if let some oldProcSuccess := processed.result? then
+              let _ ← BaseIO.mapTask (·.cancel) oldProcSuccess.firstCmdSnap.task
+
       return {
         ictx, stx
         diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog)
@@ -408,7 +366,6 @@ where
           parserState
           processedSnap := (← processHeader stx parserState)
         }
-        cancelTk? := ctx.newCancelTk
       }
 
   processHeader (stx : Syntax) (parserState : Parser.ModuleParserState) :
@@ -460,7 +417,7 @@ where
 
     -- check for cancellation, most likely during elaboration of previous command, before starting
     -- processing of next command
-    if (← ctx.newCancelTk.isSet) then
+    if (← IO.checkCanceled) then
       -- this is a bit ugly as we don't want to adjust our API with `Option`s just for cancellation
       -- (as no-one should look at this result in that case) but anything containing `Environment`
       -- is not `Inhabited`
@@ -471,25 +428,22 @@ where
         tacticCache := (← IO.mkRef {})
       }
 
-    let unchanged old newParserState : BaseIO CommandParsedSnapshot :=
+    let unchanged old : BaseIO CommandParsedSnapshot :=
       -- when syntax is unchanged, reuse command processing task as is
-      -- NOTE: even if the syntax tree is functionally unchanged, the new parser state may still
-      -- have changed because of trailing whitespace and comments etc., so it is passed separately
-      -- from `old`
-      if let some oldNext := old.nextCmdSnap? then
+      if let some oldNext := old.next? then
         return .mk (data := old.data)
           (nextCmdSnap? := (← old.data.finishedSnap.bindIO (sync := true) fun oldFinished =>
-            -- also wait on old command parse snapshot as parsing is cheap and may allow for
-            -- elaboration reuse
-            oldNext.bindIO (sync := true) fun oldNext => do
-              parseCmd oldNext newParserState oldFinished.cmdState ctx))
+              -- also wait on old command parse snapshot as parsing is cheap and may allow for
+              -- elaboration reuse
+              oldNext.bindIO (sync := true) fun oldNext => do
+                parseCmd oldNext old.data.parserState oldFinished.cmdState ctx))
       else return old  -- terminal command, we're done!
 
     -- fast path, do not even start new task for this snapshot
     if let some old := old? then
-      if let some nextCom ← old.nextCmdSnap?.bindM (·.get?) then
+      if let some nextCom ← old.next?.bindM (·.get?) then
         if (← isBeforeEditPos nextCom.data.parserState.pos) then
-          return .pure (← unchanged old old.data.parserState)
+          return .pure (← unchanged old)
 
     SnapshotTask.ofIO (some ⟨parserState.pos, ctx.input.endPos⟩) do
       let beginPos := parserState.pos
@@ -504,19 +458,15 @@ where
       -- semi-fast path
       if let some old := old? then
         if (← isBeforeEditPos parserState.pos ctx) && old.data.stx == stx then
-          -- Here we must make sure to pass the *new* parser state; see NOTE in `unchanged`
-          return (← unchanged old parserState)
-        -- on first change, make sure to cancel old invocation
-        -- TODO: pass token into incrementality-aware elaborators to improve reuse of still-valid,
-        -- still-running elaboration steps?
-        if let some tk := ctx.oldCancelTk? then
-          tk.set
+          return (← unchanged old)
+        -- on first change, make sure to cancel all further old tasks
+        old.cancel
 
       -- definitely resolved in `doElab` task
       let elabPromise ← IO.Promise.new
       let tacticCache ← old?.map (·.data.tacticCache) |>.getDM (IO.mkRef {})
       let finishedSnap ←
-        doElab stx cmdState beginPos
+        doElab stx cmdState msgLog.hasErrors beginPos
           { old? := old?.map fun old => ⟨old.data.stx, old.data.elabSnap⟩, new := elabPromise }
           tacticCache
           ctx
@@ -529,24 +479,19 @@ where
         diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog)
         stx
         parserState
-        elabSnap := { range? := stx.getRange?, task := elabPromise.result }
+        elabSnap := { range? := finishedSnap.range?, task := elabPromise.result }
         finishedSnap
         tacticCache
       }
 
-  doElab (stx : Syntax) (cmdState : Command.State) (beginPos : String.Pos)
+  doElab (stx : Syntax) (cmdState : Command.State) (hasParseError : Bool) (beginPos : String.Pos)
       (snap : SnapshotBundle DynamicSnapshot) (tacticCache : IO.Ref Tactic.Cache) :
       LeanProcessingM (SnapshotTask CommandFinishedSnapshot) := do
     let ctx ← read
-    -- (Try to) use last line of command as range for final snapshot task. This ensures we do not
-    -- retract the progress bar to a previous position in case the command support incremental
-    -- reporting but has significant work after resolving its last incremental promise, such as
-    -- final type checking; if it does not support incrementality, `elabSnap` constructed in
-    -- `parseCmd` and containing the entire range of the command will determine the reported
-    -- progress and be resolved effectively at the same time as this snapshot task, so `tailPos` is
-    -- irrelevant in this case.
-    let tailPos := stx.getTailPos? |>.getD beginPos
-    SnapshotTask.ofIO (some ⟨tailPos, tailPos⟩) do
+
+    -- signature elaboration task; for now, does full elaboration
+    -- TODO: do tactic snapshots, reuse old state for them
+    SnapshotTask.ofIO (stx.getRange?.getD ⟨beginPos, beginPos⟩) do
       let scope := cmdState.scopes.head!
       let cmdStateRef ← IO.mkRef { cmdState with messages := .empty }
       /-
@@ -560,18 +505,26 @@ where
         cmdPos       := beginPos
         tacticCache? := some tacticCacheNew
         snap?        := some snap
-        cancelTk?    := some ctx.newCancelTk
       }
       let (output, _) ←
         IO.FS.withIsolatedStreams (isolateStderr := stderrAsMessages.get scope.opts) do
           liftM (m := BaseIO) do
-            withLoggingExceptions
+            Elab.Command.catchExceptions
               (getResetInfoTrees *> Elab.Command.elabCommandTopLevel stx)
               cmdCtx cmdStateRef
       let postNew := (← tacticCacheNew.get).post
       tacticCache.modify fun _ => { pre := postNew, post := {} }
       let cmdState ← cmdStateRef.get
       let mut messages := cmdState.messages
+      -- `stx.hasMissing` should imply `hasParseError`, but the latter should be cheaper to check in
+      -- general
+      if !showPartialSyntaxErrors.get cmdState.scopes[0]!.opts && hasParseError &&
+          stx.hasMissing then
+        -- discard elaboration errors, except for a few important and unlikely misleading ones, on
+        -- parse error
+        messages := ⟨messages.msgs.filter fun msg =>
+          msg.data.hasTag (fun tag => tag == `Elab.synthPlaceholder ||
+            tag == `Tactic.unsolvedGoals || (`_traceMsg).isSuffixOf tag)⟩
       if !output.isEmpty then
         messages := messages.add {
           fileName := ctx.fileName
@@ -588,25 +541,13 @@ where
         cmdState
       }
 
-/--
-Convenience function for tool uses of the language processor that skips header handling.
--/
-def processCommands (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState)
-    (commandState : Command.State)
-    (old? : Option (Parser.InputContext × CommandParsedSnapshot) := none) :
-    BaseIO (SnapshotTask CommandParsedSnapshot) := do
-  process.parseCmd (old?.map (·.2)) parserState commandState
-    |>.run (old?.map (·.1))
-    |>.run { inputCtx with }
-
-
 /-- Waits for and returns final environment, if importing was successful. -/
 partial def waitForFinalEnv? (snap : InitialSnapshot) : Option Environment := do
   let snap ← snap.result?
   let snap ← snap.processedSnap.get.result?
   goCmd snap.firstCmdSnap.get
 where goCmd snap :=
-  if let some next := snap.nextCmdSnap? then
+  if let some next := snap.next? then
     goCmd next.get
   else
     snap.data.finishedSnap.get.cmdState.env

src/Lean/Message.lean

@@ -77,7 +77,7 @@ inductive MessageData where
 
   The `Dynamic` value is expected to be a `MessageData`,
   which is a workaround for the positivity restriction.
-
+     
   If the thunked message is produced for a term that contains a synthetic sorry,
   `hasSyntheticSorry` should return `true`.
   This is used to filter out certain messages. -/
@@ -298,69 +298,47 @@ protected def toJson (msg : Message) : IO Json := do
 
 end Message
 
-/--
-A persistent array of messages.
-
-In the Lean elaborator, we use a fresh message log per command but may also report diagnostics at
-various points inside a command, which will empty `unreported` and updated `hadErrors` accordingly
-(see `CoreM.getAndEmptyMessageLog`).
--/
+/-- A persistent array of messages. -/
 structure MessageLog where
-  /--
-  If true, there was an error in the log previously that has already been reported to the user and
-  removed from the log. Thus we say that in the current context (usually the current command), we
-  "have errors" if either this flag is set or there is an error in `msgs`; see
-  `MessageLog.hasErrors`. If we have errors, we suppress some error messages that are often the
-  result of a previous error.
-  -/
-  /-
-  Design note: We considered introducing a `hasErrors` field instead that already includes the
-  presence of errors in `msgs` but this would not be compatible with e.g.
-  `MessageLog.errorsToWarnings`.
-  -/
-  hadErrors : Bool := false
-  /-- The list of messages not already reported, in insertion order. -/
-  unreported : PersistentArray Message := {}
+  msgs : PersistentArray Message := {}
   deriving Inhabited
 
 namespace MessageLog
-def empty : MessageLog := {}
+def empty : MessageLog := ⟨{}⟩
 
-@[deprecated "renamed to `unreported`; direct access should in general be avoided in favor of \
-using `MessageLog.toList/toArray`"]
-def msgs : MessageLog → PersistentArray Message := unreported
-
-def hasUnreported (log : MessageLog) : Bool :=
-  !log.unreported.isEmpty
+def isEmpty (log : MessageLog) : Bool :=
+  log.msgs.isEmpty
 
 def add (msg : Message) (log : MessageLog) : MessageLog :=
-  { log with unreported := log.unreported.push msg }
+  ⟨log.msgs.push msg⟩
 
 protected def append (l₁ l₂ : MessageLog) : MessageLog :=
-  { hadErrors := l₁.hadErrors || l₂.hadErrors, unreported := l₁.unreported ++ l₂.unreported }
+  ⟨l₁.msgs ++ l₂.msgs⟩
 
 instance : Append MessageLog :=
   ⟨MessageLog.append⟩
 
 def hasErrors (log : MessageLog) : Bool :=
-  log.hadErrors || log.unreported.any (·.severity matches .error)
+  log.msgs.any fun m => match m.severity with
+    | MessageSeverity.error => true
+    | _                     => false
 
 def errorsToWarnings (log : MessageLog) : MessageLog :=
-  { unreported := log.unreported.map (fun m => match m.severity with | MessageSeverity.error => { m with severity := MessageSeverity.warning } | _ => m) }
+  { msgs := log.msgs.map (fun m => match m.severity with | MessageSeverity.error => { m with severity := MessageSeverity.warning } | _ => m) }
 
 def getInfoMessages (log : MessageLog) : MessageLog :=
-  { unreported := log.unreported.filter fun m => match m.severity with | MessageSeverity.information => true | _ => false }
+  { msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.information => true | _ => false }
 
 def forM {m : Type → Type} [Monad m] (log : MessageLog) (f : Message → m Unit) : m Unit :=
-  log.unreported.forM f
+  log.msgs.forM f
 
-/-- Converts the unreported messages to a list, oldest message first. -/
+/-- Converts the log to a list, oldest message first. -/
 def toList (log : MessageLog) : List Message :=
-  log.unreported.toList
+  log.msgs.toList
 
-/-- Converts the unreported messages to an array, oldest message first. -/
+/-- Converts the log to an array, oldest message first. -/
 def toArray (log : MessageLog) : Array Message :=
-  log.unreported.toArray
+  log.msgs.toArray
 
 end MessageLog
 

src/Lean/Meta/Basic.lean

@@ -304,7 +304,7 @@ structure State where
   Backtrackable state for the `MetaM` monad.
 -/
 structure SavedState where
-  core        : Core.SavedState
+  core        : Core.State
   meta        : State
   deriving Nonempty
 
@@ -410,22 +410,20 @@ instance : AddMessageContext MetaM where
   addMessageContext := addMessageContextFull
 
 protected def saveState : MetaM SavedState :=
-  return { core := (← Core.saveState), meta := (← get) }
+  return { core := (← getThe Core.State), meta := (← get) }
 
 /-- Restore backtrackable parts of the state. -/
 def SavedState.restore (b : SavedState) : MetaM Unit := do
-  b.core.restore
+  Core.restore b.core
   modify fun s => { s with mctx := b.meta.mctx, zetaDeltaFVarIds := b.meta.zetaDeltaFVarIds, postponed := b.meta.postponed }
 
-@[specialize, inherit_doc Core.withRestoreOrSaveFull]
-def withRestoreOrSaveFull (reusableResult? : Option (α × SavedState))
-    (cont : MetaM SavedState → MetaM α) : MetaM α := do
-  if let some (_, state) := reusableResult? then
-    set state.meta
-  let reusableResult? := reusableResult?.map (fun (val, state) => (val, state.core))
-  controlAt CoreM fun runInCoreM =>
-    Core.withRestoreOrSaveFull reusableResult? fun restore =>
-      runInCoreM <| cont (return { core := (← restore), meta := (← get) })
+/--
+Restores full state including sources for unique identifiers. Only intended for incremental reuse
+between elaboration runs, not for backtracking within a single run.
+-/
+def SavedState.restoreFull (b : SavedState) : MetaM Unit := do
+  Core.restoreFull b.core
+  set b.meta
 
 instance : MonadBacktrack SavedState MetaM where
   saveState      := Meta.saveState

src/Lean/Parser/Module.lean

@@ -141,7 +141,7 @@ partial def testParseModuleAux (env : Environment) (inputCtx : InputContext) (s
     match parseCommand inputCtx { env := env, options := {} } state msgs with
     | (stx, state, msgs) =>
       if isTerminalCommand stx then
-        if !msgs.hasUnreported then
+        if msgs.isEmpty then
           pure stxs
         else do
           msgs.forM fun msg => msg.toString >>= IO.println

src/Lean/Server/FileWorker.lean

@@ -196,7 +196,7 @@ This option can only be set on the command line, not in the lakefile or via `set
         return .pure ()
   where
     go (node : SnapshotTree) (st : ReportSnapshotsState) : BaseIO (Task ReportSnapshotsState) := do
-      if node.element.diagnostics.msgLog.hasUnreported then
+      if !node.element.diagnostics.msgLog.isEmpty then
         let diags ←
           if let some memorized ← node.element.diagnostics.interactiveDiagsRef?.bindM fun ref => do
               return (← ref.get).bind (·.get? MemorizedInteractiveDiagnostics) then

src/Lean/Server/FileWorker/Utils.lean

@@ -15,6 +15,22 @@ namespace Lean.Server.FileWorker
 open Snapshots
 open IO
 
+structure CancelToken where
+  ref : IO.Ref Bool
+
+namespace CancelToken
+
+def new : IO CancelToken :=
+  CancelToken.mk <$> IO.mkRef false
+
+def set (tk : CancelToken) : BaseIO Unit :=
+  tk.ref.set true
+
+def isSet (tk : CancelToken) : BaseIO Bool :=
+  tk.ref.get
+
+end CancelToken
+
 -- TEMP: translate from new heterogeneous snapshot tree to old homogeneous async list
 private partial def mkCmdSnaps (initSnap : Language.Lean.InitialSnapshot) :
     AsyncList IO.Error Snapshot := Id.run do
@@ -33,7 +49,7 @@ where
         stx := cmdParsed.data.stx
         mpState := cmdParsed.data.parserState
         cmdState := finished.cmdState
-      } (match cmdParsed.nextCmdSnap? with
+      } (match cmdParsed.next? with
         | some next => .delayed <| next.task.bind go
         | none => .nil)
 

src/Lean/Server/Snapshots.lean

@@ -59,7 +59,6 @@ def runCommandElabM (snap : Snapshot) (meta : DocumentMeta) (c : CommandElabM α
     fileMap := meta.text,
     tacticCache? := none
     snap? := none
-    cancelTk? := none
   }
   c.run ctx |>.run' snap.cmdState
 

src/Lean/Syntax.lean

@@ -30,9 +30,6 @@ def SourceInfo.updateTrailing (trailing : Substring) : SourceInfo → SourceInfo
   | SourceInfo.original leading pos _ endPos => SourceInfo.original leading pos trailing endPos
   | info                                     => info
 
-def SourceInfo.getRange? (canonicalOnly := false) (info : SourceInfo) : Option String.Range :=
-  return ⟨(← info.getPos? canonicalOnly), (← info.getTailPos? canonicalOnly)⟩
-
 /-! # Syntax AST -/
 
 inductive IsNode : Syntax → Prop where
@@ -83,34 +80,6 @@ end SyntaxNode
 
 namespace Syntax
 
-/--
-Compare syntax structures and position ranges, but not whitespace.
-We generally assume that if syntax trees equal in this way generate the same elaboration output,
-including positions contained in e.g. diagnostics and the info tree.
--/
-partial def structRangeEq : Syntax → Syntax → Bool
-  | .missing, .missing => true
-  | .node info k args, .node info' k' args' =>
-    info.getRange? == info'.getRange? && k == k' && args.isEqv args' structRangeEq
-  | .atom info val, .atom info' val' => info.getRange? == info'.getRange? && val == val'
-  | .ident info rawVal val preresolved, .ident info' rawVal' val' preresolved' =>
-    info.getRange? == info'.getRange? && rawVal == rawVal' && val == val' &&
-    preresolved == preresolved'
-  | _, _ => false
-
-/-- Like `structRangeEq` but prints trace on failure if `trace.Elab.reuse` is activated. -/
-def structRangeEqWithTraceReuse (opts : Options) (stx1 stx2 : Syntax) : Bool :=
-  if stx1.structRangeEq stx2 then
-    true
-  else
-    if opts.getBool `trace.Elab.reuse then
-      dbg_trace "reuse stopped:
-{stx1.formatStx (showInfo := true)} !=
-{stx2.formatStx (showInfo := true)}"
-      false
-    else
-      false
-
 def getAtomVal : Syntax → String
   | atom _ val => val
   | _          => ""
@@ -218,6 +187,13 @@ partial def updateTrailing (trailing : Substring) : Syntax → Syntax
      Syntax.node info k args
   | s => s
 
+partial def getTailWithPos : Syntax → Option Syntax
+  | stx@(atom info _)   => info.getPos?.map fun _ => stx
+  | stx@(ident info ..) => info.getPos?.map fun _ => stx
+  | node SourceInfo.none _ args => args.findSomeRev? getTailWithPos
+  | stx@(node ..) => stx
+  | _ => none
+
 open SourceInfo in
 /-- Split an `ident` into its dot-separated components while preserving source info.
 Macro scopes are first erased.  For example, `` `foo.bla.boo._@._hyg.4 `` ↦ `` [`foo, `bla, `boo] ``.

src/runtime/alloc.cpp

@@ -467,18 +467,14 @@ void finalize_alloc() {
 LEAN_THREAD_VALUE(uint64_t, g_heartbeat, 0);
 #endif
 
-void add_heartbeats(uint64_t count) {
-#ifdef LEAN_SMALL_ALLOCATOR
-    if (g_heap)
-        g_heap->m_heartbeat += count;
-#else
-    g_heartbeat += count;
-#endif
-}
-
 /* Helper function for increasing heartbeat even when LEAN_SMALL_ALLOCATOR is not defined */
 extern "C" LEAN_EXPORT void lean_inc_heartbeat() {
-    add_heartbeats(1);
+#ifdef LEAN_SMALL_ALLOCATOR
+    if (g_heap)
+        g_heap->m_heartbeat++;
+#else
+    g_heartbeat++;
+#endif
 }
 
 uint64_t get_num_heartbeats() {

src/runtime/alloc.h

@@ -12,7 +12,6 @@ namespace lean {
 void init_thread_heap();
 void * alloc(size_t sz);
 void dealloc(void * o, size_t sz);
-void add_heartbeats(uint64_t count);
 uint64_t get_num_heartbeats();
 void initialize_alloc();
 void finalize_alloc();

src/runtime/io.cpp

@@ -639,12 +639,6 @@ extern "C" LEAN_EXPORT obj_res lean_io_get_num_heartbeats(obj_arg /* w */) {
     return io_result_mk_ok(lean_uint64_to_nat(get_num_heartbeats()));
 }
 
-/* addHeartbeats (count : Int64) : BaseIO Unit */
-extern "C" LEAN_EXPORT obj_res lean_io_add_heartbeats(int64_t count, obj_arg /* w */) {
-    add_heartbeats(count);
-    return io_result_mk_ok(box(0));
-}
-
 extern "C" LEAN_EXPORT obj_res lean_io_getenv(b_obj_arg env_var, obj_arg) {
 #if defined(LEAN_EMSCRIPTEN)
     // HACK(WN): getenv doesn't seem to work in Emscripten even though it should

tests/lean/1079.lean.expected.out

@@ -1,4 +1,4 @@
-1079.lean:4:2-6:12: error: alternative 'isFalse' has not been provided
+1079.lean:3:2-6:12: error: alternative 'isFalse' has not been provided
 [Meta.Tactic.simp.rewrite] h:1000, m ==> n
 [Meta.Tactic.simp.rewrite] @eq_self:1000, n = n ==> True
 [Meta.Tactic.simp.unify] @eq_self:1000, failed to unify

tests/lean/inductionErrors.lean

@@ -77,5 +77,5 @@ theorem ex11 (p q : Nat) : p ≤ q ∨ p > q := by
   cases p, q using elimEx with
   | lower d => apply Or.inl; admit
   | upper d => apply Or.inr; admit
-  | lower d /- error duplicate -/ => apply Or.inl; admit
+  | lower d /- error unused -/ => apply Or.inl; admit
   | diag    => apply Or.inl; apply Nat.le_refl

tests/lean/inductionErrors.lean.expected.out

@@ -27,5 +27,5 @@ inductionErrors.lean:50:2-50:16: error: alternative 'cons' is not needed
 inductionErrors.lean:55:2-55:16: error: alternative 'cons' is not needed
 inductionErrors.lean:60:2-60:40: error: invalid alternative name 'upper2'
 inductionErrors.lean:66:2-66:28: error: invalid occurrence of wildcard alternative, it must be the last alternative
-inductionErrors.lean:74:2-74:34: error: unused alternative '_'
-inductionErrors.lean:80:2-80:56: error: unused alternative 'lower'
+inductionErrors.lean:74:2-74:34: error: unused alternative
+inductionErrors.lean:80:2-80:53: error: unused alternative

tests/lean/interactive/editAfterError.lean

@@ -1,4 +1,4 @@
 #check tru
 #check fal
-        --^ insert: "s"
+        --^ insert: s
         --^ collectDiagnostics

tests/lean/interactive/editAfterError.lean.expected.out

@@ -1,3 +1,9 @@
+{"textDocument": {"version": 2, "uri": "file:///editAfterError.lean"},
+ "contentChanges":
+ [{"text": "s",
+   "range":
+   {"start": {"line": 1, "character": 10},
+    "end": {"line": 1, "character": 11}}}]}
 {"version": 2,
  "uri": "file:///editAfterError.lean",
  "diagnostics":

tests/lean/interactive/editCompletion.lean

@@ -2,5 +2,5 @@ structure Foo where
   foo : Nat
 
 example (f : Foo) : f
-                   --^ insert: "."
+                   --^ insert: .
                     --^ textDocument/completion

tests/lean/interactive/editCompletion.lean.expected.out

@@ -1,3 +1,9 @@
+{"textDocument": {"version": 2, "uri": "file:///editCompletion.lean"},
+ "contentChanges":
+ [{"text": ".",
+   "range":
+   {"start": {"line": 3, "character": 21},
+    "end": {"line": 3, "character": 22}}}]}
 {"textDocument": {"uri": "file:///editCompletion.lean"},
  "position": {"line": 3, "character": 22}}
 {"items":

tests/lean/interactive/incrementalCombinator.lean

@@ -1,22 +0,0 @@
-/-! Incremental reuse in combinator -/
-
-def case (h : a ∨ b ∨ c) : True := by
-  cases h
-  case inr h =>
-    cases h
-    case inl =>
-      dbg_trace "c 0"
-      dbg_trace "c 1"
-      dbg_trace "c 2"
-                  --^ sync
-                  --^ insert: ".5"
-
--- RESET
-def case (h : a ∨ b) : True := by
-  cases h
-  . dbg_trace "d 0"
-    dbg_trace "d 1"
-    dbg_trace "d 2"
-                --^ sync
-                --^ insert: ".5"
-  dbg_trace "d 3"

tests/lean/interactive/incrementalCombinator.lean.expected.out

@@ -1,10 +0,0 @@
-c 0
-c 1
-c 2
-c 2.5
-d 0
-d 1
-d 2
-d 3
-d 2.5
-d 3

tests/lean/interactive/incrementalInduction.lean

@@ -1,72 +0,0 @@
-/-! Incremental reuse in `induction` -/
-
---set_option trace.Elab.reuse true
-
-theorem basic (n : Nat) : True := by
-  induction n with
-  | zero => sorry
-  | succ =>
-    dbg_trace "b 0"
-    dbg_trace "b 1"
-    dbg_trace "b 2"
-                --^ sync
-                --^ insert: ".5"
-
--- RESET
-theorem nonFirst (n : Nat) : True := by
-  induction n with
-  | zero =>
-    dbg_trace "n 0"
-    dbg_trace "n 1"
-                --^ sync
-                --^ insert: ".5"
-  | succ =>
-    dbg_trace "n 2"
-                --^ sync
-                --^ insert: ".5"
-
--- RESET
--- currently the pre-tac will be re-executed even if we can reuse a specific branch's tactics
-theorem preTac (n : Nat) : True := by
-  induction n with
-    dbg_trace "p -1"
-  | zero => sorry
-  | succ =>
-    dbg_trace "p 0"
-    dbg_trace "p 1"
-                --^ sync
-                --^ insert: ".5"
-
-/-! No reuse in cases where branch is run more than once -/
-
--- RESET
-theorem wildcard (n : Nat) : True := by
-  induction n with
-  | _ =>
-    dbg_trace "w 0"
-    dbg_trace "w 1"
-                --^ sync
-                --^ insert: ".5"
-
--- RESET
-theorem preTacMulti (x : Nat × Nat × Nat) : True := by
-  induction x with
-    cases x
-  | mk x =>
-    dbg_trace "pm 0"
-    dbg_trace "pm 1"
-                 --^ sync
-                 --^ insert: ".5"
-
--- RESET
-theorem cases (n : Nat) : True := by
-  cases n with
-  | zero =>
-    dbg_trace "c 0"
-    dbg_trace "c 1"
-                --^ sync
-                --^ insert: ".5"
-  | succ =>
-    dbg_trace "c 2"
-                --^ sync
-                --^ insert: ".5"

tests/lean/interactive/incrementalInduction.lean.expected.out

@@ -1,39 +0,0 @@
-b 0
-b 1
-b 2
-b 2.5
-n 0
-n 1
-n 2
-n 1.5
-n 2
-n 2.5
-p -1
-p -1
-p 0
-p 1
-p -1
-p -1
-p 1.5
-w 0
-w 1
-w 0
-w 1
-w 0
-w 1.5
-w 0
-w 1.5
-pm 0
-pm 1
-pm 0
-pm 1
-pm 0
-pm 1.5
-pm 0
-pm 1.5
-c 0
-c 1
-c 2
-c 1.5
-c 2
-c 2.5

tests/lean/interactive/incrementalMutual.lean

@@ -1,31 +0,0 @@
-/-! Incremental reuse in `mutual` -/
-
-/-! should invalidate body of `b1` only -/
-
-mutual
-def b0 : (by dbg_trace "b 0 0"; exact Nat) := (by dbg_trace "b 0 1"; exact 0)
-
-def b1 : (by dbg_trace "b 1 0"; exact Nat) := (by dbg_trace "b 1 1"; exact 0)
-                                                                --^ sync
-                                                                --^ insert: ".5"
-end
-
-/-! should invalidate both bodies (and, in current impl, second header) -/
-
--- RESET
-mutual
-def f0 : (by dbg_trace "f 0 0"; exact Nat) := (by dbg_trace "f 0 1"; exact 0)
-                                                                --^ sync
-                                                                --^ insert: ".5"
-def f1 : (by dbg_trace "f 1 0"; exact Nat) := (by dbg_trace "f 1 1"; exact 0)
-end
-
-/-! should invalidate everything but header of `h0` -/
-
--- RESET
-mutual
-def h0 : (by dbg_trace "h 0 0"; exact Nat) := (by dbg_trace "h 0 1"; exact 0)
-def h1 : (by dbg_trace "h 1 0"; exact Nat) := (by dbg_trace "h 1 1"; exact 0)
-                           --^ sync
-                           --^ insert: ".5"
-end

tests/lean/interactive/incrementalMutual.lean.expected.out

@@ -1,19 +0,0 @@
-b 0 0
-b 1 0
-b 0 1
-b 1 1
-b 1 1.5
-f 0 0
-f 1 0
-f 0 1
-f 1 1
-f 1 0
-f 0 1.5
-f 1 1
-h 0 0
-h 1 0
-h 0 1
-h 1 1
-h 1 0.5
-h 0 1
-h 1 1

tests/lean/interactive/incrementalTactic.lean

@@ -1,45 +0,0 @@
-/-! Basic incremental reuse in top-level tactic block -/
-
--- set_option trace.Elab.reuse true
-
-def basic : True := by
-  dbg_trace "b 0"
-  apply id
-  dbg_trace "b 1"
-  apply id
-  dbg_trace "b 2"
-              --^ sync
-              --^ insert: ".5"
-
--- RESET
-def trailingWhitespace : True := by
-  dbg_trace "t 0"
-  dbg_trace "t 1"
-  dbg_trace "t 2"
-               --^ sync
-               --^ insert: "\n "
-
-
--- RESET
--- this used to restore the wrong elab state because of input context mis-tracking
-def haveBug : True := by
-  have (a : Nat) : Nat → True := by
-    intro n m
-  --^ sync
-  --^ delete: "intro n m"
-  --^ sync
-  --^ insert: "intro n m"
-  --^ collectDiagnostics
-    exact m
-
-/-! incremental reporting should obey `showPartialSyntaxErrors` -/
--- RESET
-def partialSyntax : True := by apply (
---^ collectDiagnostics
-
-/-! A tactic block not supported by incrementality should not accidentally swallow messages. -/
--- RESET
-def otherMessage : Nat × Nat where
-  fst := no
-  snd := by skip
---^ collectDiagnostics

tests/lean/interactive/incrementalTactic.lean.expected.out

@@ -1,55 +0,0 @@
-b 0
-b 1
-b 2
-b 2.5
-t 0
-t 1
-t 2
-{"version": 3,
- "uri": "file:///incrementalTactic.lean",
- "diagnostics":
- [{"source": "Lean 4",
-   "severity": 1,
-   "range":
-   {"start": {"line": 4, "character": 4}, "end": {"line": 4, "character": 13}},
-   "message":
-   "tactic 'introN' failed, insufficient number of binders\na n : Nat\n⊢ True",
-   "fullRange":
-   {"start": {"line": 4, "character": 4}, "end": {"line": 4, "character": 13}}},
-  {"source": "Lean 4",
-   "severity": 1,
-   "range":
-   {"start": {"line": 2, "character": 22}, "end": {"line": 3, "character": 0}},
-   "message": "unsolved goals\nthis : Nat → Nat → True\n⊢ True",
-   "fullRange":
-   {"start": {"line": 2, "character": 22},
-    "end": {"line": 10, "character": 11}}}]}
-{"version": 1,
- "uri": "file:///incrementalTactic.lean",
- "diagnostics":
- [{"source": "Lean 4",
-   "severity": 1,
-   "range":
-   {"start": {"line": 1, "character": 38}, "end": {"line": 4, "character": 3}},
-   "message": "unexpected token '/-!'; expected ')', '_', identifier or term",
-   "fullRange":
-   {"start": {"line": 1, "character": 38},
-    "end": {"line": 4, "character": 3}}}]}
-{"version": 1,
- "uri": "file:///incrementalTactic.lean",
- "diagnostics":
- [{"source": "Lean 4",
-   "severity": 1,
-   "range":
-   {"start": {"line": 2, "character": 9}, "end": {"line": 2, "character": 11}},
-   "message": "unknown identifier 'no'",
-   "fullRange":
-   {"start": {"line": 2, "character": 9}, "end": {"line": 2, "character": 11}}},
-  {"source": "Lean 4",
-   "severity": 1,
-   "range":
-   {"start": {"line": 3, "character": 9}, "end": {"line": 3, "character": 16}},
-   "message": "unsolved goals\n⊢ Nat",
-   "fullRange":
-   {"start": {"line": 3, "character": 9},
-    "end": {"line": 3, "character": 16}}}]}

tests/lean/interactive/run.lean

@@ -67,8 +67,7 @@ def ident : Parsec Name := do
 
 partial def main (args : List String) : IO Unit := do
   let uri := s!"file:///{args.head!}"
-  -- We want `dbg_trace` tactics to write directly to stderr instead of being caught in reuse
-  Ipc.runWith (←IO.appPath) #["--server", "-DstderrAsMessages=false"] do
+  Ipc.runWith (←IO.appPath) #["--server"] do
     let capabilities := {
       textDocument? := some {
         completion? := some {
@@ -83,157 +82,136 @@ partial def main (args : List String) : IO Unit := do
     Ipc.writeNotification ⟨"initialized", InitializedParams.mk⟩
 
     let text ← IO.FS.readFile args.head!
-    let mut requestNo : Nat := 1
-    for text in text.splitOn "-- RESET" do
-      Ipc.writeNotification ⟨"textDocument/didOpen", {
-        textDocument := { uri := uri, languageId := "lean", version := 1, text := text } : DidOpenTextDocumentParams }⟩
-      let initialDiags ← Ipc.collectDiagnostics requestNo uri 1
-      requestNo := requestNo + 1
-      let initialRequestNo := requestNo
-      let mut lineNo := 0
-      let mut lastActualLineNo := 0
-      let mut versionNo : Nat := 2
-      let mut rpcSessionId : Option UInt64 := none
-      for line in text.splitOn "\n" do
-        match line.splitOn "--" with
-        | [ws, directive] =>
-          let line ← match directive.front with
-            | 'v' => pure <| lineNo + 1  -- TODO: support subsequent 'v'... or not
-            | '^' => pure <| lastActualLineNo
-            | _ =>
-              lastActualLineNo := lineNo
-              lineNo := lineNo + 1
-              continue
-          let directive := directive.drop 1
-          let colon := directive.posOf ':'
-          let method := directive.extract 0 colon |>.trim
-          -- TODO: correctly compute in presence of Unicode
-          let column := ws.endPos + "--"
-          let pos : Lsp.Position := { line := line, character := column.byteIdx }
-          let params := if colon < directive.endPos then directive.extract (colon + ':') directive.endPos |>.trim else "{}"
-          match method with
-          -- `delete: "foo"` deletes the given string's number of characters at the given position.
-          -- We do NOT check currently that the text at this position is indeed that string.
-          | "delete"
-          -- `insert: "foo"` inserts the given string at the given position.
-          | "insert" =>
-            let some text := Syntax.decodeStrLit params
-              | throw <| IO.userError s!"failed to parse {params}"
-            let params : DidChangeTextDocumentParams := {
-              textDocument := {
-                uri      := uri
-                version? := versionNo
-              }
-              contentChanges := #[TextDocumentContentChangeEvent.rangeChange {
-                start := pos
-                «end» := match method with
-                  | "delete" => { pos with character := pos.character + text.length }
-                  | _ => pos
-              } (match method with
-                | "delete" => ""
-                | _ => text)]
-            }
-            let params := toJson params
-            Ipc.writeNotification ⟨"textDocument/didChange", params⟩
-            -- We don't want to wait for changes to be processed so we can test concurrency
-            --let _ ← Ipc.collectDiagnostics requestNo uri versionNo
-            requestNo := requestNo + 1
-            versionNo := versionNo + 1
-          | "collectDiagnostics" =>
-            if let some diags ←
-                if requestNo = initialRequestNo then pure initialDiags
-                else Ipc.collectDiagnostics requestNo uri (versionNo - 1) then
-              IO.eprintln (toJson diags.param)
-            requestNo := requestNo + 1
-          | "sync" =>  -- wait for processing but do not print diagnostics
-            let _ ← Ipc.collectDiagnostics requestNo uri (versionNo - 1)
-            requestNo := requestNo + 1
-          | "codeAction" =>
-            let params : CodeActionParams := {
-              textDocument := {uri := uri},
-              range := ⟨pos, pos⟩
-            }
-            Ipc.writeRequest ⟨requestNo, "textDocument/codeAction", params⟩
-            let r ← Ipc.readResponseAs requestNo (Array Json)
-            for x in r.result do
-              IO.eprintln x
-            requestNo := requestNo + 1
-          | "goals" =>
-            if rpcSessionId.isNone then
-              Ipc.writeRequest ⟨requestNo, "$/lean/rpc/connect",  RpcConnectParams.mk uri⟩
-              let r ← Ipc.readResponseAs requestNo RpcConnected
-              rpcSessionId := some r.result.sessionId
-              requestNo := requestNo + 1
-            let params : Lsp.PlainGoalParams := {
-              textDocument := { uri }
-              position := pos,
-            }
-            let ps : RpcCallParams := {
-              params := toJson params
-              textDocument := { uri }
-              position := pos,
-              sessionId := rpcSessionId.get!,
-              method := `Lean.Widget.getInteractiveGoals
-            }
-            Ipc.writeRequest ⟨requestNo, "$/lean/rpc/call", ps⟩
-            let response ← Ipc.readResponseAs requestNo Client.InteractiveGoals
-            requestNo := requestNo + 1
-            IO.eprintln (repr response.result)
-            IO.eprintln ""
-          | "widgets" =>
-            if rpcSessionId.isNone then
-              Ipc.writeRequest ⟨requestNo, "$/lean/rpc/connect",  RpcConnectParams.mk uri⟩
-              let r ← Ipc.readResponseAs requestNo RpcConnected
-              rpcSessionId := some r.result.sessionId
-              requestNo := requestNo + 1
-            let ps : RpcCallParams := {
-              textDocument := {uri := uri},
-              position := pos,
-              sessionId := rpcSessionId.get!,
-              method := `Lean.Widget.getWidgets,
-              params := toJson pos,
-            }
-            Ipc.writeRequest ⟨requestNo, "$/lean/rpc/call", ps⟩
-            let response ← Ipc.readResponseAs requestNo Lean.Widget.GetWidgetsResponse
-            requestNo := requestNo + 1
-            IO.eprintln response.result.debugJson
-            for w in response.result.widgets do
-              let params : Lean.Widget.GetWidgetSourceParams := { pos, hash := w.javascriptHash }
-              let ps : RpcCallParams := {
-                ps with
-                method := `Lean.Widget.getWidgetSource,
-                params := toJson params,
-              }
-              Ipc.writeRequest ⟨requestNo, "$/lean/rpc/call", ps⟩
-              let resp ← Ipc.readResponseAs requestNo Lean.Widget.WidgetSource
-              IO.eprintln (toJson resp.result)
-              requestNo := requestNo + 1
+    Ipc.writeNotification ⟨"textDocument/didOpen", {
+      textDocument := { uri := uri, languageId := "lean", version := 1, text := text } : DidOpenTextDocumentParams }⟩
+    let _ ← Ipc.collectDiagnostics 1 uri 1
+    let mut lineNo := 0
+    let mut lastActualLineNo := 0
+    let mut versionNo : Nat := 2
+    let mut requestNo : Nat := 2
+    let mut rpcSessionId : Option UInt64 := none
+    for line in text.splitOn "\n" do
+      match line.splitOn "--" with
+      | [ws, directive] =>
+        let line ← match directive.front with
+          | 'v' => pure <| lineNo + 1  -- TODO: support subsequent 'v'... or not
+          | '^' => pure <| lastActualLineNo
           | _ =>
-            let Except.ok params ← pure <| Json.parse params
-              | throw <| IO.userError s!"failed to parse {params}"
-            let params := params.setObjVal! "textDocument" (toJson { uri := uri : TextDocumentIdentifier })
-            -- TODO: correctly compute in presence of Unicode
-            let params := params.setObjVal! "position" (toJson pos)
-            IO.eprintln params
-            Ipc.writeRequest ⟨requestNo, method, params⟩
-            let rec readFirstResponse := do
-              match ← Ipc.readMessage with
-              | Message.response id r =>
-                assert! id == requestNo
-                return r
-              | Message.notification .. => readFirstResponse
-              | Message.request .. => readFirstResponse
-              | msg => throw <| IO.userError s!"unexpected message {toJson msg}"
-            let resp ← readFirstResponse
-            IO.eprintln resp
+            lastActualLineNo := lineNo
+            lineNo := lineNo + 1
+            continue
+        let directive := directive.drop 1
+        let colon := directive.posOf ':'
+        let method := directive.extract 0 colon |>.trim
+        -- TODO: correctly compute in presence of Unicode
+        let column := ws.endPos + "--"
+        let pos : Lsp.Position := { line := line, character := column.byteIdx }
+        let params := if colon < directive.endPos then directive.extract (colon + ':') directive.endPos |>.trim else "{}"
+        match method with
+        | "insert" =>
+          let params : DidChangeTextDocumentParams := {
+            textDocument := {
+              uri      := uri
+              version? := versionNo
+            }
+            contentChanges := #[TextDocumentContentChangeEvent.rangeChange {
+              start := pos
+              «end» := { pos with character := pos.character + params.endPos.byteIdx }
+            } params]
+          }
+          let params := toJson params
+          IO.eprintln params
+          Ipc.writeNotification ⟨"textDocument/didChange", params⟩
+          -- We don't want to wait for changes to be processed so we can test concurrency
+          --let _ ← Ipc.collectDiagnostics requestNo uri versionNo
+          requestNo := requestNo + 1
+          versionNo := versionNo + 1
+        | "collectDiagnostics" =>
+          if let some diags ← Ipc.collectDiagnostics requestNo uri (versionNo - 1) then
+            IO.eprintln (toJson diags.param)
+          requestNo := requestNo + 1
+        | "codeAction" =>
+          let params : CodeActionParams := {
+            textDocument := {uri := uri},
+            range := ⟨pos, pos⟩
+          }
+          Ipc.writeRequest ⟨requestNo, "textDocument/codeAction", params⟩
+          let r ← Ipc.readResponseAs requestNo (Array Json)
+          for x in r.result do
+            IO.eprintln x
+          requestNo := requestNo + 1
+        | "goals" =>
+          if rpcSessionId.isNone then
+            Ipc.writeRequest ⟨requestNo, "$/lean/rpc/connect",  RpcConnectParams.mk uri⟩
+            let r ← Ipc.readResponseAs requestNo RpcConnected
+            rpcSessionId := some r.result.sessionId
+            requestNo := requestNo + 1
+          let params : Lsp.PlainGoalParams := {
+            textDocument := { uri }
+            position := pos,
+          }
+          let ps : RpcCallParams := {
+            params := toJson params
+            textDocument := { uri }
+            position := pos,
+            sessionId := rpcSessionId.get!,
+            method := `Lean.Widget.getInteractiveGoals
+          }
+          Ipc.writeRequest ⟨requestNo, "$/lean/rpc/call", ps⟩
+          let response ← Ipc.readResponseAs requestNo Client.InteractiveGoals
+          requestNo := requestNo + 1
+          IO.eprintln (repr response.result)
+          IO.eprintln ""
+        | "widgets" =>
+          if rpcSessionId.isNone then
+            Ipc.writeRequest ⟨requestNo, "$/lean/rpc/connect",  RpcConnectParams.mk uri⟩
+            let r ← Ipc.readResponseAs requestNo RpcConnected
+            rpcSessionId := some r.result.sessionId
+            requestNo := requestNo + 1
+          let ps : RpcCallParams := {
+            textDocument := {uri := uri},
+            position := pos,
+            sessionId := rpcSessionId.get!,
+            method := `Lean.Widget.getWidgets,
+            params := toJson pos,
+          }
+          Ipc.writeRequest ⟨requestNo, "$/lean/rpc/call", ps⟩
+          let response ← Ipc.readResponseAs requestNo Lean.Widget.GetWidgetsResponse
+          requestNo := requestNo + 1
+          IO.eprintln response.result.debugJson
+          for w in response.result.widgets do
+            let params : Lean.Widget.GetWidgetSourceParams := { pos, hash := w.javascriptHash }
+            let ps : RpcCallParams := {
+              ps with
+              method := `Lean.Widget.getWidgetSource,
+              params := toJson params,
+            }
+            Ipc.writeRequest ⟨requestNo, "$/lean/rpc/call", ps⟩
+            let resp ← Ipc.readResponseAs requestNo Lean.Widget.WidgetSource
+            IO.eprintln (toJson resp.result)
             requestNo := requestNo + 1
         | _ =>
-          lastActualLineNo := lineNo
-        lineNo := lineNo + 1
-
-      let _ ← Ipc.collectDiagnostics requestNo uri (versionNo - 1)
-      Ipc.writeNotification ⟨"textDocument/didClose", {
-        textDocument := { uri } : DidCloseTextDocumentParams }⟩
+          let Except.ok params ← pure <| Json.parse params
+            | throw <| IO.userError s!"failed to parse {params}"
+          let params := params.setObjVal! "textDocument" (toJson { uri := uri : TextDocumentIdentifier })
+          -- TODO: correctly compute in presence of Unicode
+          let params := params.setObjVal! "position" (toJson pos)
+          IO.eprintln params
+          Ipc.writeRequest ⟨requestNo, method, params⟩
+          let rec readFirstResponse := do
+            match ← Ipc.readMessage with
+            | Message.response id r =>
+              assert! id == requestNo
+              return r
+            | Message.notification .. => readFirstResponse
+            | Message.request .. => readFirstResponse
+            | msg => throw <| IO.userError s!"unexpected message {toJson msg}"
+          let resp ← readFirstResponse
+          IO.eprintln resp
+          requestNo := requestNo + 1
+      | _ =>
+        lastActualLineNo := lineNo
+      lineNo := lineNo + 1
 
     Ipc.shutdown requestNo
     discard <| Ipc.waitForExit

tests/lean/interactive/unterminatedDocComment.lean

@@ -4,6 +4,6 @@ def a2 := sorry
 def a3 := sorry
 ...
  -
---^ insert: "/"
+--^ insert: /
 --^ collectDiagnostics
 def a4 := 0

tests/lean/interactive/unterminatedDocComment.lean.expected.out

@@ -1 +1,6 @@
+{"textDocument": {"version": 2, "uri": "file:///unterminatedDocComment.lean"},
+ "contentChanges":
+ [{"text": "/",
+   "range":
+   {"start": {"line": 5, "character": 2}, "end": {"line": 5, "character": 3}}}]}
 {"version": 2, "uri": "file:///unterminatedDocComment.lean", "diagnostics": []}

tests/lean/run/anonymous_ctor_error_msg.lean

@@ -25,12 +25,12 @@ Foo.sum [x1, x2, x3, x5, x6]
 
 /--
 error: invalid constructor ⟨...⟩, expected type must be an inductive type ⏎
-  ?m.441
+  ?m.442
 ---
 info: let x1 := { n := 1 };
 let x2 := { n := 2 };
 let x3 := { n := 3 };
-let x4 := ?m.445 x1 x2 x3;
+let x4 := ?m.446 x1 x2 x3;
 let x5 := { n := 5 };
 let x6 := { n := 6 };
 Foo.sum [x1, x2, x3, x5, x6] : Foo

tests/lean/run/meta3.lean

@@ -64,7 +64,7 @@ info: [Meta.debug] (Add.add => (node
     (* => (node #[5]))
     (Nat.add => (node (0 => (node (20 => (node #[3]))))))
 [Meta.debug] #[5, 1]
-[Meta.debug] Add.add ?m.4906 ?m.4906
+[Meta.debug] Add.add ?m.4904 ?m.4904
 [Meta.debug] #[5]
 [Meta.debug] #[5, 1, 4, 2]
 [Meta.debug] #[1, 4, 2, 5, 3]

tests/lean/run/variable_slowdown.lean

@@ -1,153 +0,0 @@
-/-!
-Minimization of a problem noticed in Mathlib's slowest file `Mathlib.RingTheory.Kaehler`
-(although this is probably not the cause of the major slowdown, it is still a problem).
-
-Adding an irrelevant `variable` statement can dramatically slow down every elaboration problem.
-
-In this example we have:
-```
-...
-
-example : Nat := 0
-
-variable [Algebra R S]
-
-example : Nat := 0 -- now takes more than 9x as many heartbeats!
-```
--/
-
-universe u
-
-section Mathlib.Init.Order.Defs
-
-class LinearOrder (α : Type u) where
-
-end Mathlib.Init.Order.Defs
-
-section Mathlib.Algebra.Group.Defs
-
-class SMul (M : Type u) (α : Type u) where
-
-class Semigroup (G : Type u) extends Mul G where
-
-class AddSemigroup (G : Type u) extends Add G where
-
-class AddMonoid (M : Type u) extends AddSemigroup M where
-
-class Monoid (M : Type u) extends Semigroup M where
-
-class AddCommMonoid (M : Type u) extends AddMonoid M
-
-class CommMonoid (M : Type u) extends Monoid M
-
-class AddCommGroup (G : Type u)
-
-end Mathlib.Algebra.Group.Defs
-
-section Mathlib.Algebra.GroupWithZero.Defs
-
-class SemigroupWithZero (S₀ : Type u) extends Semigroup S₀
-
-end Mathlib.Algebra.GroupWithZero.Defs
-
-section Mathlib.Algebra.Ring.Defs
-
-variable {α : Type u}
-
-class Distrib (R : Type u) extends Mul R where
-
-class NonUnitalNonAssocSemiring (α : Type u) extends AddCommMonoid α, Distrib α
-
-class NonUnitalSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, SemigroupWithZero α
-
-class NonAssocSemiring (α : Type u) extends NonUnitalNonAssocSemiring α
-
-class NonUnitalNonAssocRing (α : Type u) extends AddCommGroup α
-
-class NonUnitalRing (α : Type u) extends NonUnitalNonAssocRing α, NonUnitalSemiring α
-
-class Semiring (α : Type u) extends NonUnitalSemiring α
-
-class Ring (R : Type u) extends Semiring R, AddCommGroup R
-
-class NonUnitalNonAssocCommSemiring (α : Type u) extends NonUnitalNonAssocSemiring α
-
-class NonUnitalCommSemiring (α : Type u) extends NonUnitalSemiring α
-
-class CommSemiring (R : Type u) extends Semiring R, CommMonoid R
-
-instance (priority := 100) CommSemiring.toNonUnitalCommSemiring [CommSemiring α] :
-    NonUnitalCommSemiring α :=
-  { inferInstanceAs (CommMonoid α), inferInstanceAs (CommSemiring α) with }
-
-instance (priority := 200) [Ring α] : Semiring α :=
-  { ‹Ring α› with }
-
-class NonUnitalNonAssocCommRing (α : Type u)
-  extends NonUnitalNonAssocCommSemiring α
-
-class NonUnitalCommRing (α : Type u) extends NonUnitalRing α, NonUnitalNonAssocCommRing α
-
-instance (priority := 100) NonUnitalCommRing.toNonUnitalCommSemiring [s : NonUnitalCommRing α] :
-    NonUnitalCommSemiring α :=
-  { s with }
-
-class CommRing (α : Type u) extends Ring α, CommMonoid α
-
-instance (priority := 100) CommRing.toCommSemiring [s : CommRing α] : CommSemiring α :=
-  { s with }
-
-instance (priority := 100) CommRing.toNonUnitalCommRing [s : CommRing α] : NonUnitalCommRing α :=
-  { s with }
-
-end Mathlib.Algebra.Ring.Defs
-
-section Mathlib.Algebra.Order.Ring.Defs
-
-class OrderedSemiring (α : Type u) extends Semiring α where
-  protected zero_le_one : True
-
-class OrderedCommSemiring (α : Type u) extends OrderedSemiring α, CommSemiring α where
-
-class OrderedRing (α : Type u) extends Ring α where
-
-class OrderedCommRing (α : Type u) extends OrderedRing α, CommRing α
-
-class StrictOrderedSemiring (α : Type u) extends Semiring α where
-
-class StrictOrderedCommSemiring (α : Type u) extends StrictOrderedSemiring α, CommSemiring α
-
-class StrictOrderedRing (α : Type u) extends Ring α where
-
-class LinearOrderedSemiring (α : Type u) extends StrictOrderedSemiring α
-
-class LinearOrderedCommSemiring (α : Type u) extends StrictOrderedCommSemiring α,
-  LinearOrderedSemiring α
-
-class LinearOrderedRing (α : Type u) extends StrictOrderedRing α, LinearOrder α
-
-class LinearOrderedCommRing (α : Type u) extends LinearOrderedRing α
-
-end Mathlib.Algebra.Order.Ring.Defs
-
-section Mathlib.Algebra.Algebra.Defs
-
-class Algebra (R : Type) (A : Type) [Semigroup R] [Semigroup A] extends SMul R A where
-
-end Mathlib.Algebra.Algebra.Defs
-
-variable (R S : Type) [NonUnitalRing R] [NonUnitalRing S]
-
-set_option maxHeartbeats 10 in
-example : Nat := 0
-
-variable [Algebra R S] -- Add this irrelevant variable, and we take about 15x more heartbeats.
-
-/--
-error: (deterministic) timeout at `isDefEq`, maximum number of heartbeats (90) has been reached
-use `set_option maxHeartbeats <num>` to set the limit
-use `set_option diagnostics true` to get diagnostic information
--/
-#guard_msgs in
-set_option maxHeartbeats 90 in
-example : Nat := 0

tests/lean/server/test_single.sh

@@ -1,4 +1,4 @@
 #!/usr/bin/env bash
 source ../../common.sh
 
-exec_check lean -Dlinter.all=false --run "$f"
+exec_check lean -j 0 -Dlinter.all=false --run "$f"

tests/pkg/frontend/Frontend/Compile.lean

@@ -10,7 +10,7 @@ unsafe def processInput (input : String) (initializers := false)  :
   let (header, parserState, messages) ← Parser.parseHeader inputCtx
   let (env, messages) ← processHeader header {} messages inputCtx
   let s ← IO.processCommands inputCtx parserState (Command.mkState env messages {}) <&> Frontend.State.commandState
-  pure (s.env, s.messages.toList)
+  pure (s.env, s.messages.msgs.toList)
 
 open System in
 def findLean (mod : Name) : IO FilePath := do