fix: incremental goal state requests select incomplete snapshot

src/Init/Prelude.lean

@@ -2503,6 +2503,9 @@ instance (p₁ p₂ : String.Pos) : Decidable (LE.le p₁ p₂) :=
 instance (p₁ p₂ : String.Pos) : Decidable (LT.lt p₁ p₂) :=
   inferInstanceAs (Decidable (LT.lt p₁.byteIdx p₂.byteIdx))
 
+instance : Min String.Pos := minOfLe
+instance : Max String.Pos := maxOfLe
+
 /-- A `String.Pos` pointing at the end of this string. -/
 @[inline] def String.endPos (s : String) : String.Pos where
   byteIdx := utf8ByteSize s

src/Lean/AddDecl.lean

@@ -84,7 +84,7 @@ def addDecl (decl : Declaration) : CoreM Unit := do
       async.commitFailure
   let t ← BaseIO.mapTask (fun _ => checkAct) env.checked
   let endRange? := (← getRef).getTailPos?.map fun pos => ⟨pos, pos⟩
-  Core.logSnapshotTask { range? := endRange?, task := t }
+  Core.logSnapshotTask { stx? := none, reportingRange? := endRange?, task := t }
 where doAdd := do
   profileitM Exception "type checking" (← getOptions) do
     withTraceNode `Kernel (fun _ => return m!"typechecking declarations {decl.getNames}") do

src/Lean/Data/Lsp/Basic.lean

@@ -27,7 +27,7 @@ offsets. For diagnostics, one-based `Lean.Position`s are used internally.
 structure Position where
   line : Nat
   character : Nat
-  deriving Inhabited, BEq, Ord, Hashable, ToJson, FromJson
+  deriving Inhabited, BEq, Ord, Hashable, ToJson, FromJson, Repr
 
 instance : ToString Position := ⟨fun p =>
   "(" ++ toString p.line ++ ", " ++ toString p.character ++ ")"⟩
@@ -38,7 +38,7 @@ instance : LE Position := leOfOrd
 structure Range where
   start : Position
   «end» : Position
-  deriving Inhabited, BEq, Hashable, ToJson, FromJson, Ord
+  deriving Inhabited, BEq, Hashable, ToJson, FromJson, Ord, Repr
 
 instance : LT Range := ltOfOrd
 instance : LE Range := leOfOrd

src/Lean/Elab/Command.lean

@@ -359,7 +359,7 @@ def runLintersAsync (stx : Syntax) : CommandElabM Unit := do
   -- We only start one task for all linters for now as most linters are fast and we simply want
   -- to unblock elaboration of the next command
   let lintAct ← wrapAsyncAsSnapshot fun _ => runLinters stx
-  logSnapshotTask { range? := none, task := (← BaseIO.asTask lintAct) }
+  logSnapshotTask { stx? := none, task := (← BaseIO.asTask lintAct) }
 
 protected def getCurrMacroScope : CommandElabM Nat  := do pure (← read).currMacroScope
 protected def getMainModule     : CommandElabM Name := do pure (← getEnv).mainModule
@@ -497,7 +497,7 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
                     newNextMacroScope := nextMacroScope
                     hasTraces
                     next := cmdPromises.zipWith cmds fun cmdPromise cmd =>
-                      { range? := cmd.getRange?, task := cmdPromise.result }
+                      { stx? := cmd, task := cmdPromise.result }
                     : MacroExpandedSnapshot
                   }
                   -- After the first command whose syntax tree changed, we must disable

src/Lean/Elab/MutualDef.lean

@@ -215,6 +215,17 @@ private def elabHeaders (views : Array DefView)
             return newHeader
       if let some snap := view.headerSnap? then
         let (tacStx?, newTacTask?) ← mkTacTask view.value tacPromise
+        let bodySnap := {
+          stx? := none
+          reportingRange? :=
+            if newTacTask?.isSome then
+              -- Only use first line of body as range when we have incremental tactics as otherwise we
+              -- would cover their progress
+              view.ref.getPos?.map fun pos => ⟨pos, pos⟩
+            else
+              getBodyTerm? view.value |>.getD view.value |>.getRange?
+          task := bodyPromise.result
+        }
         snap.new.resolve <| some {
           diagnostics :=
             (← Language.Snapshot.Diagnostics.ofMessageLog (← Core.getAndEmptyMessageLog))
@@ -223,7 +234,7 @@ private def elabHeaders (views : Array DefView)
           tacStx?
           tacSnap? := newTacTask?
           bodyStx := view.value
-          bodySnap := mkBodyTask view.value bodyPromise
+          bodySnap
         }
         newHeader := { newHeader with
           -- We should only forward the promise if we are actually waiting on the
@@ -245,12 +256,6 @@ where
     guard whereDeclsOpt.isNone
     return body
 
-  /-- 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
@@ -261,7 +266,7 @@ where
    := do
     if let some e := getBodyTerm? body then
       if let `(by $tacs*) := e then
-        return (e, some { range? := mkNullNode tacs |>.getRange?, task := tacPromise.result })
+        return (e, some { stx? := mkNullNode tacs, task := tacPromise.result })
     tacPromise.resolve default
     return (none, none)
 
@@ -1075,7 +1080,7 @@ def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
         } }
         defs := defs.push {
           fullHeaderRef
-          headerProcessedSnap := { range? := d.getRange?, task := headerPromise.result }
+          headerProcessedSnap := { stx? := d, task := headerPromise.result }
         }
         reusedAllHeaders := reusedAllHeaders && view.headerSnap?.any (·.old?.isSome)
       views := views.push view

src/Lean/Elab/Tactic/Basic.lean

@@ -230,11 +230,11 @@ where
                       stx := stx'
                       diagnostics := .empty
                       inner? := none
-                      finished := .pure {
+                      finished := .finished stx' {
                         diagnostics := .empty
                         state? := (← Tactic.saveState)
                       }
-                      next := #[{ range? := stx'.getRange?, task := promise.result }]
+                      next := #[{ stx? := stx', task := promise.result }]
                     }
                     -- Update `tacSnap?` to old unfolding
                     withTheReader Term.Context ({ · with tacSnap? := some {

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -75,27 +75,16 @@ where
           -- only allow `next` reuse in this case
           oldNext? := oldParsed.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 {
               desc := tac.getKind.toString
               diagnostics := .empty
               stx := tac
-              inner? := some { range?, task := inner.result }
-              finished := { range?, task := finished.result }
-              next := #[{ range? := stxs.getRange?, task := next.result }]
+              inner? := some { stx? := tac, task := inner.result }
+              finished := { stx? := tac, task := finished.result }
+              next := #[{ stx? := stxs, 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`

src/Lean/Elab/Tactic/Induction.lean

@@ -285,9 +285,13 @@ where
               stx := mkNullNode altStxs
               diagnostics := .empty
               inner? := none
-              finished := { range? := none, task := finished.result }
+              finished := {
+                stx? := mkNullNode altStxs
+                reportingRange? := none
+                task := finished.result
+              }
               next := altStxs.zipWith altPromises fun stx prom =>
-                { range? := stx.getRange?, task := prom.result }
+                { stx? := stx, task := prom.result }
             }
             goWithIncremental <| altPromises.mapIdx fun i prom => {
               old? := do

src/Lean/Language/Basic.lean

@@ -66,31 +66,48 @@ structure Snapshot where
   isFatal := false
 deriving Inhabited
 
+/--
+Yields the default reporting range of a `Syntax`, which is just the `canonicalOnly` range
+of the syntax.
+-/
+def SnapshotTask.defaultReportingRange? (stx? : Option Syntax) : Option String.Range :=
+  stx?.bind (·.getRange? (canonicalOnly := true))
+
 /-- A task producing some snapshot type (usually a subclass of `Snapshot`). -/
 -- Longer-term TODO: Give the server more control over the priority of tasks, depending on e.g. the
 -- 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
+  /--
+  `Syntax` processed by this `SnapshotTask`.
+  The `Syntax` is used by the language server to determine whether to force this `SnapshotTask`
+  when a request is made.
+  -/
+  stx? : Option Syntax
   /--
   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
+  reportingRange? : Option String.Range := SnapshotTask.defaultReportingRange? stx?
   /-- Underlying task producing the snapshot. -/
   task : Task α
 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
+/-- Creates a snapshot task from the syntax processed by the task and a `BaseIO` action. -/
+def SnapshotTask.ofIO (stx? : Option Syntax)
+    (reportingRange? : Option String.Range := defaultReportingRange? stx?) (act : BaseIO α) :
+    BaseIO (SnapshotTask α) := do
   return {
-    range?
+    stx?
+    reportingRange?
     task := (← BaseIO.asTask act)
   }
 
 /-- Creates a finished snapshot task. -/
-def SnapshotTask.pure (a : α) : SnapshotTask α where
+def SnapshotTask.finished (stx? : Option Syntax) (a : α) : SnapshotTask α where
+  stx?
   -- irrelevant when already finished
-  range? := none
+  reportingRange? := none
   task := .pure a
 
 /--
@@ -99,25 +116,30 @@ def SnapshotTask.pure (a : α) : SnapshotTask α where
 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? : Option String.Range := t.range?)
-    (sync := false) : SnapshotTask β :=
-  { range?, task := t.task.map (sync := sync) f }
+/-- Transforms a task's output without changing the processed syntax. -/
+def SnapshotTask.map (t : SnapshotTask α) (f : α → β) (stx? : Option Syntax := t.stx?)
+    (reportingRange? : Option String.Range := t.reportingRange?) (sync := false) : SnapshotTask β :=
+  { stx?, reportingRange?, 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. -/
+  Chains two snapshot tasks. The processed syntax and the reporting range are taken from the first
+  task if not specified; the processed syntax and the reporting range of the second task are
+  discarded. -/
 def SnapshotTask.bind (t : SnapshotTask α) (act : α → SnapshotTask β)
-    (range? : Option String.Range := t.range?) (sync := false) : SnapshotTask β :=
-  { range?, task := t.task.bind (sync := sync) (act · |>.task) }
+    (stx? : Option Syntax := t.stx?) (reportingRange? : Option String.Range := t.reportingRange?)
+    (sync := false) : SnapshotTask β :=
+  { stx?, reportingRange?, 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. -/
+  Chains two snapshot tasks. The processed syntax and the reporting range are taken from the first
+  task if not specified; the processed syntax and the reporting range of the second task are
+  discarded. -/
 def SnapshotTask.bindIO (t : SnapshotTask α) (act : α → BaseIO (SnapshotTask β))
-    (range? : Option String.Range := t.range?) (sync := false) : BaseIO (SnapshotTask β) :=
+    (stx? : Option Syntax := t.stx?) (reportingRange? : Option String.Range := t.reportingRange?)
+    (sync := false) : BaseIO (SnapshotTask β) :=
   return {
-    range?
+    stx?
+    reportingRange?
     task := (← BaseIO.bindTask (sync := sync) t.task fun a => (·.task) <$> (act a))
   }