feat: respond to info view requests as soon as relevant tactic has finished execution

src/Lean/Elab/Command.lean

@@ -479,7 +479,7 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro
       -- should be true iff the command supports incrementality
       if (← IO.hasFinished snap.new.result) then
         trace[Elab.snapshotTree]
-          Language.ToSnapshotTree.toSnapshotTree snap.new.result.get |>.format
+          (←Language.ToSnapshotTree.toSnapshotTree snap.new.result.get |>.format)
     modify fun st => { st with
       messages := initMsgs ++ msgs
       infoState := { st.infoState with trees := initInfoTrees ++ st.infoState.trees }

src/Lean/Elab/Tactic/Basic.lean

@@ -155,7 +155,9 @@ partial def evalTactic (stx : Syntax) : TacticM Unit := do
         -- Macro writers create a sequence of tactics `t₁ ... tₙ` using `mkNullNode #[t₁, ..., tₙ]`
         -- We could support incrementality here by allocating `n` new snapshot bundles but the
         -- practical value is not clear
-        Term.withoutTacticIncrementality true do
+        -- NOTE: `withTacticInfoContext` is used to preserve the invariant of `elabTactic` producing
+        -- exactly one info tree, which is necessary for using `getInfoTreeWithContext`.
+        Term.withoutTacticIncrementality true <| withTacticInfoContext stx do
           stx.getArgs.forM evalTactic
       else withTraceNode `Elab.step (fun _ => return stx) (tag := stx.getKind.toString) do
         let evalFns := tacticElabAttribute.getEntries (← getEnv) stx.getKind
@@ -222,14 +224,18 @@ where
                     snap.new.resolve <| .mk {
                       stx := stx'
                       diagnostics := .empty
-                      finished := .pure { state? := (← Tactic.saveState) }
-                    } #[{ range? := stx'.getRange?, task := promise.result }]
+                      finished := .pure {
+                        diagnostics := .empty
+                        state? := (← Tactic.saveState)
+                      }
+                      next := #[{ range? := stx'.getRange?, task := promise.result }]
+                    }
                     -- Update `tacSnap?` to old unfolding
                     withTheReader Term.Context ({ · with tacSnap? := some {
                       new := promise
                       old? := do
                         let old ← old?
-                        return ⟨old.data.stx, (← old.next.get? 0)⟩
+                        return ⟨old.data.stx, (← old.data.next.get? 0)⟩
                     } }) do
                       evalTactic stx'
                   return

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -60,7 +60,7 @@ where
     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, ·⟩)
+        oldInner? := oldParsed.data.inner? |>.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?
@@ -73,29 +73,47 @@ where
         if let some state := oldParsed.data.finished.get.state? then
           reusableResult? := some ((), state)
           -- only allow `next` reuse in this case
-          oldNext? := oldParsed.next.get? 1 |>.map (⟨old.stx, ·⟩)
-
+          oldNext? := oldParsed.data.next.get? 0 |>.map (⟨old.stx, ·⟩)
+
+      -- For `tac`'s snapshot task range, disregard synthetic info as otherwise
+      -- `SnapshotTree.findInfoTreeAtPos` might choose the wrong snapshot: for example, when
+      -- hovering over a `show` tactic, we should choose the info tree in `finished` over that in
+      -- `inner`, which points to execution of the synthesized `refine` step and does not contain
+      -- the full info. In most other places, siblings in the snapshot tree have disjoint ranges and
+      -- so this issue does not occur.
+      let mut range? := tac.getRange? (canonicalOnly := true)
+      -- Include trailing whitespace in the range so that `goalsAs?` does not have to wait for more
+      -- snapshots than necessary.
+      if let some range := range? then
+        range? := some { range with stop := ⟨range.stop.byteIdx + tac.getTrailingSize⟩ }
       withAlwaysResolvedPromise fun next => do
         withAlwaysResolvedPromise fun finished => do
           withAlwaysResolvedPromise fun inner => do
             snap.new.resolve <| .mk {
+              diagnostics := .empty
               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?
-                -- set up nested reuse; `evalTactic` will check for `isIncrementalElab`
-                (tacSnap? := some { old? := oldInner?, new := inner }) do
-              Term.withReuseContext tac do
-                evalTactic tac
-            finished.resolve { state? := state }
+              inner? := some { range?, task := inner.result }
+              finished := { range?, task := finished.result }
+              next := #[{ range? := stxs.getRange?, task := next.result }]
+            }
+            -- Run `tac` in a fresh info tree state and store resulting state in snapshot for
+            -- incremental reporting, then add back saved trees. Here we rely on `evalTactic`
+            -- producing at most one info tree as otherwise `getInfoTreeWithContext?` would panic.
+            let trees ← getResetInfoTrees
+            try
+              let (_, state) ← withRestoreOrSaveFull reusableResult?
+                  -- set up nested reuse; `evalTactic` will check for `isIncrementalElab`
+                  (tacSnap? := some { old? := oldInner?, new := inner }) do
+                Term.withReuseContext tac do
+                  evalTactic tac
+              finished.resolve {
+                diagnostics := (← Language.Snapshot.Diagnostics.ofMessageLog
+                  (← Core.getAndEmptyMessageLog))
+                infoTree? := (← Term.getInfoTreeWithContext?)
+                state? := state
+              }
+            finally
+              modifyInfoState fun s => { s with trees := trees ++ s.trees }
 
         withTheReader Term.Context ({ · with tacSnap? := some {
           new := next

src/Lean/Elab/Tactic/Induction.lean

@@ -263,9 +263,10 @@ where
               -- 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 })
+              finished := { range? := none, task := finished.result }
+              next := altStxs.zipWith altPromises fun stx prom =>
+                { range? := stx.getRange?, task := prom.result }
+            }
             goWithIncremental <| altPromises.mapIdx fun i prom => {
               old? := do
                 let old ← tacSnap.old?
@@ -274,10 +275,10 @@ where
                 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]?)⟩
+                return ⟨old.data.stx, (← old.data.next[i]?)⟩
               new := prom
             }
-            finished.resolve { state? := (← saveState) }
+            finished.resolve { diagnostics := .empty, state? := (← saveState) }
         return
 
     goWithIncremental #[]

src/Lean/Elab/Term.lean

@@ -190,33 +190,38 @@ 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. -/
+/-- Snapshot after finishing execution of a tactic. -/
+structure TacticFinishedSnapshot extends Language.Snapshot where
+  /-- State saved for reuse, if no fatal exception occurred. -/
   state? : Option SavedState
 deriving Inhabited
+instance : ToSnapshotTree TacticFinishedSnapshot where
+  toSnapshotTree s := ⟨s.toSnapshot, #[]⟩
 
 /-- Snapshot just before execution of a tactic. -/
-structure TacticParsedSnapshotData extends Language.Snapshot where
+structure TacticParsedSnapshotData (TacticParsedSnapshot : Type) extends Language.Snapshot where
   /-- Syntax tree of the tactic, stored and compared for incremental reuse. -/
   stx      : Syntax
+  /-- Task for nested incrementality, if enabled for tactic. -/
+  inner?   : Option (SnapshotTask TacticParsedSnapshot) := none
   /-- Task for state after tactic execution. -/
-  finished : Task TacticFinished
+  finished : SnapshotTask TacticFinishedSnapshot
+  /-- Tasks for subsequent, potentially parallel, tactic steps. -/
+  next     : Array (SnapshotTask TacticParsedSnapshot) := #[]
 deriving Inhabited
 
 /-- State after execution of a single synchronous tactic step. -/
 inductive TacticParsedSnapshot where
-  | mk (data : TacticParsedSnapshotData) (next : Array (SnapshotTask TacticParsedSnapshot))
+  | mk (data : TacticParsedSnapshotData 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
+abbrev TacticParsedSnapshot.data : TacticParsedSnapshot → TacticParsedSnapshotData TacticParsedSnapshot
+  | .mk data => data
 partial instance : ToSnapshotTree TacticParsedSnapshot where
   toSnapshotTree := go where
-    go := fun ⟨s, next⟩ => ⟨s.toSnapshot, next.map (·.map (sync := true) go)⟩
+    go := fun ⟨s⟩ => ⟨s.toSnapshot,
+      s.inner?.toArray.map (·.map (sync := true) go) ++
+      #[s.finished.map (sync := true) toSnapshotTree] ++
+      s.next.map (·.map (sync := true) go)⟩
 
 end Snapshot
 end Tactic
@@ -630,6 +635,32 @@ private def withoutModifyingStateWithInfoAndMessagesImpl (x : TermElabM α) : Te
     let saved := { saved with meta.core.infoState := (← getInfoState), meta.core.messages := (← getThe Core.State).messages }
     restoreState saved
 
+/--
+Wraps the trees returned from `getInfoTrees`, if any, in an `InfoTree.context` node based on the
+current monadic context and state. This is mainly used to report info trees early via
+`Snapshot.infoTree?`. The trees are not removed from the `getInfoTrees` state as the final info tree
+of the elaborated command should be complete and not depend on whether parts have been reported
+early.
+
+As `InfoTree.context` can have only one child, this function panics if `trees` contains more than 1
+tree. Also, `PartialContextInfo.parentDeclCtx` is not currently generated as that information is not
+available in the monadic context and only needed for the final info tree.
+-/
+def getInfoTreeWithContext? : TermElabM (Option InfoTree) := do
+  let st ← getInfoState
+  if st.trees.size > 1 then
+    return panic! "getInfoTreeWithContext: overfull tree"
+  let some t := st.trees[0]? |
+    return none
+  let t := t.substitute st.assignment
+  let ctx ← readThe Core.Context
+  let s ← getThe Core.State
+  let ctx := PartialContextInfo.commandCtx {
+    env := s.env, fileMap := ctx.fileMap, mctx := {}, currNamespace := ctx.currNamespace,
+    openDecls := ctx.openDecls, options := ctx.options, ngen := s.ngen
+  }
+  return InfoTree.context ctx t
+
 /-- For testing `TermElabM` methods. The #eval command will sign the error. -/
 def throwErrorIfErrors : TermElabM Unit := do
   if (← MonadLog.hasErrors) then

src/Lean/Language/Basic.lean

@@ -12,6 +12,7 @@ prelude
 import Init.System.Promise
 import Lean.Message
 import Lean.Parser.Types
+import Lean.Elab.InfoTree
 
 set_option linter.missingDocs true
 
@@ -46,6 +47,8 @@ def Snapshot.Diagnostics.empty : Snapshot.Diagnostics where
   The base class of all snapshots: all the generic information the language server needs about a
   snapshot. -/
 structure Snapshot where
+  /-- Debug description shown by `trace.Elab.snapshotTree`, defaults to the caller's decl name. -/
+  desc : String := by exact decl_name%.toString
   /--
     The messages produced by this step. The union of message logs of all finished snapshots is
     reported to the user. -/
@@ -71,7 +74,7 @@ structure SnapshotTask (α : Type) where
   range? : Option String.Range
   /-- Underlying task producing the snapshot. -/
   task : Task α
-deriving Nonempty
+deriving Nonempty, Inhabited
 
 /-- Creates a snapshot task from a reporting range and a `BaseIO` action. -/
 def SnapshotTask.ofIO (range? : Option String.Range) (act : BaseIO α) : BaseIO (SnapshotTask α) := do
@@ -203,15 +206,19 @@ abbrev SnapshotTree.children : SnapshotTree → Array (SnapshotTask SnapshotTree
   | mk _ children => children
 
 /-- Produces debug tree format of given snapshot tree, synchronously waiting on all children. -/
-partial def SnapshotTree.format : SnapshotTree → Format := go none
-where go range? s :=
-  let range := match range? with
-    | some range => f!"{range.start}..{range.stop} "
-    | none => ""
-  let element := f!"{s.element.diagnostics.msgLog.unreported.size} diagnostics"
-  let children := Std.Format.prefixJoin .line <|
-    s.children.toList.map fun c => go c.range? c.get
-  .nestD f!"• {range}{element}{children}"
+partial def SnapshotTree.format [Monad m] [MonadFileMap m] [MonadLiftT IO m] :
+    SnapshotTree → m Format :=
+  go none
+where go range? s := do
+  let file ← getFileMap
+  let mut desc := f!"• {s.element.desc}"
+  if let some range := range? then
+    desc := desc ++ f!"{file.toPosition range.start}-{file.toPosition range.stop} "
+  desc := desc ++ .prefixJoin "\n• " (← s.element.diagnostics.msgLog.toList.mapM (·.toString))
+  if let some t := s.element.infoTree? then
+    desc := desc ++ f!"\n{← t.format}"
+  desc := desc ++ .prefixJoin "\n" (← s.children.toList.mapM fun c => go c.range? c.get)
+  return .nestD desc
 
 /--
   Helper class for projecting a heterogeneous hierarchy of snapshot classes to a homogeneous

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -234,31 +234,27 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
   let doc ← readDoc
   let text := doc.meta.text
   let hoverPos := text.lspPosToUtf8Pos p.position
-  -- NOTE: use `>=` since the cursor can be *after* the input
-  withWaitFindSnap doc (fun s => s.endPos >= hoverPos)
-    (notFoundX := return none) fun snap => do
-      if let rs@(_ :: _) := snap.infoTree.goalsAt? doc.meta.text hoverPos then
-        let goals : List Widget.InteractiveGoals ← rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter, .. } => do
-          let ciAfter := { ci with mctx := ti.mctxAfter }
-          let ci := if useAfter then ciAfter else { ci with mctx := ti.mctxBefore }
-          -- compute the interactive goals
-          let goals ← ci.runMetaM {} (do
-            let goals := List.toArray <| if useAfter then ti.goalsAfter else ti.goalsBefore
-            let goals ← goals.mapM Widget.goalToInteractive
-            return {goals}
-          )
-          -- compute the goal diff
-          let goals ← ciAfter.runMetaM {} (do
-              try
-                Widget.diffInteractiveGoals useAfter ti goals
-              catch _ =>
-                -- fail silently, since this is just a bonus feature
-                return goals
-          )
-          return goals
-        return some <| goals.foldl (· ++ ·) ∅
-      else
-        return none
+  mapTask (findInfoTreeAtPos doc hoverPos) <| Option.bindM fun infoTree => do
+    let rs@(_ :: _) := infoTree.goalsAt? doc.meta.text hoverPos
+      | return none
+    let goals : List Widget.InteractiveGoals ← rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter, .. } => do
+      let ciAfter := { ci with mctx := ti.mctxAfter }
+      let ci := if useAfter then ciAfter else { ci with mctx := ti.mctxBefore }
+      -- compute the interactive goals
+      let goals ← ci.runMetaM {} (do
+        let goals := List.toArray <| if useAfter then ti.goalsAfter else ti.goalsBefore
+        let goals ← goals.mapM Widget.goalToInteractive
+        return {goals}
+      )
+      -- compute the goal diff
+      ciAfter.runMetaM {} (do
+          try
+            Widget.diffInteractiveGoals useAfter ti goals
+          catch _ =>
+            -- fail silently, since this is just a bonus feature
+            return goals
+      )
+    return some <| goals.foldl (· ++ ·) ∅
 
 open Elab in
 def handlePlainGoal (p : PlainGoalParams)
@@ -280,19 +276,17 @@ def getInteractiveTermGoal (p : Lsp.PlainTermGoalParams)
   let doc ← readDoc
   let text := doc.meta.text
   let hoverPos := text.lspPosToUtf8Pos p.position
-  withWaitFindSnap doc (fun s => s.endPos > hoverPos)
-    (notFoundX := pure none) fun snap => do
-      if let some {ctx := ci, info := i@(Elab.Info.ofTermInfo ti), ..} := snap.infoTree.termGoalAt? hoverPos then
-        let ty ← ci.runMetaM i.lctx do
-          instantiateMVars <| ti.expectedType?.getD (← Meta.inferType ti.expr)
-        -- for binders, hide the last hypothesis (the binder itself)
-        let lctx' := if ti.isBinder then i.lctx.pop else i.lctx
-        let goal ← ci.runMetaM lctx' do
-          Widget.goalToInteractive (← Meta.mkFreshExprMVar ty).mvarId!
-        let range := if let some r := i.range? then r.toLspRange text else ⟨p.position, p.position⟩
-        return some { goal with range, term := ⟨ti⟩ }
-      else
-        return none
+  mapTask (findInfoTreeAtPos doc hoverPos) <| Option.bindM fun infoTree => do
+    let some {ctx := ci, info := i@(Elab.Info.ofTermInfo ti), ..} := infoTree.termGoalAt? hoverPos
+      | return none
+    let ty ← ci.runMetaM i.lctx do
+      instantiateMVars <| ti.expectedType?.getD (← Meta.inferType ti.expr)
+    -- for binders, hide the last hypothesis (the binder itself)
+    let lctx' := if ti.isBinder then i.lctx.pop else i.lctx
+    let goal ← ci.runMetaM lctx' do
+      Widget.goalToInteractive (← Meta.mkFreshExprMVar ty).mvarId!
+    let range := if let some r := i.range? then r.toLspRange text else ⟨p.position, p.position⟩
+    return some { goal with range, term := ⟨ti⟩ }
 
 def handlePlainTermGoal (p : PlainTermGoalParams)
     : RequestM (RequestTask (Option PlainTermGoal)) := do