From ce338cdbb4ce77851f5b1d3949127c55298aab93 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 22 Mar 2026 10:54:16 +0100 Subject: [PATCH] doc: simplify the main lean-beam skill surface --- README.md | 17 +++++------------ skills/lean-beam/SKILL.md | 21 ++++++++++++--------- 2 files changed, 17 insertions(+), 21 deletions(-) diff --git a/README.md b/README.md index 7c9cb8e6..0a05051e 100644 --- a/README.md +++ b/README.md @@ -80,7 +80,6 @@ lean-beam ensure lean-beam hover "Foo.lean" 10 2 lean-beam goals-prev "Foo.lean" 10 2 lean-beam run-at "Foo.lean" 10 2 "exact trivial" -printf 'example : True := by\n trivial\n' | lean-beam run-at "Foo.lean" 10 2 --stdin lean-beam sync "MyPkg/Sub/Module.lean" lean-beam refresh "MyPkg/Sub/Module.lean" lean-beam save "MyPkg/Sub/Module.lean" @@ -96,25 +95,19 @@ Read those commands like this: Multiline and handle-oriented wrapper ergonomics: ```bash -# avoid shell-escape mistakes for multiline probe text +# for multiline probe text, prefer stdin printf 'example : True := by\n trivial\n' | lean-beam run-at "Foo.lean" 10 2 --stdin -lean-beam run-at "Foo.lean" 10 2 --text-file probe.lean -# continuation from an explicit stored handle +# for exact continuation, prefer a handle file lean-beam run-at-handle "Foo.lean" 10 2 "constructor" lean-beam run-with "Foo.lean" --handle-file handle.json "exact trivial" - -# when quoting is suspect, inspect exactly what the wrapper is sending -BEAM_DEBUG_TEXT=1 lean-beam run-at "Foo.lean" 10 2 "exact trivial" ``` Read those flags like this: -- `--stdin` and `--text-file ` avoid shell quoting fragility for text-carrying Lean probes -- `--` forces the remaining arguments to be treated as text, even if they start with `--` -- `--handle-file ` avoids inlining handle JSON for `lean-beam run-with`, `lean-beam run-with-linear`, and `lean-beam release` -- `BEAM_DEBUG_TEXT=1` prints escaped probe text and UTF-8 bytes to wrapper stderr for human debugging -- if `lean-beam run-with` or `lean-beam run-with-linear` takes the handle as `-`, stdin is already used for the handle JSON, so prefer `--handle-file ` or `--text-file ` for the continuation text +- `--stdin` is the normal multiline path for speculative Lean text +- `--handle-file ` is the normal handle path for exact continuation and release +- deeper shell-oriented variants and debugging knobs live in [skills/lean-beam/SKILL.md](skills/lean-beam/SKILL.md) and the linked reference docs When `lean-beam sync` fails with `syncBarrierIncomplete`, the JSON error may include `error.data.staleDirectDeps`, `error.data.saveDeps`, and `error.data.recoveryPlan` to suggest a diff --git a/skills/lean-beam/SKILL.md b/skills/lean-beam/SKILL.md index ed05de10..adcd90f6 100644 --- a/skills/lean-beam/SKILL.md +++ b/skills/lean-beam/SKILL.md @@ -85,12 +85,10 @@ Prefer the smallest command that matches the actual task: truly empty line only character `0` is valid - use `lean-beam run-at-handle` and then `lean-beam run-with` or `lean-beam run-with-linear` only when exact speculative continuation matters -- for multiline text-carrying Lean probes (`lean-beam run-at`, `lean-beam run-at-handle`, - `lean-beam run-with`, `lean-beam run-with-linear`), prefer `--stdin` or `--text-file `; - use `--` before text that itself starts with `--` -- when `lean-beam run-with` or `lean-beam run-with-linear` takes the handle as `-`, stdin is already - consumed by the handle json, so prefer `--handle-file ` or use `--text-file` for the - continuation text +- for multiline speculative text, prefer `--stdin` as the normal path; use `--text-file ` + when the text already lives in a file +- for handle-based continuation, prefer `--handle-file ` as the normal path; deeper shell-loop + variants such as stdin handle piping live in the reference docs - do not expect one `lean-beam run-at` call to become the basis of the next one automatically - use `lean-beam sync` right after every real saved edit before the next speculative probe - use `lean-beam save` or `lean-beam close-save` only for a synced workspace module path such as @@ -136,8 +134,6 @@ Use the right tool for each goal: - for handle-based commands, `--handle-file ` is the easiest way to avoid inlining handle json - if surface syntax depends on indentation or layout: pass the exact text you want Lean to parse, or make a real edit in the file instead of expecting the wrapper to fill whitespace for you -- if shell quoting is suspect, set `BEAM_DEBUG_TEXT=1` to print the exact escaped text and UTF-8 - bytes the wrapper is sending for text-carrying Lean probes Open [references/lean-run-at-semantics.md](references/lean-run-at-semantics.md) when the task needs concrete examples for: @@ -146,6 +142,13 @@ 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/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. @@ -209,6 +212,7 @@ lean-beam goals-prev "Foo.lean" 10 2 # try speculative Lean text without editing the file lean-beam run-at "Foo.lean" 10 2 "exact trivial" +# for multiline probes, prefer stdin printf 'example : True := by\n trivial\n' | lean-beam run-at "Foo.lean" 10 2 --stdin # after every real edit saved to disk, on that same workspace module path @@ -249,7 +253,6 @@ Surface rule: - wrapper `stderr` is the human-facing diagnostic surface - wrapper `stderr` may distinguish request-level failures from a completed request whose payload failed inside Lean; use stdout JSON for machine decisions -- `BEAM_DEBUG_TEXT=1` adds escaped text and UTF-8 byte dumps for text-carrying Lean probes on stderr - `beam-client request-stream ...` is the machine-facing streamed surface - do not parse wrapper `stderr` in tooling