fix: report runAt tactic probes that use the declaration being proved

Beam/LSP/RunAt.lean

@@ -509,13 +509,27 @@ def runTacticText (snapshot : ProofSnapshot) (initialProofState : ProofState) (t
             -- restore the failed proof state rather than backtracking its messages.
             tryCatchRuntimeEx
               (do
+                let initialGoals ← Elab.Tactic.getGoals
                 Elab.Tactic.evalTactic stx
                 Elab.Term.synthesizeSyntheticMVarsNoPostponing
                 -- Lean lifts local recursive definitions and checks their termination when
                 -- finalizing the enclosing declaration. A standalone tactic probe has no such
                 -- finalization step, so it must not report these pending definitions as solved.
                 unless (← Elab.Term.getLetRecsToLift).isEmpty do
                   throwError "Local recursive declarations are not supported in runAt tactics. Add the declaration to the document and sync before probing."
+                -- While a declaration elaborates, Lean exposes it to its own body as an auxiliary
+                -- local, and finalization checks every use for termination. A probe has no such
+                -- step, so a use proves nothing about the edit; report it instead of success.
+                let declName? ← Elab.Term.getDeclName?
+                for goal in initialGoals do
+                  let lctx := (← goal.getDecl).lctx
+                  let value ← instantiateMVars (mkMVar goal)
+                  let selfRef? := value.find? fun e =>
+                    (e.isFVar && (lctx.find? e.fvarId!).any (·.isAuxDecl)) ||
+                      (e.isConst && declName? == some e.constName!)
+                  if let some ref := selfRef? then
+                    let name := if ref.isFVar then (lctx.get! ref.fvarId!).userName else ref.constName!
+                    throwError "This probe refers to `{name}`, the declaration it is inside. runAt cannot check termination for that reference, so its result does not show whether the edit elaborates. Make the edit and sync to check it."
                 let (messages, traces) ← collectNewTacticArtifacts initialMsgCount initialTraceCount
                 return { disposition := .keepAdvanced, error? := none, messages, traces })
               (fun ex => do

CHANGELOG.md

@@ -19,6 +19,10 @@ This project keeps a lightweight, reverse-chronological changelog. Dates use `YY
 - Clarify that installer skill and MCP setup summaries describe only actions performed during
   the current run, so skipped registration does not imply that existing client setup is absent
   ([#394](https://github.com/leanprover/lean-beam/pull/394), @ejgallego).
+- A tactic probe that uses the declaration being proved, or another member of its `mutual` block,
+  now returns `success: false` with the original proof state and a message naming that declaration,
+  instead of reporting success for an edit that Lean's termination check may reject
+  ([#413](https://github.com/leanprover/lean-beam/pull/413), @ejgallego).
 - `references` now waits for Lean to finish the requested document version, so a query right after
   `update` reports that version's references instead of `[]` or locations from the previous text
   ([#399](https://github.com/leanprover/lean-beam/pull/399), @ejgallego).

docs/MCP.md

@@ -328,10 +328,10 @@ code-action resolution. Raw LSP methods and generic broker escape hatches are in
 
 The [proof-probe limitations](STATUS.md#operational-notes) also apply to `lean_run_at`,
 `lean_run_at_handle`, `lean_run_with`, and `lean_run_with_linear`: introducing a local `let rec` in a
-tactic returns `success=false`, the original proof state, and no successor handle, even when the
-recursion is valid. Save the complete enclosing declaration and call `lean_sync` to validate it;
-use the returned version and fresh handles after the edit. Complete command probes use Lean's
-normal termination checks. The skill's
+tactic, or using the declaration being proved, returns `success=false`, the original proof state,
+and no successor handle, even when the recursion is valid. Save the complete enclosing declaration
+and call `lean_sync` to validate it; use the returned version and fresh handles after the edit.
+Complete command probes use Lean's normal termination checks. The skill's
 [local recursion workflow](../skills/lean-beam/references/lean-run-at-semantics.md#5-introducing-local-recursion-in-a-tactic-probe)
 also explains why this boundary exists and how linear handle consumption applies on failure.
 

docs/STATUS.md

@@ -126,6 +126,12 @@ handle, including when the recursion is valid in ordinary Lean. Lean checks thes
 their termination when finalizing the enclosing declaration; a tactic fragment has no such step.
 Add valid recursive definitions to the document and sync before probing their use. Command probes
 that elaborate a complete declaration use Lean's normal finalization and termination checks.
+
+For the same reason, a tactic probe whose result uses the declaration being proved, or another
+member of its `mutual` block, returns a semantic failure with the original proof state and no
+successor handle. Lean would check that reference for termination when finalizing the declaration,
+so the probe cannot tell whether the edit elaborates; this includes recursion that is valid in
+ordinary Lean. Make the edit and sync to check it.
 See the skill's [local recursion workflow](../skills/lean-beam/references/lean-run-at-semantics.md#5-introducing-local-recursion-in-a-tactic-probe)
 for saved-file validation, version updates, and handle invalidation.
 

docs/TESTING.md

@@ -97,7 +97,7 @@ Current LSP coverage includes:
 - handle API, restart, lifecycle, and nested-failure coverage in [tests/lean/BeamTest/LSP/Handle](../tests/lean/BeamTest/LSP/Handle)
 - full registered LSP request coverage through request-family tests under [tests/lean/BeamTest/LSP/Requests](../tests/lean/BeamTest/LSP/Requests), aggregated by [tests/lean/BeamTest/LSP/RequestSurfaceTest.lean](../tests/lean/BeamTest/LSP/RequestSurfaceTest.lean), including `$/lean/todo` and `$/lean/runAt` composition; the agent corpus [tests/save_olean_project/TodoAgentSmoke.lean](../tests/save_olean_project/TodoAgentSmoke.lean) pins one whole-file `todo` item per common proof mistake, with its goal, and a `runAt` solution for each at the item's position, including term placeholders and a handle continued from one
 - tactic-sequence parsing in [RunAt/BasicTest.lean](../tests/lean/BeamTest/LSP/Requests/RunAt/BasicTest.lean): newline- and `;`-separated tactics, comments and nested bullets, more-indented argument continuation, a line break that must end `intro`'s binders instead of naming one after the next tactic, the same text through a `runWith` continuation, rollback of a continuation whose second tactic fails (no successor handle; a non-linear parent stays reusable, a linear parent is consumed), and a clear error for comment-only text
-- placeholder probes in the same file: tactics at an unfilled `sorry`, `_`, or `?x` term run against its goal, with its local context and instances, from its first character through its end, inside a tactic proof as well; a hole that elaboration filled keeps the command basis, and a `?_` whose goal a later tactic solved or closed with `sorry` keeps the tactic basis; a stored handle continues goals the tactics leave; placeholder contexts with `let` values, local instances, open namespaces, local notation, and section or header universes; a local introduced by one probe visible only through its stored handle, also across concurrent probes; handles stored at a placeholder invalidated by an edit; and the documented self-reference limitation (a probe may use the declaration being proved, while later declarations stay unknown)
+- placeholder probes in the same file: tactics at an unfilled `sorry`, `_`, or `?x` term run against its goal, with its local context and instances, from its first character through its end, inside a tactic proof as well; a hole that elaboration filled keeps the command basis, and a `?_` whose goal a later tactic solved or closed with `sorry` keeps the tactic basis; a stored handle continues goals the tactics leave; placeholder contexts with `let` values, local instances, open namespaces, local notation, and section or header universes; a local introduced by one probe visible only through its stored handle, also across concurrent probes; handles stored at a placeholder invalidated by an edit; and self-reference (a probe that uses the declaration being proved reports an unchecked failure, while later declarations stay unknown)
 - auxiliary-declaration conformance in [AuxiliaryDeclarationTest.lean](../tests/lean/BeamTest/LSP/Requests/RunAt/AuxiliaryDeclarationTest.lean), comparing `runAt` with identical tactic replacements through ordinary LSP document edits, including private and nested proofs, stored-handle branches, and failure isolation
 - proof-context combinations in the same fixture: universe-polymorphic kernel `decide` and `grind`, rollback within `first`, local instances and dependent induction across handle branches, native computation, `conv` under binders, and bitvector solver success and counterexamples
 - available-goal execution in [AvailabilityTest.lean](../tests/lean/BeamTest/LSP/Requests/RunAt/AvailabilityTest.lean): a later tactic signals entry and waits on a gate; goal inspection and `runAt` must finish before that gate is released, with both synchronous and asynchronous elaboration

skills/lean-beam/references/workflow-details.md

@@ -23,8 +23,10 @@ Use this reference when the task needs more than the default loop in `SKILL.md`.
   use `exact t` for a term. Only the placeholder's type is checked, not later parts of the
   enclosing term
 - a successful probe is not proof that the edit elaborates: probes check the text against its goal
-  only and do not run Lean's termination checking, so text that uses the declaration being proved
-  can succeed; confirm with a real edit and `sync`
+  only and do not run Lean's termination checking; confirm with a real edit and `sync`
+- text that uses the declaration being proved, or another member of its `mutual` block, returns
+  `success: false` with a message naming that declaration, even when the recursion is valid; make
+  the edit and `sync` instead
 - standalone comments, blank lines, and many declaration headers often do not have a usable basis
 - nearby whitespace/comments may still work when Lean can recover a neighboring basis, but do not
   assume that from arbitrary file positions

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

@@ -446,6 +446,67 @@ def checkRunAtPlaceholders : ScenarioM Unit := do
 
   closeDoc doc
 
+/-- The position of the first `needle` on the line that starts with `linePrefix`. -/
+private def positionAt (source linePrefix needle : String) : IO Lean.Lsp.Position := do
+  let some (text, line) := source.splitOn "\n" |>.zipIdx |>.find? (·.1.startsWith linePrefix)
+    | throw <| IO.userError s!"missing fixture line {linePrefix}"
+  let some (pre :: _ :: _) := some (text.splitOn needle)
+    | throw <| IO.userError s!"missing {needle} on fixture line {linePrefix}"
+  pure { line, character := pre.length }
+
+private def selfReferenceNeedle : String :=
+  "the declaration it is inside"
+
+def checkRunAtSelfReference : ScenarioM Unit := do
+  let path := "tests/scenario/docs/RunAtSelfReference.lean"
+  let doc ← openDoc path
+  syncDoc doc
+  let source ← IO.FS.readFile path
+  let tacticSorry ← positionAt source "theorem tacticSelf" "sorry"
+  -- The probe environment already contains the declaration being proved; using it must not
+  -- report success, at a tactic position, a term `sorry`, or a term hole.
+  for (label, linePrefix, needle, text) in [
+      ("tactic self-reference", "theorem tacticSelf", "sorry", "exact tacticSelf"),
+      ("term sorry self-reference", "theorem termSelf", "sorry", "exact termSelf"),
+      ("term hole self-reference", "def holeSelf", "_", "exact holeSelf"),
+      ("mutual block reference", "  theorem mutualLeft", "sorry", "exact mutualRight")] do
+    requireRunAtFailureMessage label doc (← positionAt source linePrefix needle) text
+      selfReferenceNeedle
+  -- Valid recursion is reported as unchecked, never as a termination failure.
+  let recursiveExact ← positionAt source "  | n + 1 => by" "exact"
+  let recursive : Beam.LSP.RunAt.Result ← awaitResponseAs <| ← sendRunAt doc {
+    line := recursiveExact.line, character := recursiveExact.character, text := "exact countDown n" }
+  unless !recursive.success &&
+      recursive.messages.any (·.text.contains selfReferenceNeedle) &&
+      recursive.messages.all (fun msg =>
+        msg.severity != .error || msg.text.contains selfReferenceNeedle) do
+    throw <| IO.userError s!"recursive probe must be unchecked, not failed: {(toJson recursive).compress}"
+  -- Earlier declarations remain usable and later ones remain unknown.
+  let earlier ← requireRunAtSuccess "earlier declaration" doc tacticSorry
+    "have _h := earlierFact"
+  unless earlier.proofState?.map (·.goals.map (·.target)) == some #["False"] do
+    throw <| IO.userError s!"earlier declaration changed the goal: {(toJson earlier).compress}"
+  requireRunAtFailureMessage "later declaration" doc tacticSorry "have _h := laterFact"
+    "laterFact"
+  -- A handle continuation applies the same check and restores the stored state.
+  let initial ← requireRunAtResponseSuccess "self-reference basis" <|
+    ← sendRunAt doc {
+      line := tacticSorry.line, character := tacticSorry.character, text := "skip", storeHandle := true }
+  let some handle := initial.handle?
+    | throw <| IO.userError "missing self-reference basis handle"
+  let continued : Beam.LSP.RunAt.Result ← awaitResponseAs <|
+    ← runWithHandle doc handle { text := "exact tacticSelf", storeHandle := true }
+  unless !continued.success && continued.handle?.isNone &&
+      continued.proofState?.map (·.goals.map (·.target)) == some #["False"] &&
+      continued.messages.any (·.text.contains selfReferenceNeedle) do
+    throw <| IO.userError s!"continued self-reference must fail with the stored goal: {(toJson continued).compress}"
+  let retry ← requireRunAtResponseSuccess "reuse handle after self-reference" <|
+    ← runWithHandle doc handle { text := "skip" }
+  unless retry.proofState?.map (·.goals.map (·.target)) == some #["False"] do
+    throw <| IO.userError s!"self-reference changed the stored proof state: {(toJson retry).compress}"
+  releaseHandle doc handle
+  closeDoc doc
+
 private def placeholderContentModifiedJson : Json :=
   Json.mkObj [("code", toJson "contentModified")]
 
@@ -511,11 +572,12 @@ def checkRunAtPlaceholderContexts : ScenarioM Unit := do
       throw <| IO.userError s!"concurrent placeholder probe {i}: {(toJson result).compress}"
   requireRunAtGoals "placeholder after concurrent probes" doc letHole #["Nat"]
 
-  -- Known limitation, documented with runAt: probes do not run Lean's termination checking, so
-  -- text that uses the declaration being proved succeeds although the same edit fails. Update
-  -- these expectations when probes reject self-use. Later declarations stay unknown.
-  requireRunAtSolvesProof "self-reference at a term sorry" doc ⟨20, 28⟩ "exact termSelf"
-  requireRunAtSolvesProof "self-reference at a tactic sorry" doc ⟨21, 33⟩ "exact tacticSelf"
+  -- Probes do not run Lean's termination checking, so text that uses the declaration being proved
+  -- is reported as unchecked rather than solved. Later declarations stay unknown.
+  requireRunAtFailureMessage "self-reference at a term sorry" doc ⟨20, 28⟩ "exact termSelf"
+    selfReferenceNeedle
+  requireRunAtFailureMessage "self-reference at a tactic sorry" doc ⟨21, 33⟩ "exact tacticSelf"
+    selfReferenceNeedle
   requireRunAtFailureMessage "later declaration at a term sorry" doc ⟨20, 28⟩
     "exact tacticSelf" "tacticSelf"
 
@@ -549,6 +611,7 @@ def run : ScenarioM Unit := do
   checkRunAtTacticPositions
   checkRunAtTacticSequences
   checkRunAtPlaceholders
+  checkRunAtSelfReference
   checkRunAtPlaceholderContexts
   checkRunAtElaborationAborts
   checkRunAtResourceLimits

tests/scenario/docs/RunAtSelfReference.lean

@@ -0,0 +1,18 @@
+theorem earlierFact : True := trivial
+
+theorem tacticSelf : False := by sorry
+
+theorem termSelf : False := sorry
+
+def holeSelf : Nat := _
+
+def countDown : Nat → Nat
+  | 0 => 0
+  | n + 1 => by exact countDown n
+
+theorem laterFact : True := trivial
+
+mutual
+  theorem mutualLeft : False := by sorry
+  theorem mutualRight : False := by sorry
+end