rebased merge

src/Lean/CoreM.lean

@@ -179,7 +179,7 @@ def restore (b : State) : CoreM Unit :=
 
 /--
 Restores full state including sources for unique identifiers. Only intended for incremental reuse
-betweeen elaboration runs, not for backtracking within a single run.
+between elaboration runs, not for backtracking within a single run.
 -/
 def restoreFull (b : State) : CoreM Unit :=
   set b

src/Lean/Elab/MutualDef.lean

@@ -941,7 +941,7 @@ where
     for header in headers, view in views do
       if let some classNamesStx := view.deriving? then
         for classNameStx in classNamesStx do
-          let className ← resolveGlobalConstNoOverload classNameStx
+          let className ← realizeGlobalConstNoOverload classNameStx
           withRef classNameStx do
             unless (← processDefDeriving className header.declName) do
               throwError "failed to synthesize instance '{className}' for '{header.declName}'"

src/Lean/Elab/Tactic/Induction.lean

@@ -59,7 +59,7 @@ def evalAlt (mvarId : MVarId) (alt : Syntax) (addInfo : TermElabM Unit) : Tactic
   withCaseRef (getAltDArrow alt) rhs do
     if isHoleRHS rhs then
       addInfo
-      mvarId.withContext <| withRef rhs do
+      mvarId.withContext <| withTacticInfoContext rhs do
         let mvarDecl ← mvarId.getDecl
         let val ← elabTermEnsuringType rhs mvarDecl.type
         mvarId.assign val

src/Lean/Elab/Term.lean

@@ -307,7 +307,7 @@ def SavedState.restore (s : SavedState) (restoreInfo : Bool := false) : TermElab
 
 /--
 Restores full state including sources for unique identifiers. Only intended for incremental reuse
-betweeen elaboration runs, not for backtracking within a single run.
+between elaboration runs, not for backtracking within a single run.
 -/
 def SavedState.restoreFull (s : SavedState) : TermElabM Unit := do
   s.meta.restoreFull

src/Lean/Language/Basic.lean

@@ -17,11 +17,6 @@ set_option linter.missingDocs true
 
 namespace Lean.Language
 
-/-- Unique diagnostics ID type of `Snapshot.Diagnostics.id?`. -/
-structure Snapshot.Diagnostics.ID where
-  private id : Nat
-deriving Nonempty, BEq, Ord
-
 /-- `MessageLog` with interactive diagnostics. -/
 structure Snapshot.Diagnostics where
   /-- Non-interactive message log. -/
@@ -36,15 +31,6 @@ structure Snapshot.Diagnostics where
   interactiveDiagsRef? : Option (IO.Ref (Option Dynamic))
 deriving Inhabited
 
-/-- Next ID to be used for `Snapshot.Diagnostics.id?`. -/
--- As the `Nat` value is not observable outside of this  module, using a global ref should be
--- justified and simplifies reporting diagnostics from inside the elaborator
-private builtin_initialize nextDiagsIdRef : IO.Ref Nat ← IO.mkRef 0
-
-/-- Returns a new, unique diagnostics ID. -/
-def Snapshot.Diagnostics.ID.new : BaseIO ID :=
-  nextDiagsIdRef.modifyGet fun id => (⟨id⟩, id + 1)
-
 /-- The empty set of diagnostics. -/
 def Snapshot.Diagnostics.empty : Snapshot.Diagnostics where
   msgLog := .empty

src/Lean/Language/Lean.lean

@@ -169,9 +169,9 @@ register_builtin_option showPartialSyntaxErrors : Bool := {
 /-- Snapshot after elaboration of the entire command. -/
 structure CommandFinishedSnapshot extends Language.Snapshot where
   /-- Resulting elaboration state. -/
-  cmdState : State
+  cmdState : Command.State
 deriving Nonempty
-instance : Language.ToSnapshotTree CommandFinishedSnapshot where
+instance : ToSnapshotTree CommandFinishedSnapshot where
   toSnapshotTree s := ⟨s.toSnapshot, #[]⟩
 
 /-- State after a command has been parsed. -/
@@ -187,6 +187,8 @@ structure CommandParsedSnapshotData extends Snapshot where
   elabSnap : SnapshotTask DynamicSnapshot
   /-- State after processing is finished. -/
   finishedSnap : SnapshotTask CommandFinishedSnapshot
+  /-- Cache for `save`; to be replaced with incrementality. -/
+  tacticCache : IO.Ref Tactic.Cache
 deriving Nonempty
 
 /-- State after a command has been parsed. -/
@@ -213,9 +215,9 @@ partial instance : ToSnapshotTree CommandParsedSnapshot where
 
 /-- 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
+  -- 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)
@@ -449,6 +451,7 @@ where
         diagnostics := .empty, stx := .missing, parserState
         elabSnap := .pure <| .ofTyped { diagnostics := .empty : SnapshotLeaf }
         finishedSnap := .pure { diagnostics := .empty, cmdState }
+        tacticCache := (← IO.mkRef {})
       }
 
     let unchanged old : BaseIO CommandParsedSnapshot :=
@@ -485,11 +488,14 @@ where
         -- on first change, make sure to cancel all further old tasks
         old.cancel
 
-      -- definitely assigned in `doElab` task
-      let headers ← IO.Promise.new
+      -- definitely resolved in `doElab` task
+      let elabPromise ← IO.Promise.new
+      let tacticCache ← old?.map (·.data.tacticCache) |>.getDM (IO.mkRef {})
       let finishedSnap ←
         doElab stx cmdState msgLog.hasErrors beginPos
-          { old? := old?.map fun old => ⟨old.data.stx, old.data.elabSnap⟩, new := headers } ctx
+          { old? := old?.map fun old => ⟨old.data.stx, old.data.elabSnap⟩, new := elabPromise }
+          tacticCache
+          ctx
 
       let next? ← if Parser.isTerminalCommand stx then pure none
         -- for now, wait on "command finished" snapshot before parsing next command
@@ -499,20 +505,28 @@ where
         diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog)
         stx
         parserState
-        elabSnap := { range? := none, task := headers.result }
+        elabSnap := { range? := finishedSnap.range?, task := elabPromise.result }
         finishedSnap
+        tacticCache
       }
 
   doElab (stx : Syntax) (cmdState : Command.State) (hasParseError : Bool) (beginPos : String.Pos)
-      (snap : SnapshotBundle DynamicSnapshot) :
+      (snap : SnapshotBundle DynamicSnapshot) (tacticCache : IO.Ref Tactic.Cache) :
       LeanProcessingM (SnapshotTask CommandFinishedSnapshot) := do
     let ctx ← read
     SnapshotTask.ofIO (stx.getRange?.getD ⟨beginPos, beginPos⟩) do
       let scope := cmdState.scopes.head!
       let cmdStateRef ← IO.mkRef { cmdState with messages := .empty }
+      /-
+      The same snapshot may be executed by different tasks. So, to make sure `elabCommandTopLevel`
+      has exclusive access to the cache, we create a fresh reference here. Before this change, the
+      following `tacticCache.modify` would reset the tactic post cache while another snapshot was
+      still using it.
+      -/
+      let tacticCacheNew ← IO.mkRef (← tacticCache.get)
       let cmdCtx : Elab.Command.Context := { ctx with
         cmdPos       := beginPos
-        tacticCache? := none
+        tacticCache? := some tacticCacheNew
         snap?        := some snap
       }
       let (output, _) ←
@@ -543,8 +557,7 @@ where
           data     := output
         }
       let cmdState := { cmdState with messages }
-      -- only has an effect if actual `resolve` was skipped from fatal exception (caught by
-      -- `catchExceptions` above) or it not being a mutual def
+      -- definitely resolve eventually
       snap.new.resolve <| .ofTyped { diagnostics := .empty : SnapshotLeaf }
       return {
         diagnostics := (← Snapshot.Diagnostics.ofMessageLog cmdState.messages)

src/Lean/Meta/Basic.lean

@@ -373,7 +373,7 @@ def SavedState.restore (b : SavedState) : MetaM Unit := do
 
 /--
 Restores full state including sources for unique identifiers. Only intended for incremental reuse
-betweeen elaboration runs, not for backtracking within a single run.
+between elaboration runs, not for backtracking within a single run.
 -/
 def SavedState.restoreFull (b : SavedState) : MetaM Unit := do
   Core.restoreFull b.core