doc: simplify the main lean-beam skill surface

Author: ejgallego

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 <path>` 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 <path>` 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 <path>` or `--text-file <path>` for the continuation text
+- `--stdin` is the normal multiline path for speculative Lean text
+- `--handle-file <path>` 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

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 <path>`;
-  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 <path>` or use `--text-file` for the
-  continuation text
+- for multiline speculative text, prefer `--stdin` as the normal path; use `--text-file <path>`
+  when the text already lives in a file
+- for handle-based continuation, prefer `--handle-file <path>` 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 <path>` 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