doc: clarify run-at tactic positions

Beam/LSP/RunAt.lean

@@ -51,6 +51,8 @@ Current request semantics:
 - command-mode `text` is one Lean command, not a top-level command sequence
 - proof-mode `text` is one tactic block
 - `position` uses Lean/LSP `Position` semantics against the matching document version
+- proof execution uses Lean's cursor-selected before/after tactic state; the tactic's start
+  selects its before-state, while positions inside it may select its after-state
 - positions outside the document are invalid request parameters
 - request-level failures are reported as transport errors rather than as `Result`
 -/

CHANGELOG.md

@@ -33,6 +33,9 @@ This project keeps a lightweight, reverse-chronological changelog. Dates use `YY
 
 ### Changed
 
+- Clarify zero-based `run-at` coordinates and how tactic positions select before/after proof states,
+  with guidance for probing tactic replacements
+  ([#253](https://github.com/leanprover/lean-beam/pull/253), @ejgallego).
 - Local builds now write to Lake's toolchain-scoped artifact cache and restore cached outputs into
   `.lake/build`, preserving the paths used by Beam's wrapper, installer, and tests. CI restores that
   cache for Lean jobs and lets one job per OS publish each commit's updated cache.

docs/SETUP.md

@@ -204,7 +204,9 @@ lean-beam doctor
 ```
 
 Command positions use Lean/LSP coordinates: line and character are zero-based, and character counts
-UTF-16 code units.
+UTF-16 code units. To probe a tactic replacement, select its first character after indentation
+to use its before-state. See [Position Semantics](../skills/lean-beam/references/workflow-details.md#position-semantics)
+for the argument order and a before/after example.
 
 Start one foreground owner for the wrapper session and keep it running. In another terminal or agent
 process, ask questions against saved Lean files in that project:

skills/lean-beam/SKILL.md

@@ -189,6 +189,8 @@ Prefer the smallest command that matches the actual task:
 - use `lean-beam todo` when you want actionable items in a saved file range, such as sorries, holes,
   diagnostics, code actions, or incomplete proofs
 - use `lean-beam run-at` when you want to try one speculative Lean snippet without editing the file
+- for a tactic replacement, probe at its first character after indentation to use its before-state;
+  positions inside a simple tactic can use its after-state
 - before `lean-beam run-at`, `lean-beam run-at-handle`, `lean-beam hover`,
   `lean-beam signature-help`, `lean-beam definition`, `lean-beam references`,
   `lean-beam document-symbols`, `lean-beam goals`, or `lean-beam todo`, call
@@ -270,12 +272,8 @@ concrete examples for:
 - chaining speculative state across multiple calls
 - indentation-sensitive or newline-sensitive probes on blank or layout-sensitive lines
 
-Open [references/workflow-details.md](references/workflow-details.md) when the task needs the shell-oriented
-details for:
-
-- `--text-file`, `--`, or stdin-handle piping variants
-- handle-file versus stdin-handle tradeoffs
-- debugging-oriented wrapper details instead of the normal path
+Open [references/workflow-details.md](references/workflow-details.md) for position semantics,
+text/handle input variants, and wrapper debugging.
 
 Open [references/commit-speculative.md](references/commit-speculative.md) when the task needs the
 current workflow for turning a good speculative probe into a real saved edit.

skills/lean-beam/references/lean-run-at-semantics.md

@@ -3,6 +3,8 @@
 Use this reference when a task is confused about what `lean-beam run-at` means. The short rule is:
 `lean-beam run-at` is a speculative execution probe against one explicit broker document version, not a source edit.
 
+For coordinates and tactic-state selection, see [Position Semantics](workflow-details.md#position-semantics).
+
 ## What It Is Not
 
 - it is not an edit to the file on disk

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

@@ -5,9 +5,7 @@ Use this reference when the task needs more than the default loop in `SKILL.md`.
 ## Position Semantics
 
 - `lean-beam run-at` and `lean-beam run-at-handle` take the broker document version before
-  Lean/LSP `Position` coordinates: `<version> <line> <character>`
-- the wrapper passes those coordinates through directly; they are not editor-specific line numbers,
-  byte offsets, or parser-token offsets
+  Lean/LSP `Position` coordinates: `<version> <line> <character>`; use the version from `update`
 - line `0` is the first line, and character `0` is the first UTF-16 code unit on that line
 - on a truly empty line, only character `0` is valid; character `1` is already out of range
 - on an indented blank line, either probe after the existing spaces using that exact character
@@ -18,13 +16,35 @@ Use this reference when the task needs more than the default loop in `SKILL.md`.
   execution basis there
 - valid probe positions are not arbitrary file coordinates; `lean-beam run-at` needs a command basis or
   proof/tactic snapshot at that position, or one Lean can recover from nearby syntax
-- positions inside proof bodies are the safest choice for tactic probes
+- for a tactic replacement, select its first character after indentation to use its before-state;
+  inside a simple tactic or at its end, Lean generally selects the after-state
 - 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
 - those errors do not by themselves mean the Beam daemon is unhealthy
-- known-good proof probe in this repo:
-  `lean-beam run-at "tests/interactive/proofBasisBefore.lean" <version-from-update> 2 2 "exact trivial"`
+
+For `BeamRunAtProbe.lean` containing exactly these three lines:
+
+```lean
+example (a b : Nat) (h : a = b) : 0 + a = b := by
+  simp
+  exact h
+```
+
+| Position (line, character) | Selected state | Probe `exact h` |
+| --- | --- | --- |
+| `1 2`: start of `simp` | Before `simp`: `0 + a = b` | Fails |
+| `1 3`: inside `simp` | After `simp`: `a = b` | Succeeds |
+| `2 2`: start of `exact h` | Before `exact h`: `a = b` | Succeeds |
+
+After updating the file, this replacement probe correctly returns `result.success=false`:
+
+```bash
+lean-beam run-at "BeamRunAtProbe.lean" <version-from-update> 1 2 -- "exact h"
+```
+
+Nested tactics and whitespace may select an enclosing or neighboring tactic. `goals before` and
+`goals after` inspect both sides of the selected tactic; they do not configure a later `run-at`.
 
 ## Command Details
 

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

@@ -20,6 +20,48 @@ private def invalidParamsJson : Json :=
 private def requestCancelledJson : Json :=
   Json.mkObj [("code", toJson "requestCancelled")]
 
+def checkRunAtTacticPositions : ScenarioM Unit := do
+  let doc ← openDoc "tests/scenario/docs/TacticPositionProof.lean"
+  syncDoc doc
+
+  -- At the start of simp, its replacement must handle the unsimplified goal.
+  requireRunAtFailureMessage "runAt at simp start" doc { line := 1, character := 2 }
+    "exact h" "0 + a = b"
+  let simplified ← requireRunAtSuccess "rerun simp at its start" doc
+    { line := 1, character := 2 } "simp"
+  unless simplified.proofState?.map (·.goals.map (·.target)) == some #["a = b"] do
+    throw <| IO.userError s!"simp should leave a = b, got {(toJson simplified).compress}"
+
+  -- Moving inside simp or to its end selects the state after it.
+  for character in [3, 6] do
+    requireRunAtSolvesProof "runAt inside/at end of simp" doc { line := 1, character }
+      "exact h"
+
+  -- Zero-based line 2 is exact h; its before-state already includes simp's effect.
+  requireRunAtSolvesProof "runAt at exact start" doc { line := 2, character := 2 } "exact h"
+  requireRunAtFailureMessage "simp at exact start" doc { line := 2, character := 2 }
+    "simp" "made no progress"
+  requireRunAtFailureMessage "runAt inside exact" doc { line := 2, character := 3 }
+    "exact h" "No goals to be solved"
+
+  -- Explicit goal queries expose both states without changing later probes.
+  for (useAfter, target) in [(false, "0 + a = b"), (true, "a = b")] do
+    let req ← sendGoals doc { line := 1, character := 2, useAfter }
+    let state : Beam.LSP.Lib.ProofState ← awaitResponseAs req
+    unless state.goals.map (·.target) == #[target] do
+      throw <| IO.userError s!"goals useAfter={useAfter}: expected {target}, got {(toJson state).compress}"
+  requireRunAtFailureMessage "runAt still uses simp's before-state" doc
+    { line := 1, character := 2 } "exact h" "0 + a = b"
+
+  -- A real LSP replacement agrees with the probe at the tactic's start.
+  changeDoc doc { line := 1, character := 2, delete := "simp", insert := "exact h" }
+  let diagnostics ← collectDiagnostics doc
+  unless diagnostics.diagnostics.any (fun diagnostic =>
+      diagnostic.severity? == some .error && diagnostic.range.start.line == 1 &&
+      diagnostic.message.contains "0 + a = b") do
+    throw <| IO.userError s!"expected replacement type mismatch, got {(toJson diagnostics).compress}"
+  closeDoc doc
+
 def checkRunAtOneCommandOnly : ScenarioM Unit := do
   let doc ← openDoc "tests/lean/BeamTest/Fixtures/Deps/DepA.lean"
   syncDoc doc
@@ -148,6 +190,7 @@ def checkRunAtWithStandardLspInterference : ScenarioM Unit := do
   closeDoc editDoc
 
 def run : ScenarioM Unit := do
+  checkRunAtTacticPositions
   checkRunAtOneCommandOnly
   checkRunAtTheoremSuccessOmitsSilentMessages
   checkRunAtTheoremProofFailure

tests/lsp-coverage/cases.json

@@ -1,5 +1,11 @@
 {
   "cases": [
+    {
+      "id": "runAt.tactic-position",
+      "method": "$/lean/runAt",
+      "coverage": ["tactic-position", "isolation"],
+      "pointer": "tests/lean/BeamTest/LSP/Requests/RunAt/BasicTest.lean#checkRunAtTacticPositions"
+    },
     {
       "id": "runAt.proof-isolation",
       "method": "$/lean/runAt",

tests/lsp-coverage/methods.json

@@ -7,6 +7,7 @@
       "definition": "Beam/LSP/RunAt.lean#method",
       "requiredCoverage": [
         "isolation",
+        "tactic-position",
         "single-command-limit",
         "theorem-proof-failure",
         "theorem-tactic-failure",

tests/scenario/docs/TacticPositionProof.lean

@@ -0,0 +1,3 @@
+example (a b : Nat) (h : a = b) : 0 + a = b := by
+  simp
+  exact h