diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index 4da1807f2e..ba8b732585 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -177,6 +177,13 @@ instance : MonadTrace CoreM where
 def restore (b : State) : CoreM Unit :=
   modify fun s => { s with env := b.env, messages := b.messages, infoState := b.infoState }
 
+/--
+Restores full state including sources for unique identifiers. Only intended for incremental reuse
+between elaboration runs, not for backtracking within a single run.
+-/
+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 })
   return addMacroScope (← getEnv).mainModule n fresh
@@ -245,6 +252,13 @@ def resetMessageLog : CoreM Unit :=
 def getMessageLog : CoreM MessageLog :=
   return (← get).messages
 
+/--
+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 log => ({ log with msgs := {} }, log)
+
 instance : MonadLog CoreM where
   getRef      := getRef
   getFileMap  := return (← read).fileMap
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index b084ff0293..8bd32db7d6 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -7,6 +7,7 @@ prelude
 import Lean.Elab.Binders
 import Lean.Elab.SyntheticMVars
 import Lean.Elab.SetOption
+import Lean.Language.Basic
 
 namespace Lean.Elab.Command
 
@@ -44,6 +45,16 @@ structure Context where
   currMacroScope : MacroScope := firstFrontendMacroScope
   ref            : Syntax := Syntax.missing
   tacticCache?   : Option (IO.Ref Tactic.Cache)
+  /--
+  Snapshot for incremental reuse and reporting of command elaboration. Currently unused in Lean
+  itself.
+
+  Definitely resolved in `Language.Lean.process.doElab`.
+
+  Invariant: if the bundle's `old?` is set, the context and state at the beginning of current and
+  old elaboration are identical.
+  -/
+  snap?          : Option (Language.SnapshotBundle Language.DynamicSnapshot)
 
 abbrev CommandElabCoreM (ε) := ReaderT Context $ StateRefT State $ EIO ε
 abbrev CommandElabM := CommandElabCoreM Exception
@@ -520,6 +531,7 @@ def liftCommandElabM (cmd : CommandElabM α) : CoreM α := do
       fileMap := ← getFileMap
       ref := ← getRef
       tacticCache? := none
+      snap? := none
     } |>.run {
       env := ← getEnv
       maxRecDepth := ← getMaxRecDepth
diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean
index f1b0c89d18..1149a3a270 100644
--- a/src/Lean/Elab/Frontend.lean
+++ b/src/Lean/Elab/Frontend.lean
@@ -33,6 +33,7 @@ def setCommandState (commandState : Command.State) : FrontendM Unit :=
     fileName     := ctx.inputCtx.fileName
     fileMap      := ctx.inputCtx.fileMap
     tacticCache? := none
+    snap?        := 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}"
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 1321c50d5d..ce929262f8 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -261,6 +261,14 @@ def SavedState.restore (s : SavedState) (restoreInfo : Bool := false) : TermElab
   unless restoreInfo do
     setInfoState infoState
 
+/--
+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
@@ -1758,6 +1766,7 @@ builtin_initialize
   registerTraceClass `Elab.postpone
   registerTraceClass `Elab.coe
   registerTraceClass `Elab.debug
+  registerTraceClass `Elab.reuse
 
 export Term (TermElabM)
 
diff --git a/src/Lean/Language/Basic.lean b/src/Lean/Language/Basic.lean
index e09fad8523..5106161798 100644
--- a/src/Lean/Language/Basic.lean
+++ b/src/Lean/Language/Basic.lean
@@ -9,6 +9,7 @@ Authors: Sebastian Ullrich
 -/
 
 prelude
+import Init.System.Promise
 import Lean.Message
 import Lean.Parser.Types
 
@@ -58,23 +59,26 @@ deriving Inhabited
 -- cursor position. This may require starting the tasks suspended (e.g. in `Thunk`). The server may
 -- also need more dependency information for this in order to avoid priority inversion.
 structure SnapshotTask (α : Type) where
-  /-- Range that is marked as being processed by the server while the task is running. -/
-  range : String.Range
+  /--
+  Range that is marked as being processed by the server while the task is running. If `none`,
+  the range of the outer task if some or else the entire file is reported.
+  -/
+  range? : Option String.Range
   /-- Underlying task producing the snapshot. -/
   task : Task α
 deriving Nonempty
 
 /-- Creates a snapshot task from a reporting range and a `BaseIO` action. -/
-def SnapshotTask.ofIO (range : String.Range) (act : BaseIO α) : BaseIO (SnapshotTask α) := do
+def SnapshotTask.ofIO (range? : Option String.Range) (act : BaseIO α) : BaseIO (SnapshotTask α) := do
   return {
-    range
+    range?
     task := (← BaseIO.asTask act)
   }
 
 /-- Creates a finished snapshot task. -/
 def SnapshotTask.pure (a : α) : SnapshotTask α where
   -- irrelevant when already finished
-  range := default
+  range? := none
   task := .pure a
 
 /--
@@ -84,23 +88,26 @@ def SnapshotTask.cancel (t : SnapshotTask α) : BaseIO Unit :=
   IO.cancel t.task
 
 /-- Transforms a task's output without changing the reporting range. -/
-def SnapshotTask.map (t : SnapshotTask α) (f : α → β) (range : String.Range := t.range)
+def SnapshotTask.map (t : SnapshotTask α) (f : α → β) (range? : Option String.Range := t.range?)
     (sync := false) : SnapshotTask β :=
-  { range, task := t.task.map (sync := sync) f }
+  { range?, task := t.task.map (sync := sync) f }
 
 /--
   Chains two snapshot tasks. The range is taken from the first task if not specified; the range of
   the second task is discarded. -/
 def SnapshotTask.bind (t : SnapshotTask α) (act : α → SnapshotTask β)
-    (range : String.Range := t.range) (sync := false) : SnapshotTask β :=
-  { range, task := t.task.bind (sync := sync) (act · |>.task) }
+    (range? : Option String.Range := t.range?) (sync := false) : SnapshotTask β :=
+  { range?, task := t.task.bind (sync := sync) (act · |>.task) }
 
 /--
   Chains two snapshot tasks. The range is taken from the first task if not specified; the range of
   the second task is discarded. -/
 def SnapshotTask.bindIO (t : SnapshotTask α) (act : α → BaseIO (SnapshotTask β))
-    (range : String.Range := t.range) (sync := false) : BaseIO (SnapshotTask β) :=
-  return { range, task := (← BaseIO.bindTask (sync := sync) t.task fun a => (·.task) <$> (act a)) }
+    (range? : Option String.Range := t.range?) (sync := false) : BaseIO (SnapshotTask β) :=
+  return {
+    range?
+    task := (← BaseIO.bindTask (sync := sync) t.task fun a => (·.task) <$> (act a))
+  }
 
 /-- Synchronously waits on the result of the task. -/
 def SnapshotTask.get (t : SnapshotTask α) : α :=
@@ -110,6 +117,40 @@ def SnapshotTask.get (t : SnapshotTask α) : α :=
 def SnapshotTask.get? (t : SnapshotTask α) : BaseIO (Option α) :=
   return if (← IO.hasFinished t.task) then some t.task.get else none
 
+/--
+Arbitrary value paired with a syntax that should be inspected when considering the value for reuse.
+-/
+structure SyntaxGuarded (α : Type) where
+  /-- Syntax to be inspected for reuse. -/
+  stx : Syntax
+  /-- Potentially reusable value. -/
+  val : α
+
+/--
+Pair of (optional) old snapshot task usable for incremental reuse and new snapshot promise for
+incremental reporting. Inside the elaborator, we build snapshots by carrying such bundles and then
+checking if we can reuse `old?` if set or else redoing the corresponding elaboration step. In either
+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!
+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.
+-/
+structure SnapshotBundle (α : Type) where
+  /--
+  Snapshot task of corresponding elaboration in previous document version if any, paired with its
+  old syntax to be considered for reuse. Should be set to `none` as soon as reuse can be ruled out.
+  -/
+  old? : Option (SyntaxGuarded (SnapshotTask α))
+  /--
+  Promise of snapshot value for the current document. When resolved, the language server will
+  report its result even before the current elaborator invocation has finished.
+  -/
+  new  : IO.Promise α
+
 /--
   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.
@@ -118,7 +159,7 @@ def SnapshotTask.get? (t : SnapshotTask α) : BaseIO (Option α) :=
 inductive SnapshotTree where
   /-- Creates a snapshot tree node. -/
   | mk (element : Snapshot) (children : Array (SnapshotTask SnapshotTree))
-deriving Nonempty
+deriving Inhabited
 
 /-- The immediately available element of the snapshot tree node. -/
 abbrev SnapshotTree.element : SnapshotTree → Snapshot
@@ -135,6 +176,39 @@ class ToSnapshotTree (α : Type) where
   toSnapshotTree : α → SnapshotTree
 export ToSnapshotTree (toSnapshotTree)
 
+instance [ToSnapshotTree α] : ToSnapshotTree (Option α) where
+  toSnapshotTree
+    | some a => toSnapshotTree a
+    | none   => default
+
+/-- Snapshot type without child nodes. -/
+structure SnapshotLeaf extends Snapshot
+deriving Nonempty, TypeName
+
+instance : ToSnapshotTree SnapshotLeaf where
+  toSnapshotTree s := SnapshotTree.mk s.toSnapshot #[]
+
+/-- Arbitrary snapshot type, used for extensibility. -/
+structure DynamicSnapshot where
+  /-- Concrete snapshot value as `Dynamic`. -/
+  val  : Dynamic
+  /-- Snapshot tree retrieved from `val` before erasure. -/
+  tree : SnapshotTree
+deriving Nonempty
+
+instance : ToSnapshotTree DynamicSnapshot where
+  toSnapshotTree s := s.tree
+
+/-- Creates a `DynamicSnapshot` from a typed snapshot value. -/
+def DynamicSnapshot.ofTyped [TypeName α] [ToSnapshotTree α] (val : α) : DynamicSnapshot where
+  val := .mk val
+  tree := ToSnapshotTree.toSnapshotTree val
+
+/-- Returns the original snapshot value if it is of the given type. -/
+def DynamicSnapshot.toTyped? (α : Type) [TypeName α] (snap : DynamicSnapshot) :
+    Option α :=
+  snap.val.get? α
+
 /--
   Option for printing end position of each message in addition to start position. Used for testing
   message ranges in the test suite. -/
@@ -187,7 +261,7 @@ Creates snapshot message log from non-interactive message log, also allocating a
 that can be used by the server to memorize interactive diagnostics derived from the log.
 -/
 def Snapshot.Diagnostics.ofMessageLog (msgLog : Lean.MessageLog) :
-    ProcessingM Snapshot.Diagnostics := do
+    BaseIO Snapshot.Diagnostics := do
   return { msgLog, interactiveDiagsRef? := some (← IO.mkRef none) }
 
 /-- Creates diagnostics from a single error message that should span the whole file. -/
diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean
index c967565bf3..ca48730c7d 100644
--- a/src/Lean/Language/Lean.lean
+++ b/src/Lean/Language/Lean.lean
@@ -58,6 +58,51 @@ exist currently and likely it could at best be approximated by e.g. "furthest `t
 we remain at "go two commands up" at this point.
 -/
 
+/-!
+# Note [Incremental Command Elaboration]
+
+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 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 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. `)
+* 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 `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.
+
+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
+multiple times because otherwise the progress bar would snap back and forth multiple times. For this
+purpose, we can disable both incremental modes using `Term.withoutTacticIncrementality`, assuming we
+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.
+-/
+
 set_option linter.missingDocs true
 
 namespace Lean.Language.Lean
@@ -84,34 +129,29 @@ register_builtin_option showPartialSyntaxErrors : Bool := {
 
 /-! The hierarchy of Lean snapshot types -/
 
-/-- Final state of processing of a command. -/
-structure CommandFinishedSnapshot extends Snapshot where
+/-- Snapshot after elaboration of the entire command. -/
+structure CommandFinishedSnapshot extends Language.Snapshot where
   /-- Resulting elaboration state. -/
   cmdState : Command.State
 deriving Nonempty
 instance : ToSnapshotTree CommandFinishedSnapshot where
   toSnapshotTree s := ⟨s.toSnapshot, #[]⟩
 
-/--
-  State after processing a command's signature and before executing its tactic body, if any. Other
-  commands should immediately proceed to `finished`. -/
--- TODO: tactics
-structure CommandSignatureProcessedSnapshot extends Snapshot where
-  /-- State after processing is finished. -/
-  finishedSnap : SnapshotTask CommandFinishedSnapshot
-deriving Nonempty
-instance : ToSnapshotTree CommandSignatureProcessedSnapshot where
-  toSnapshotTree s := ⟨s.toSnapshot, #[s.finishedSnap.map (sync := true) toSnapshotTree]⟩
-
 /-- State after a command has been parsed. -/
 structure CommandParsedSnapshotData extends Snapshot where
   /-- Syntax tree of the command. -/
   stx : Syntax
   /-- Resulting parser state. -/
   parserState : Parser.ModuleParserState
-  /-- Signature processing task. -/
-  sigSnap : SnapshotTask CommandSignatureProcessedSnapshot
+  /--
+  Snapshot for incremental reporting and reuse during elaboration, type dependent on specific
+  elaborator.
+   -/
+  elabSnap : SnapshotTask DynamicSnapshot
+  /-- State after processing is finished. -/
+  finishedSnap : SnapshotTask CommandFinishedSnapshot
 deriving Nonempty
+
 /-- State after a command has been parsed. -/
 -- workaround for lack of recursive structures
 inductive CommandParsedSnapshot where
@@ -123,22 +163,23 @@ deriving Nonempty
 abbrev CommandParsedSnapshot.data : CommandParsedSnapshot → CommandParsedSnapshotData
   | mk data _ => data
 /-- Next command, unless this is a terminal command. -/
--- It would be really nice to not make this depend on `sig.finished` where possible
 abbrev CommandParsedSnapshot.next? : CommandParsedSnapshot →
     Option (SnapshotTask CommandParsedSnapshot)
   | mk _ next? => next?
 partial instance : ToSnapshotTree CommandParsedSnapshot where
   toSnapshotTree := go where
     go s := ⟨s.data.toSnapshot,
-      #[s.data.sigSnap.map (sync := true) toSnapshotTree] |>
+      #[s.data.elabSnap.map (sync := true) toSnapshotTree,
+        s.data.finishedSnap.map (sync := true) toSnapshotTree] |>
         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
-  -- TODO: cancel additional elaboration tasks if we add them without switching to implicit
-  -- cancellation
-  snap.data.sigSnap.cancel
+  -- 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
@@ -308,7 +349,7 @@ where
   processHeader (stx : Syntax) (parserState : Parser.ModuleParserState) :
       LeanProcessingM (SnapshotTask HeaderProcessedSnapshot) := do
     let ctx ← read
-    SnapshotTask.ofIO ⟨0, ctx.input.endPos⟩ <|
+    SnapshotTask.ofIO (some ⟨0, ctx.input.endPos⟩) <|
     ReaderT.run (r := ctx) <|  -- re-enter reader in new task
     withHeaderExceptions (α := HeaderProcessedSnapshot) ({ · with result? := none }) do
       let opts ← match (← setupImports stx) with
@@ -362,16 +403,15 @@ where
       -- is not `Inhabited`
       return .pure <| .mk (nextCmdSnap? := none) {
         diagnostics := .empty, stx := .missing, parserState
-        sigSnap := .pure {
-          diagnostics := .empty
-          finishedSnap := .pure { diagnostics := .empty, cmdState } } }
+        elabSnap := .pure <| .ofTyped { diagnostics := .empty : SnapshotLeaf }
+        finishedSnap := .pure { diagnostics := .empty, cmdState }
+      }
 
     let unchanged old : BaseIO CommandParsedSnapshot :=
       -- when syntax is unchanged, reuse command processing task as is
       if let some oldNext := old.next? then
         return .mk (data := old.data)
-          (nextCmdSnap? := (← old.data.sigSnap.bindIO (sync := true) fun oldSig =>
-            oldSig.finishedSnap.bindIO (sync := true) fun oldFinished =>
+          (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
@@ -384,7 +424,7 @@ where
         if (← isBeforeEditPos nextCom.data.parserState.pos) then
           return .pure (← unchanged old)
 
-    SnapshotTask.ofIO ⟨parserState.pos, ctx.input.endPos⟩ do
+    SnapshotTask.ofIO (some ⟨parserState.pos, ctx.input.endPos⟩) do
       let beginPos := parserState.pos
       let scope := cmdState.scopes.head!
       let pmctx := {
@@ -401,21 +441,27 @@ where
         -- on first change, make sure to cancel all further old tasks
         old.cancel
 
-      let sigSnap ← processCmdSignature stx cmdState msgLog.hasErrors beginPos ctx
+      -- definitely resolved in `doElab` task
+      let elabPromise ← IO.Promise.new
+      let finishedSnap ←
+        doElab stx cmdState msgLog.hasErrors beginPos
+          { old? := old?.map fun old => ⟨old.data.stx, old.data.elabSnap⟩, new := elabPromise } ctx
+
       let next? ← if Parser.isTerminalCommand stx then pure none
         -- for now, wait on "command finished" snapshot before parsing next command
-        else some <$> (sigSnap.bind (·.finishedSnap)).bindIO fun finished =>
+        else some <$> finishedSnap.bindIO fun finished =>
           parseCmd none parserState finished.cmdState ctx
       return .mk (nextCmdSnap? := next?) {
-        diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog ctx.toProcessingContext)
+        diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog)
         stx
         parserState
-        sigSnap
+        elabSnap := { range? := finishedSnap.range?, task := elabPromise.result }
+        finishedSnap
       }
 
-  processCmdSignature (stx : Syntax) (cmdState : Command.State) (hasParseError : Bool)
-      (beginPos : String.Pos) :
-      LeanProcessingM (SnapshotTask CommandSignatureProcessedSnapshot) := do
+  doElab (stx : Syntax) (cmdState : Command.State) (hasParseError : Bool) (beginPos : String.Pos)
+      (snap : SnapshotBundle DynamicSnapshot) :
+      LeanProcessingM (SnapshotTask CommandFinishedSnapshot) := do
     let ctx ← read
 
     -- signature elaboration task; for now, does full elaboration
@@ -423,7 +469,11 @@ where
     SnapshotTask.ofIO (stx.getRange?.getD ⟨beginPos, beginPos⟩) do
       let scope := cmdState.scopes.head!
       let cmdStateRef ← IO.mkRef { cmdState with messages := .empty }
-      let cmdCtx : Elab.Command.Context := { ctx with cmdPos := beginPos, tacticCache? := none }
+      let cmdCtx : Elab.Command.Context := { ctx with
+        cmdPos       := beginPos
+        tacticCache? := none
+        snap?        := some snap
+      }
       let (output, _) ←
         IO.FS.withIsolatedStreams (isolateStderr := stderrAsMessages.get scope.opts) do
           liftM (m := BaseIO) do
@@ -449,14 +499,12 @@ where
           data     := output
         }
       let cmdState := { cmdState with messages }
+      -- definitely resolve eventually
+      snap.new.resolve <| .ofTyped { diagnostics := .empty : SnapshotLeaf }
       return {
-        diagnostics := .empty
-        finishedSnap := .pure {
-          diagnostics :=
-            (← Snapshot.Diagnostics.ofMessageLog cmdState.messages ctx.toProcessingContext)
-          infoTree? := some cmdState.infoState.trees[0]!
-          cmdState
-        }
+        diagnostics := (← Snapshot.Diagnostics.ofMessageLog cmdState.messages)
+        infoTree? := some cmdState.infoState.trees[0]!
+        cmdState
       }
 
 /-- Waits for and returns final environment, if importing was successful. -/
@@ -468,6 +516,6 @@ where goCmd snap :=
   if let some next := snap.next? then
     goCmd next.get
   else
-    snap.data.sigSnap.get.finishedSnap.get.cmdState.env
+    snap.data.finishedSnap.get.cmdState.env
 
 end Lean
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 37e2ae7647..0882164276 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -371,6 +371,14 @@ def SavedState.restore (b : SavedState) : MetaM Unit := do
   Core.restore b.core
   modify fun s => { s with mctx := b.meta.mctx, zetaDeltaFVarIds := b.meta.zetaDeltaFVarIds, postponed := b.meta.postponed }
 
+/--
+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
   restoreState s := s.restore
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 304cb92c7f..ca8e133013 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -223,7 +223,8 @@ This option can only be set on the command line, not in the lakefile or via `set
       | t::ts => do
         let mut st := st
         unless (← IO.hasFinished t.task) do
-          ctx.chanOut.send <| mkFileProgressAtPosNotification doc.meta t.range.start
+          if let some range := t.range? then
+            ctx.chanOut.send <| mkFileProgressAtPosNotification doc.meta range.start
           if !st.hasBlocked then
             publishDiagnostics ctx doc
             st := { st with hasBlocked := true }
diff --git a/src/Lean/Server/FileWorker/Utils.lean b/src/Lean/Server/FileWorker/Utils.lean
index 13c89720dd..b14f08819a 100644
--- a/src/Lean/Server/FileWorker/Utils.lean
+++ b/src/Lean/Server/FileWorker/Utils.lean
@@ -42,9 +42,9 @@ private partial def mkCmdSnaps (initSnap : Language.Lean.InitialSnapshot) :
       mpState := headerParsed.parserState
       cmdState := headerSuccess.cmdState
     } <| .delayed <| headerSuccess.firstCmdSnap.task.bind go
-where go cmdParsed :=
-  cmdParsed.data.sigSnap.task.bind fun sig =>
-    sig.finishedSnap.task.map fun finished =>
+where
+  go cmdParsed :=
+    cmdParsed.data.finishedSnap.task.map fun finished =>
       .ok <| .cons {
         stx := cmdParsed.data.stx
         mpState := cmdParsed.data.parserState
diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean
index cb1f5ea7c7..5d3070f752 100644
--- a/src/Lean/Server/Snapshots.lean
+++ b/src/Lean/Server/Snapshots.lean
@@ -58,6 +58,7 @@ def runCommandElabM (snap : Snapshot) (meta : DocumentMeta) (c : CommandElabM α
     fileName := meta.uri,
     fileMap := meta.text,
     tacticCache? := none
+    snap? := none
   }
   c.run ctx |>.run' snap.cmdState