fix: harden wrapper text and handle inputs

README.md

@@ -80,6 +80,7 @@ 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"
@@ -92,6 +93,29 @@ Read those commands like this:
 - `lean-beam refresh` is `lean-beam close` plus `lean-beam sync`
 - `lean-beam save` checkpoints one synced workspace module; it does not validate downstream importers
 
+Multiline and handle-oriented wrapper ergonomics:
+
+```bash
+# avoid shell-escape mistakes for multiline probe text
+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
+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
+
 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
 cheap direct-import recovery path before falling back to `lake build`.

scripts/install-beam-notes.txt

@@ -2,6 +2,8 @@
 Quick Start
   lean-beam ensure
   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
+  BEAM_DEBUG_TEXT=1 lean-beam run-at "Foo.lean" 10 2 "exact trivial"
 
 After Saving A Real Edit
   lean-beam sync "Foo.lean"
@@ -11,6 +13,7 @@ Exact Continuation
   Separate lean-beam run-at calls do not chain.
   For exact continuation from one speculative state:
   lean-beam run-at-handle "Foo.lean" 10 2 "constructor"
+  lean-beam run-with "Foo.lean" --handle-file handle.json "exact trivial"
 
 Diagnostics
   lean-beam sync / lean-beam save / lean-beam close-save stream errors by default

scripts/lean-beam

@@ -10,14 +10,14 @@ usage() {
   cat <<'EOF' >&2
 usage:
   lean-beam [--root PATH] [--socket PATH | --port N] ensure [lean|rocq]
-  lean-beam [--root PATH] [--socket PATH | --port N] run-at <path> <line> <character> <text...>
-  lean-beam [--root PATH] [--socket PATH | --port N] run-at-handle <path> <line> <character> <text...>
+  lean-beam [--root PATH] [--socket PATH | --port N] run-at <path> <line> <character> [--stdin | --text-file <path> | -- <text...> | <text...>]
+  lean-beam [--root PATH] [--socket PATH | --port N] run-at-handle <path> <line> <character> [--stdin | --text-file <path> | -- <text...> | <text...>]
   lean-beam [--root PATH] [--socket PATH | --port N] hover <path> <line> <character>
   lean-beam [--root PATH] [--socket PATH | --port N] goals-after <path> <line> <character>
   lean-beam [--root PATH] [--socket PATH | --port N] goals-prev <path> <line> <character>
-  lean-beam [--root PATH] [--socket PATH | --port N] run-with <path> <handle-json|-> <text...>
-  lean-beam [--root PATH] [--socket PATH | --port N] run-with-linear <path> <handle-json|-> <text...>
-  lean-beam [--root PATH] [--socket PATH | --port N] release <path> <handle-json|->
+  lean-beam [--root PATH] [--socket PATH | --port N] run-with <path> <handle-json|-|--handle-file <path>> [--stdin | --text-file <path> | -- <text...> | <text...>]
+  lean-beam [--root PATH] [--socket PATH | --port N] run-with-linear <path> <handle-json|-|--handle-file <path>> [--stdin | --text-file <path> | -- <text...> | <text...>]
+  lean-beam [--root PATH] [--socket PATH | --port N] release <path> <handle-json|-|--handle-file <path>>
   lean-beam [--root PATH] [--socket PATH | --port N] deps <path>
   lean-beam [--root PATH] [--socket PATH | --port N] sync <path> [+full]
   lean-beam [--root PATH] [--socket PATH | --port N] refresh <path> [+full]
@@ -37,6 +37,9 @@ usage:
 notes:
   - lean-beam keeps the Lean wrapper surface primary, but also exposes Rocq goal probes and backend selection commands
   - common Rocq entry points are `lean-beam ensure rocq`, `lean-beam doctor rocq`, `lean-beam rocq-goals-after`, and `lean-beam rocq-goals-prev`
+  - for multiline text-carrying Lean probes, prefer `--stdin` or `--text-file <path>`; use `--` before text that starts with `--`
+  - for handle-based commands, use `--handle-file <path>` when you do not want to inline handle json
+  - set `BEAM_DEBUG_TEXT=1` to print the exact escaped text and UTF-8 bytes sent for text-carrying Lean probes
 EOF
 }
 

skills/lean-beam/SKILL.md

@@ -85,6 +85,12 @@ 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
 - 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
@@ -127,8 +133,11 @@ Use the right tool for each goal:
 - if you made a real edit and want fresh file diagnostics: save the file, then use `lean-beam sync`
 - if you want exact continuation from speculative state: mint a handle with `lean-beam run-at-handle`,
   then continue with `lean-beam run-with` or `lean-beam run-with-linear`
+- 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:
@@ -200,6 +209,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"
+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
 lean-beam sync "MyPkg/Sub/Module.lean"
@@ -237,6 +247,9 @@ Diagnostic defaults on that path:
 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
 

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

@@ -98,7 +98,13 @@ If the speculative text is the version you want to keep, open
 For multi-line probes, include the actual newline characters you want Lean to parse. For example:
 
 ```bash
-# using ANSI-C shell quoting so `\n` becomes a real newline
+# piping the exact text through stdin avoids shell-escape mistakes
+printf '  first | exact h1\n  | exact h2\n' | lean-beam run-at "Foo.lean" 18 0 --stdin
+
+# or read the probe from a file
+lean-beam run-at "Foo.lean" 18 0 --text-file probe.lean
+
+# ANSI-C shell quoting also works when you do want to keep everything on one command line
 lean-beam run-at "Foo.lean" 18 0 $'  first | exact h1\n  | exact h2'
 ```
 

skills/lean-beam/references/mcts-search.md

@@ -39,8 +39,14 @@ Rules:
 lean-beam ensure
 root="$(lean-beam run-at-handle "Proofs.lean" 42 6 "constructor")"
 
-left="$(printf '%s\n' "$root" | lean-beam run-with "Proofs.lean" - "constructor")"
-right="$(printf '%s\n' "$root" | lean-beam run-with "Proofs.lean" - "aesop")"
+# writing handles to files avoids stdin conflicts in larger shell scripts
+printf '%s\n' "$root" > root.handle.json
+left="$(lean-beam run-with "Proofs.lean" --handle-file root.handle.json "constructor")"
+right="$(lean-beam run-with "Proofs.lean" --handle-file root.handle.json "aesop")"
+
+# stdin handle flow remains supported too
+left_pipe="$(printf '%s\n' "$root" | lean-beam run-with "Proofs.lean" - "constructor")"
+right_pipe="$(printf '%s\n' "$root" | lean-beam run-with "Proofs.lean" - "aesop")"
 
 printf '%s\n' "$left" | lean-beam release "Proofs.lean" -
 printf '%s\n' "$right" | lean-beam release "Proofs.lean" -
@@ -53,9 +59,18 @@ Use this when you want to explore multiple children from the same preserved basi
 ```bash
 lean-beam ensure
 root="$(lean-beam run-at-handle "Proofs.lean" 42 6 "constructor")"
-step1="$(printf '%s\n' "$root" | lean-beam run-with-linear "Proofs.lean" - "constructor")"
-step2="$(printf '%s\n' "$step1" | lean-beam run-with-linear "Proofs.lean" - "exact trivial")"
-printf '%s\n' "$step2" | lean-beam run-with-linear "Proofs.lean" - "exact trivial"
+# file-backed handles are often easier in longer shell loops
+printf '%s\n' "$root" > root.handle.json
+step1="$(lean-beam run-with-linear "Proofs.lean" --handle-file root.handle.json "constructor")"
+printf '%s\n' "$step1" > step1.handle.json
+step2="$(lean-beam run-with-linear "Proofs.lean" --handle-file step1.handle.json "exact trivial")"
+printf '%s\n' "$step2" > step2.handle.json
+lean-beam run-with-linear "Proofs.lean" --handle-file step2.handle.json "exact trivial"
+
+# stdin handle flow remains supported when you prefer pipes
+step1_pipe="$(printf '%s\n' "$root" | lean-beam run-with-linear "Proofs.lean" - "constructor")"
+step2_pipe="$(printf '%s\n' "$step1_pipe" | lean-beam run-with-linear "Proofs.lean" - "exact trivial")"
+printf '%s\n' "$step2_pipe" | lean-beam run-with-linear "Proofs.lean" - "exact trivial"
 ```
 
 Use this when you want one evolving playout path instead of a preserved branch point.

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

@@ -31,6 +31,12 @@ Use this reference when the task needs more than the default loop in `SKILL.md`.
 Continue from a stored handle:
 
 ```bash
+# `--handle-file` avoids inlining handle json and frees stdin for continuation text
+lean-beam run-with "Foo.lean" --handle-file handle.json "exact trivial"
+lean-beam run-with-linear "Foo.lean" --handle-file handle.json "exact trivial"
+lean-beam release "Foo.lean" --handle-file handle.json
+
+# stdin handle flow remains supported when it fits your shell loop better
 printf '%s\n' "$HANDLE_JSON" | lean-beam run-with "Foo.lean" - "exact trivial"
 printf '%s\n' "$HANDLE_JSON" | lean-beam run-with-linear "Foo.lean" - "exact trivial"
 printf '%s\n' "$HANDLE_JSON" | lean-beam release "Foo.lean" -
@@ -135,7 +141,6 @@ What is not a valid checkpoint target:
   `contentModified` or handle invalidation instead of hidden reuse
 - `lean-beam save` / `lean-beam close-save` checkpoint the current synced Lake module only; they do not
   rebuild reverse dependencies or make downstream files fresh by themselves
-
 ## Diagnostics, Progress, And Request IDs
 
 - `lean-beam sync`, `lean-beam save`, and `lean-beam close-save` always stream fresh diagnostics for the current