fix: align speculative elaboration with its input text

Beam/LSP/RunAt.lean

@@ -21,6 +21,21 @@ The speculative execution request family.
 
 This module owns the public `$/lean/runAt` method plus the related handle continuation methods
 `$/lean/runWith` and `$/lean/releaseHandle`.
+
+Execution invariants (a probe is the Lean text supplied by the current request):
+
+- The document position selects a semantic starting state. Newly parsed syntax uses positions
+  relative to the probe, interpreted with that exact text and the parser's `<runAt>` file name.
+  A speculative command's `cmdPos` comes from its own syntax, not the document command.
+- Every execution installs fresh source context and cancellation, including `runWith` from a
+  handle created with different text. These are updates to derived state; elaboration must not
+  mutate the real document or another request's state.
+- Artifact collection follows Lean's reset boundaries: `elabCommandTopLevel` resets command
+  messages, while tactic messages and traces require before/after deltas. Child command snapshot
+  diagnostics are collected once, then their tasks are removed from stored continuation state.
+
+Suggestion range, continuation failure/reuse, and document isolation regressions live in
+`BeamTest.LSP.Requests.RunAt.SuggestionTest`; see `docs/TESTING.md` for their assertions.
 -/
 namespace Beam.LSP.RunAt
 
@@ -210,15 +225,20 @@ def withInnerCancelToken (k : IO.CancelToken → RequestM α) : RequestM α := d
   finally
     finished.resolve ()
 
+/--
+Run using the saved command state. `stx` must have been parsed from `text` with file name `<runAt>`;
+the saved snapshot's syntax and document source do not describe this speculative input.
+-/
 def runCommandElabMWithCancel
     (snap : Snapshots.Snapshot)
-    (doc : DocumentMeta)
+    (stx : Syntax)
+    (text : String)
     (cancelTk? : Option IO.CancelToken)
     (c : Elab.Command.CommandElabM α) : EIO Exception α := do
   let ctx : Command.Context := {
-    cmdPos := snap.stx.getPos? |>.getD 0
-    fileName := doc.uri
-    fileMap := doc.text
+    cmdPos := stx.getPos? |>.getD 0
+    fileName := "<runAt>"
+    fileMap := text.toFileMap
     snap? := none
     cancelTk?
   }
@@ -340,19 +360,17 @@ def runCommandText (snap : Snapshots.Snapshot) (text : String) :
     RequestM (Result × Option StoredHandleState) := do
   checkRequestCancelled
   withInnerCancelToken fun innerCancelTk => do
-    let rc ← readThe RequestContext
     let stx ←
       match parseOneCommandText snap.env text with
       | .ok stx => pure stx
       | .extraInput err => return (oneCommandOnlyResult err, none)
       | .error err => return (errorResult err, none)
     let (output, response) ← IO.FS.withIsolatedStreams do
       EIO.toBaseIO do
-        runCommandElabMWithCancel snap rc.doc.meta (some innerCancelTk) do
+        runCommandElabMWithCancel snap stx text (some innerCancelTk) do
           -- The incoming snapshot can carry already-accounted-for async work from the saved file.
           -- A speculative command result should include only tasks spawned by this command.
           modify fun state => { state with snapshotTasks := #[] }
-          let initialMsgCount := (← get).messages.toList.length
           let initialTraceCount := (← getTraces).size
           let error? ← try
             Elab.Command.elabCommandTopLevel stx
@@ -362,7 +380,9 @@ def runCommandText (snap : Snapshots.Snapshot) (text : String) :
               throw ex
             pure (some (← ex.toMessageData.toString))
           let state ← get
-          let messages := state.messages.toList.drop initialMsgCount
+          -- Lean resets command messages in `elabCommandTopLevel`, including for continuations.
+          -- Traces accumulate instead, so only they use the incoming count here.
+          let messages := state.messages.toList
           let traces := (← getTraces).toList.drop initialTraceCount
           let (snapshotMessages, snapshotTraces) ←
             collectSnapshotTaskArtifacts state.snapshotTasks
@@ -456,6 +476,10 @@ def runTacticText (snapshot : ProofSnapshot) (initialProofState : ProofState) (t
   checkRequestCancelled
   withInnerCancelToken fun innerCancelTk => do
     let snapshot := snapshot.withCancelToken (some innerCancelTk)
+    -- InfoTree reconstruction supplies an empty map; a handle may instead retain an older probe's.
+    -- Replace either with this execution's parser input before interpreting its syntax offsets.
+    let snapshot := { snapshot with coreContext := {
+      snapshot.coreContext with fileName := "<runAt>", fileMap := text.toFileMap } }
     let stx ←
       match Parser.runParserCategory snapshot.coreState.env `tactic text "<runAt>" with
       | .ok stx => pure stx

docs/TESTING.md

@@ -107,6 +107,26 @@ resuming, and check that failed attempts and sibling branches leave the original
 Keep ordinary Lean's own rejection cases as controls; for example, `decide +kernel` rejects a goal
 containing free variables in both execution paths.
 
+The source-context and artifact-lifetime invariants are documented beside the implementation in
+[RunAt.lean](../Beam/LSP/RunAt.lean). The suggestion regressions in
+[SuggestionTest.lean](../tests/lean/BeamTest/LSP/Requests/RunAt/SuggestionTest.lean) exercise fresh
+tactic and command probes, then handle continuations with different input text:
+
+- Test shifted ASCII input as well as multibyte document and probe text. Invalid offsets are not
+  exclusively a Unicode problem.
+- Inspect Lean's typed `TryThisInfo` edits with
+  [SuggestionSupport.lean](../tests/lean/BeamTest/LSP/Requests/RunAt/SuggestionSupport.lean). Require
+  valid UTF-8 boundaries, round trips through LSP's UTF-16 positions, and a range selecting the
+  actual `exact?` source. Rendered suggestion text alone does not establish range correctness.
+- Require new command suggestions and errors to survive a continuation from a handle whose
+  command already emitted messages. A failed continuation must produce no successor handle;
+  the original handle must remain usable for a separate branch.
+- Check the real document's goals and disk source remain unchanged, and compare any newly
+  published diagnostics with the initial diagnostics.
+
+Require absence of captured panic output as well as success and closed goals: a suggestion
+formatter panic can otherwise coexist with an apparently successful tactic result.
+
 The local-recursion tests deliberately distinguish tactic fragments from complete declarations.
 Valid tactic-local `let rec` fragments, including postponed terms and nested `have`/`refine` terms,
 must return an explicit unsupported diagnostic with unchanged goals and no successor handle. Their

tests/lean/BeamTest/LSP/RequestSurfaceTest.lean

@@ -12,6 +12,7 @@ import BeamTest.LSP.Requests.RunAt.BasicTest
 import BeamTest.LSP.Requests.RunAt.AuxiliaryDeclarationTest
 import BeamTest.LSP.Requests.RunAt.AvailabilityTest
 import BeamTest.LSP.Requests.RunAt.HeaderUniverseTest
+import BeamTest.LSP.Requests.RunAt.SuggestionTest
 import BeamTest.LSP.Requests.Save.BasicTest
 import BeamTest.LSP.Requests.Todo.BasicTest
 
@@ -22,6 +23,7 @@ def main : IO Unit := BeamTest.LSP.Scenario.run do
   BeamTest.LSP.Requests.RunAt.AuxiliaryDeclarationTest.run
   BeamTest.LSP.Requests.RunAt.AvailabilityTest.run
   BeamTest.LSP.Requests.RunAt.HeaderUniverseTest.run
+  BeamTest.LSP.Requests.RunAt.SuggestionTest.run
   BeamTest.LSP.Requests.Goals.BasicTest.run
   BeamTest.LSP.Requests.Todo.BasicTest.run
   BeamTest.LSP.Requests.DiagnosticsBarrier.BasicTest.run

tests/lean/BeamTest/LSP/Requests/RunAt/SuggestionSupport.lean

@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Emilio J. Gallego Arias
+-/
+
+import Lean
+
+open Lean Elab Tactic
+
+namespace BeamTest.LSP.Requests.RunAt.SuggestionSupport
+
+private partial def suggestionEdits : InfoTree → Array Lsp.TextEdit
+  | .context _ tree => suggestionEdits tree
+  | .hole _ => #[]
+  | .node info children => Id.run do
+    let mut edits := #[]
+    if let .ofCustomInfo info := info then
+      if let some suggestion := info.value.get? Meta.Tactic.TryThis.TryThisInfo then
+        edits := edits.push suggestion.edit
+    for child in children do
+      edits := edits ++ suggestionEdits child
+    return edits
+
+private def validBoundary (source : String) (pos : String.Pos.Raw) : Bool :=
+  pos.byteIdx ≤ source.utf8ByteSize &&
+    (pos.byteIdx == source.utf8ByteSize || source.toUTF8[pos.byteIdx]! &&& 0xc0 != 0x80)
+
+/-- Inspect the actual typed suggestion edits before the public response renders message text. -/
+elab "check_probe_suggestion " expectedPrefix:str " in " tac:tactic : tactic => do
+  let map ← getFileMap
+  unless map.source.startsWith expectedPrefix.getString do
+    throwError "probe file map does not contain its speculative text"
+  unless (← readThe Core.Context).fileName == "<runAt>" do
+    throwError "probe file name differs from its parser input"
+  let before := (← getInfoTrees).size
+  evalTactic tac
+  let trees := (← getInfoTrees).toArray
+  let edits := (trees.extract before trees.size).foldl
+    (fun edits tree => edits ++ suggestionEdits tree) #[]
+  if edits.isEmpty then
+    throwError "tactic produced no typed suggestion edits"
+  let some expected := tac.raw.getRange? | throwError "tactic has no source range"
+  unless validBoundary map.source expected.start && validBoundary map.source expected.stop do
+    throwError "tactic range is not a valid UTF-8 range in the speculative source"
+  for edit in edits do
+    unless edit.range == map.utf8RangeToLspRange expected do
+      throwError "suggestion range differs from its tactic range"
+    let start := map.lspPosToUtf8Pos edit.range.start
+    let stop := map.lspPosToUtf8Pos edit.range.end
+    unless start == expected.start && stop == expected.stop &&
+        validBoundary map.source start && validBoundary map.source stop do
+      throwError "suggestion range does not round-trip through the speculative source"
+    unless (String.Pos.Raw.extract map.source start stop).trimAscii.toString == "exact?" do
+      throwError "suggestion range does not select its actual source tactic"
+
+end BeamTest.LSP.Requests.RunAt.SuggestionSupport

tests/lean/BeamTest/LSP/Requests/RunAt/SuggestionTest.lean

@@ -0,0 +1,92 @@
+/-
+Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Emilio J. Gallego Arias
+-/
+
+import BeamTest.LSP.Requests.Support
+import BeamTest.LSP.Requests.RunAt.SuggestionSupport
+
+open Lean BeamTest.LSP.Scenario BeamTest.LSP.Requests.Support
+
+namespace BeamTest.LSP.Requests.RunAt.SuggestionTest
+
+private def markerLine (source marker : String) : ScenarioM Nat := do
+  let [(_, line)] := source.splitOn "\n" |>.zipIdx |>.filter (fun (s, _) => s.endsWith s!" -- {marker}")
+    | throw <| IO.userError s!"missing suggestion marker {marker}"
+  pure line
+
+private def requireSuggestion (label : String) (result : Beam.LSP.RunAt.Result) : ScenarioM Unit := do
+  unless result.success &&
+      result.messages.any (·.text.contains "Try this:") &&
+      !result.messages.any (·.text.contains "PANIC") do
+    throw <| IO.userError s!"{label}: invalid suggestion result: {(toJson result).compress}"
+
+private def requireProofSuggestion (label : String) (result : Beam.LSP.RunAt.Result) : ScenarioM Unit := do
+  requireSuggestion label result
+  unless result.proofState?.map (·.goals.isEmpty) == some true do
+    throw <| IO.userError s!"{label}: suggestion did not close the proof"
+
+def run : ScenarioM Unit := do
+  for name in ["RunAtSuggestions", "RunAtSuggestionsUnicode"] do
+    let path : System.FilePath := s!"tests/scenario/docs/{name}.lean"
+    let source ← IO.FS.readFile path
+    let line ← markerLine source "probe"
+    let doc ← openDoc path
+    let initial ← collectDiagnostics doc
+    unless initial.diagnostics.all (fun d => d.severity? != some .error) do
+      throw <| IO.userError "invalid ordinary suggestion fixture"
+    for text in [
+        "check_probe_suggestion \"check_probe\" in exact?",
+        "first | check_probe_suggestion \"first | \" in exact?",
+        "-- éα😀\ncheck_probe_suggestion \"-- éα😀\" in exact?"] do
+      let result ← requireRunAtSuccess s!"{name}: tactic suggestion" doc { line, character := 2 } text
+      requireProofSuggestion name result
+    let req ← sendRunAt doc { line, character := 2, text := "skip", storeHandle := true }
+    let stored ← requireRunAtResponseSuccess "store suggestion basis" req
+    let some handle := stored.handle? | throw <| IO.userError "missing suggestion handle"
+    let failedReq ← runWithHandle doc handle { text := "fail \"expected suggestion rollback\"", storeHandle := true }
+    let failed : Beam.LSP.RunAt.Result ← awaitResponseAs failedReq
+    unless !failed.success && failed.handle?.isNone &&
+        failed.proofState?.map (·.goals.map (·.target)) == some #["True"] do
+      throw <| IO.userError "failed suggestion branch changed its root or produced a successor"
+    for text in [
+        "-- longer ASCII handle input\ncheck_probe_suggestion \"-- longer ASCII\" in exact?",
+        "-- α😀\ncheck_probe_suggestion \"-- α😀\" in exact?"] do
+      let req ← runWithHandle doc handle { text }
+      requireProofSuggestion "handle suggestion" (← requireRunAtResponseSuccess "handle suggestion" req)
+    releaseHandle doc handle
+    let commandLine ← markerLine source "command"
+    let commandText := "-- command éα😀\nexample : True := by\n  check_probe_suggestion \"-- command éα😀\" in exact?"
+    let commandReq ← sendRunAt doc { line := commandLine, character := 0, text := commandText, storeHandle := true }
+    let commandResult ← requireRunAtResponseSuccess "command suggestion" commandReq
+    requireSuggestion "command suggestion" commandResult
+    unless commandResult.proofState?.isNone do
+      throw <| IO.userError "expected a command suggestion basis"
+    let some commandHandle := commandResult.handle? | throw <| IO.userError "missing command suggestion handle"
+    let rejected ← runWithHandle doc commandHandle {
+      text := "#check missingSuggestionConstant"
+      storeHandle := true
+    }
+    let rejectedResult : Beam.LSP.RunAt.Result ← awaitResponseAs rejected
+    unless !rejectedResult.success && rejectedResult.handle?.isNone &&
+        rejectedResult.messages.any (·.severity == .error) do
+      throw <| IO.userError "command continuation discarded its new error diagnostics"
+    let continuation ← runWithHandle doc commandHandle {
+      text := "-- different command input\nexample : True := by\n  check_probe_suggestion \"-- different command\" in exact?"
+    }
+    requireSuggestion "command handle suggestion"
+      (← requireRunAtResponseSuccess "command handle suggestion" continuation)
+    releaseHandle doc commandHandle
+    let goalsReq ← sendGoals doc { line, character := 2, useAfter := false }
+    let goals : Beam.LSP.Lib.ProofState ← awaitResponseAs goalsReq
+    unless goals.goals.map (·.target) == #["True"] do
+      throw <| IO.userError "suggestion probe changed the real proof state"
+    if let some after ← collectDiagnostics? doc then
+      unless after.diagnostics == initial.diagnostics do
+        throw <| IO.userError "suggestion probe changed the real document diagnostics"
+    closeDoc doc
+    unless (← IO.FS.readFile path) == source do
+      throw <| IO.userError "suggestion probe changed the real document source"
+
+end BeamTest.LSP.Requests.RunAt.SuggestionTest

tests/lsp-coverage/cases.json

@@ -1,5 +1,17 @@
 {
   "cases": [
+    {
+      "id": "runAt.suggestion-ranges",
+      "method": "$/lean/runAt",
+      "coverage": ["suggestion-ranges", "isolation"],
+      "pointer": "tests/lean/BeamTest/LSP/Requests/RunAt/SuggestionTest.lean#run"
+    },
+    {
+      "id": "runWith.suggestion-ranges",
+      "method": "$/lean/runWith",
+      "coverage": ["suggestion-ranges", "handle-continuation"],
+      "pointer": "tests/lean/BeamTest/LSP/Requests/RunAt/SuggestionTest.lean#run"
+    },
     {
       "id": "runAt.header-universes",
       "method": "$/lean/runAt",

tests/lsp-coverage/methods.json

@@ -19,7 +19,8 @@
         "stale-edit",
         "cancellation",
         "standard-lsp-interference",
-        "mixed-concurrency"
+        "mixed-concurrency",
+        "suggestion-ranges"
       ]
     },
     {
@@ -38,7 +39,8 @@
         "document-edit-invalidation",
         "document-close-invalidation",
         "standard-lsp-interference",
-        "mixed-concurrency"
+        "mixed-concurrency",
+        "suggestion-ranges"
       ]
     },
     {

tests/scenario/docs/RunAtSuggestions.lean

@@ -0,0 +1,6 @@
+import BeamTest.LSP.Requests.RunAt.SuggestionSupport
+
+theorem suggestionGoal : True := by
+  trivial -- probe
+
+#check Nat -- command

tests/scenario/docs/RunAtSuggestionsUnicode.lean

@@ -0,0 +1,7 @@
+import BeamTest.LSP.Requests.RunAt.SuggestionSupport
+
+-- Multibyte document text: éα😀
+theorem suggestionGoalUnicode : True := by
+  trivial -- probe
+
+#check Nat -- command