feat: respond to info view requests as soon as relevant tactic has fi…

…nished execution (#4727)

After each tactic step, we save the info tree created by it together
with an appropriate info tree context that makes it stand-alone (which
we already did before to some degree, see `Info.updateContext?`). Then,
in the adjusted request handlers, we first search for a snapshot task
containing the required position, if so wait on it, and if it yielded an
info tree, use it to answer the request, or else continue searching and
waiting, falling back to the full info tree, which should be unchanged
by this PR.

The definition header does *not* report info trees early as in general
it is not stand-alone in the tactic sense but may contain e.g.
metavariables solved by the body in which case we do want to show the
ultimate state as before. This could be refined in the future in case
there are no unsolved mvars.

The adjusted request handlers are exactly the ones waited on together by
the info view, so they all have to be adjusted to have any effect on the
UX. Further request handlers may be adjusted in the future.

No new tests as "replies early" is not something we can test with our
current framework but the existing test suite did help in uncovering
functional regressions.

src/Lean/Elab/Command.lean

@@ -525,7 +525,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

@@ -156,7 +156,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
@@ -223,14 +225,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