From 8276f93d58022a7bcb6a71b907af9c4f88dea995 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 7 Sep 2026 15:12:28 +0200 Subject: [PATCH 1/3] doc: clarify run-at tactic positions --- Beam/LSP/RunAt.lean | 2 + docs/SETUP.md | 10 ++++- skills/lean-beam/SKILL.md | 6 +++ .../references/lean-run-at-semantics.md | 39 +++++++++++++++++ .../lean-beam/references/workflow-details.md | 3 ++ .../LSP/Requests/RunAt/BasicTest.lean | 43 +++++++++++++++++++ tests/lsp-coverage/cases.json | 6 +++ tests/lsp-coverage/methods.json | 1 + tests/scenario/docs/TacticPositionProof.lean | 3 ++ 9 files changed, 112 insertions(+), 1 deletion(-) create mode 100644 tests/scenario/docs/TacticPositionProof.lean diff --git a/Beam/LSP/RunAt.lean b/Beam/LSP/RunAt.lean index 5bb59e44..b7ac96fd 100644 --- a/Beam/LSP/RunAt.lean +++ b/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` -/ diff --git a/docs/SETUP.md b/docs/SETUP.md index 9c3b4f7d..4f1653d4 100644 --- a/docs/SETUP.md +++ b/docs/SETUP.md @@ -204,7 +204,15 @@ 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. The arguments to `run-at` are ` `; +the version precedes the coordinates. + +To try replacing an existing tactic, point to its first character after indentation. At that position, +`run-at` uses the state before the tactic. A position inside a simple tactic can select its +after-state, and the following tactic starts with the preceding tactic's effects already applied. +For example, `simp` on the second line with two leading spaces starts at `1 2`. +See the [tactic replacement example](../skills/lean-beam/references/lean-run-at-semantics.md#selecting-a-tactic-replacement-position) +for concrete before/after results. 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: diff --git a/skills/lean-beam/SKILL.md b/skills/lean-beam/SKILL.md index 510b3aea..cba587b9 100644 --- a/skills/lean-beam/SKILL.md +++ b/skills/lean-beam/SKILL.md @@ -239,6 +239,11 @@ batch-equivalence check rather than one-file probing. `lean-beam run-at` is a speculative execution request against one explicit broker document version. Read it as "try this Lean text here", not as "edit the file here". +To probe a replacement for an existing tactic, use the position of its first character after +indentation. That selects the state before the tactic. A position inside a simple tactic can select +the state after it; moving to the following line also includes earlier tactics' effects. Inspect +with `goals before` / `goals after` when needed; those queries do not change `run-at`'s selection. + What `lean-beam run-at` does not do: - it does not edit the source file or create a new on-disk baseline for the next request @@ -266,6 +271,7 @@ Use the right tool for each goal: Open [references/lean-run-at-semantics.md](references/lean-run-at-semantics.md) when the task needs concrete examples for: +- selecting the state before a tactic when probing its replacement - full-file diagnostics after a speculative probe - chaining speculative state across multiple calls - indentation-sensitive or newline-sensitive probes on blank or layout-sensitive lines diff --git a/skills/lean-beam/references/lean-run-at-semantics.md b/skills/lean-beam/references/lean-run-at-semantics.md index 9fbfa4b8..8eb82527 100644 --- a/skills/lean-beam/references/lean-run-at-semantics.md +++ b/skills/lean-beam/references/lean-run-at-semantics.md @@ -3,6 +3,45 @@ 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. +## Selecting A Tactic Replacement Position + +The wrapper takes ` `. Both coordinates are zero-based; the +version is the value returned by `lean-beam update`. + +For `BeamRunAtProbe.lean` containing exactly these three lines: + +```lean +example (a b : Nat) (h : a = b) : 0 + a = b := by + simp + exact h +``` + +The start of `simp` is line `1`, character `2`. After updating the file, use that position to +test replacing `simp`: + +```bash +lean-beam run-at "BeamRunAtProbe.lean" 1 2 -- "exact h" +``` + +This returns `result.success=false`: `h : a = b` does not solve `0 + a = b`. +The same probe at `2 2` succeeds because that is the start of `exact h`, after `simp` has already +simplified the goal. + +| 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 | + +`run-at` follows Lean's cursor-based tactic selection. At a tactic's first character it uses the +before-state; inside a simple tactic or at its end it generally uses the after-state. Nested +tactics and nearby whitespace can select a different enclosing or neighboring tactic, so choose +the start of the specific tactic you intend to replace. + +`goals before` and `goals after` inspect both sides of the selected tactic. They do not configure +the state used by a later `run-at`. After applying a replacement to the saved file, use +`lean-beam sync` to check the resulting file, including later proof steps. + ## What It Is Not - it is not an edit to the file on disk diff --git a/skills/lean-beam/references/workflow-details.md b/skills/lean-beam/references/workflow-details.md index 7c8430d3..4c579039 100644 --- a/skills/lean-beam/references/workflow-details.md +++ b/skills/lean-beam/references/workflow-details.md @@ -19,6 +19,9 @@ Use this reference when the task needs more than the default loop in `SKILL.md`. - 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 the tactic's first character after indentation; positions inside + a simple tactic may use its after-state. See the + [replacement-position example](lean-run-at-semantics.md#selecting-a-tactic-replacement-position) - 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 diff --git a/tests/lean/BeamTest/LSP/Requests/RunAt/BasicTest.lean b/tests/lean/BeamTest/LSP/Requests/RunAt/BasicTest.lean index 06d79ea0..650a49b4 100644 --- a/tests/lean/BeamTest/LSP/Requests/RunAt/BasicTest.lean +++ b/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 diff --git a/tests/lsp-coverage/cases.json b/tests/lsp-coverage/cases.json index 757767d6..7da13b6e 100644 --- a/tests/lsp-coverage/cases.json +++ b/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", diff --git a/tests/lsp-coverage/methods.json b/tests/lsp-coverage/methods.json index 2e49c6de..423380f9 100644 --- a/tests/lsp-coverage/methods.json +++ b/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", diff --git a/tests/scenario/docs/TacticPositionProof.lean b/tests/scenario/docs/TacticPositionProof.lean new file mode 100644 index 00000000..9869abee --- /dev/null +++ b/tests/scenario/docs/TacticPositionProof.lean @@ -0,0 +1,3 @@ +example (a b : Nat) (h : a = b) : 0 + a = b := by + simp + exact h From 02901b9500e38e740c0529d237b7ee11266004da Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 7 Sep 2026 15:15:31 +0200 Subject: [PATCH 2/3] doc: record tactic position guidance in changelog --- CHANGELOG.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index e4b124b2..4fcacd4e 100644 --- a/CHANGELOG.md +++ b/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. From df47386ee71d1bfb5b30ef86e2806102dbae5c0a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 7 Sep 2026 15:47:09 +0200 Subject: [PATCH 3/3] doc: consolidate tactic position guidance Thanks to Bas Spitters (@spitters) for the clear report and reproducer in #239. --- docs/SETUP.md | 12 ++---- skills/lean-beam/SKILL.md | 16 ++------ .../references/lean-run-at-semantics.md | 39 +------------------ .../lean-beam/references/workflow-details.md | 35 ++++++++++++----- 4 files changed, 34 insertions(+), 68 deletions(-) diff --git a/docs/SETUP.md b/docs/SETUP.md index 4f1653d4..627df973 100644 --- a/docs/SETUP.md +++ b/docs/SETUP.md @@ -204,15 +204,9 @@ lean-beam doctor ``` Command positions use Lean/LSP coordinates: line and character are zero-based, and character counts -UTF-16 code units. The arguments to `run-at` are ` `; -the version precedes the coordinates. - -To try replacing an existing tactic, point to its first character after indentation. At that position, -`run-at` uses the state before the tactic. A position inside a simple tactic can select its -after-state, and the following tactic starts with the preceding tactic's effects already applied. -For example, `simp` on the second line with two leading spaces starts at `1 2`. -See the [tactic replacement example](../skills/lean-beam/references/lean-run-at-semantics.md#selecting-a-tactic-replacement-position) -for concrete before/after results. +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: diff --git a/skills/lean-beam/SKILL.md b/skills/lean-beam/SKILL.md index cba587b9..f3be1b63 100644 --- a/skills/lean-beam/SKILL.md +++ b/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 @@ -239,11 +241,6 @@ batch-equivalence check rather than one-file probing. `lean-beam run-at` is a speculative execution request against one explicit broker document version. Read it as "try this Lean text here", not as "edit the file here". -To probe a replacement for an existing tactic, use the position of its first character after -indentation. That selects the state before the tactic. A position inside a simple tactic can select -the state after it; moving to the following line also includes earlier tactics' effects. Inspect -with `goals before` / `goals after` when needed; those queries do not change `run-at`'s selection. - What `lean-beam run-at` does not do: - it does not edit the source file or create a new on-disk baseline for the next request @@ -271,17 +268,12 @@ Use the right tool for each goal: Open [references/lean-run-at-semantics.md](references/lean-run-at-semantics.md) when the task needs concrete examples for: -- selecting the state before a tactic when probing its replacement - full-file diagnostics after a speculative probe - 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. diff --git a/skills/lean-beam/references/lean-run-at-semantics.md b/skills/lean-beam/references/lean-run-at-semantics.md index 8eb82527..b5b8713f 100644 --- a/skills/lean-beam/references/lean-run-at-semantics.md +++ b/skills/lean-beam/references/lean-run-at-semantics.md @@ -3,44 +3,7 @@ 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. -## Selecting A Tactic Replacement Position - -The wrapper takes ` `. Both coordinates are zero-based; the -version is the value returned by `lean-beam update`. - -For `BeamRunAtProbe.lean` containing exactly these three lines: - -```lean -example (a b : Nat) (h : a = b) : 0 + a = b := by - simp - exact h -``` - -The start of `simp` is line `1`, character `2`. After updating the file, use that position to -test replacing `simp`: - -```bash -lean-beam run-at "BeamRunAtProbe.lean" 1 2 -- "exact h" -``` - -This returns `result.success=false`: `h : a = b` does not solve `0 + a = b`. -The same probe at `2 2` succeeds because that is the start of `exact h`, after `simp` has already -simplified the goal. - -| 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 | - -`run-at` follows Lean's cursor-based tactic selection. At a tactic's first character it uses the -before-state; inside a simple tactic or at its end it generally uses the after-state. Nested -tactics and nearby whitespace can select a different enclosing or neighboring tactic, so choose -the start of the specific tactic you intend to replace. - -`goals before` and `goals after` inspect both sides of the selected tactic. They do not configure -the state used by a later `run-at`. After applying a replacement to the saved file, use -`lean-beam sync` to check the resulting file, including later proof steps. +For coordinates and tactic-state selection, see [Position Semantics](workflow-details.md#position-semantics). ## What It Is Not diff --git a/skills/lean-beam/references/workflow-details.md b/skills/lean-beam/references/workflow-details.md index 4c579039..174c2a96 100644 --- a/skills/lean-beam/references/workflow-details.md +++ b/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: ` ` -- the wrapper passes those coordinates through directly; they are not editor-specific line numbers, - byte offsets, or parser-token offsets + Lean/LSP `Position` coordinates: ` `; 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,16 +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 the tactic's first character after indentation; positions inside - a simple tactic may use its after-state. See the - [replacement-position example](lean-run-at-semantics.md#selecting-a-tactic-replacement-position) +- 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" 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" 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