From b3992e76e85dc9f80210264438d43d7737383311 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <emilio@lean-fro.org>
Date: Mon, 16 Mar 2026 16:27:48 +0100
Subject: [PATCH 1/6] Unify Rocq CI opam setup

---
 README.md                       |  1 +
 docs/DEVELOPMENT.md             |  1 +
 docs/TESTING.md                 |  2 ++
 tests/setup-rocq-opam.sh        | 12 +++++++++---
 tests/test-beam-wrapper-rocq.sh | 33 ++++++++++++++++++++++++++++-----
 tests/test-broker-fast.sh       |  1 -
 tests/test-broker-rocq.sh       | 20 +++++---------------
 7 files changed, 46 insertions(+), 24 deletions(-)

diff --git a/README.md b/README.md
index cc0a3717..2f45f444 100644
--- a/README.md
+++ b/README.md
@@ -135,6 +135,7 @@ Broker and wrapper suites:
 ```bash
 bash tests/test-broker-fast.sh
 bash tests/test-broker-slow.sh
+bash tests/test-broker-rocq.sh
 bash tests/test-broker.sh
 bash scripts/lint-shell.sh
 ```
diff --git a/docs/DEVELOPMENT.md b/docs/DEVELOPMENT.md
index 0679dbf9..3a01bbff 100644
--- a/docs/DEVELOPMENT.md
+++ b/docs/DEVELOPMENT.md
@@ -70,6 +70,7 @@ Preferred maintainer entrypoints:
 
 - broker protocol / stream / barrier changes: `bash tests/test-broker-fast.sh`
 - wrapper / install / bundle-resolution changes: `bash tests/test-broker-slow.sh`
+- Rocq broker / wrapper changes: `bash tests/test-broker-rocq.sh`
 - risky local install or wrapper validation: `bash scripts/validate-defensive.sh`
 - shell changes: `bash scripts/lint-shell.sh`
 
diff --git a/docs/TESTING.md b/docs/TESTING.md
index 99503e89..c3b51e08 100644
--- a/docs/TESTING.md
+++ b/docs/TESTING.md
@@ -95,6 +95,8 @@ correctness regression, not yet a performance benchmark.
   and request-stream contract changes; this is the quickest broker signal
 - add [tests/test-broker-slow.sh](../tests/test-broker-slow.sh) when the change touches wrapper,
   install, or bundle-resolution behavior
+- use [tests/test-broker-rocq.sh](../tests/test-broker-rocq.sh) for Rocq broker and wrapper
+  coverage, including project-local `coq-lsp` discovery
 - use [tests/test-broker.sh](../tests/test-broker.sh) to execute both suites together before
   landing a broader broker-facing change
 - use [scripts/lint-shell.sh](../scripts/lint-shell.sh) when you change shell wrappers, installer,
diff --git a/tests/setup-rocq-opam.sh b/tests/setup-rocq-opam.sh
index 6a047d7c..390d56a4 100755
--- a/tests/setup-rocq-opam.sh
+++ b/tests/setup-rocq-opam.sh
@@ -8,11 +8,17 @@ set -euo pipefail
 
 cd "$(dirname "$0")/.."
 
-if [ ! -d "_opam/_opam" ]; then
-  opam switch create ./_opam 4.14.2
+if ! command -v opam > /dev/null 2>&1; then
+  echo "missing opam; install it first or run under ocaml/setup-ocaml" >&2
+  exit 1
 fi
 
-eval "$(opam env --switch=./_opam --set-switch)"
+if ! opam switch show > /dev/null 2>&1; then
+  echo "missing active opam switch; run under ocaml/setup-ocaml or select a switch first" >&2
+  exit 1
+fi
+
+eval "$(opam env)"
 
 if ! opam repo list --short | grep -qx 'coq-released'; then
   opam repo add coq-released https://coq.inria.fr/opam/released
diff --git a/tests/test-beam-wrapper-rocq.sh b/tests/test-beam-wrapper-rocq.sh
index 10675dde..7363eaff 100755
--- a/tests/test-beam-wrapper-rocq.sh
+++ b/tests/test-beam-wrapper-rocq.sh
@@ -10,6 +10,7 @@ cd "$(dirname "$0")/.."
 
 beam_script="$PWD/scripts/lean-beam"
 rocq_cmd="${BEAM_ROCQ_CMD:-}"
+path_rocq_cmd=""
 
 if [ ! -x "$beam_script" ]; then
   echo "missing lean-beam wrapper at $beam_script" >&2
@@ -17,7 +18,11 @@ if [ ! -x "$beam_script" ]; then
 fi
 
 if [ -z "$rocq_cmd" ]; then
-  echo "missing BEAM_ROCQ_CMD for Rocq wrapper test" >&2
+  path_rocq_cmd="$(command -v coq-lsp || true)"
+fi
+
+if [ -z "$rocq_cmd" ] && [ -z "$path_rocq_cmd" ]; then
+  echo "missing coq-lsp; set BEAM_ROCQ_CMD or install it in PATH" >&2
   exit 1
 fi
 
@@ -42,7 +47,11 @@ remove_owned_tmp_tree() {
 
 cleanup() {
   if [ -d "$tmp_repo/tests/rocq/Minimal" ]; then
-    BEAM_ROCQ_CMD="$rocq_cmd" "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" shutdown > /dev/null 2>&1 || true
+    if [ -n "$rocq_cmd" ]; then
+      BEAM_ROCQ_CMD="$rocq_cmd" "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" shutdown > /dev/null 2>&1 || true
+    else
+      "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" shutdown > /dev/null 2>&1 || true
+    fi
   fi
   remove_owned_tmp_tree "$tmp_repo"
 }
@@ -62,15 +71,29 @@ rsync -a \
     echo "expected lake build beam-cli not to prebuild Beam daemon helper executables" >&2
     exit 1
   fi
-  BEAM_ROCQ_CMD="$rocq_cmd" "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" doctor rocq > /dev/null
+  if [ -n "$rocq_cmd" ]; then
+    BEAM_ROCQ_CMD="$rocq_cmd" "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" doctor rocq > /dev/null
+  else
+    mkdir -p "$tmp_repo/tests/rocq/Minimal/_opam/bin"
+    ln -sf "$path_rocq_cmd" "$tmp_repo/tests/rocq/Minimal/_opam/bin/coq-lsp"
+    "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" doctor rocq > /dev/null
+  fi
   if [ -x ".lake/build/bin/beam-daemon" ] || [ -x ".lake/build/bin/beam-client" ]; then
     echo "expected doctor rocq to remain read-only and not build Beam daemon helpers" >&2
     exit 1
   fi
-  BEAM_ROCQ_CMD="$rocq_cmd" "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" ensure rocq > /dev/null
+  if [ -n "$rocq_cmd" ]; then
+    BEAM_ROCQ_CMD="$rocq_cmd" "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" ensure rocq > /dev/null
+  else
+    "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" ensure rocq > /dev/null
+  fi
   if [ ! -x ".lake/build/bin/beam-daemon" ] || [ ! -x ".lake/build/bin/beam-client" ]; then
     echo "expected rocq CLI startup to build missing Beam daemon helpers on demand" >&2
     exit 1
   fi
-  BEAM_ROCQ_CMD="$rocq_cmd" "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" shutdown > /dev/null
+  if [ -n "$rocq_cmd" ]; then
+    BEAM_ROCQ_CMD="$rocq_cmd" "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" shutdown > /dev/null
+  else
+    "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" shutdown > /dev/null
+  fi
 )
diff --git a/tests/test-broker-fast.sh b/tests/test-broker-fast.sh
index 65ac10ee..f3e5621b 100644
--- a/tests/test-broker-fast.sh
+++ b/tests/test-broker-fast.sh
@@ -17,7 +17,6 @@ lake build \
   beam-daemon-smoke-test \
   beam-daemon-save-stream-test \
   beam-daemon-request-stream-test \
-  beam-daemon-rocq-smoke-test \
   > /dev/null
 
 .lake/build/bin/beam-daemon-smoke-test > /dev/null
diff --git a/tests/test-broker-rocq.sh b/tests/test-broker-rocq.sh
index f532f7f7..4417bd92 100644
--- a/tests/test-broker-rocq.sh
+++ b/tests/test-broker-rocq.sh
@@ -16,25 +16,15 @@ lake build \
   beam-daemon-rocq-smoke-test \
   > /dev/null
 
-ROCQ_LSP=""
-for candidate in "_opam/bin/coq-lsp" "_opam/_opam/bin/coq-lsp"; do
-  if [ -x "$candidate" ]; then
-    ROCQ_LSP="$candidate"
-    break
-  fi
-done
-
-if [ -z "$ROCQ_LSP" ]; then
+eval "$(opam env)"
+
+if ! command -v coq-lsp > /dev/null 2>&1; then
   echo "missing coq-lsp; run tests/setup-rocq-opam.sh first" >&2
   exit 1
 fi
 
-if [ -d "_opam/_opam" ]; then
-  eval "$(opam env --switch=./_opam --set-switch)"
-fi
-
 echo "[broker-rocq] wrapper tests"
-BEAM_ROCQ_CMD="$PWD/$ROCQ_LSP" bash tests/test-beam-wrapper-rocq.sh > /dev/null
+bash tests/test-beam-wrapper-rocq.sh > /dev/null
 
 echo "[broker-rocq] smoke test"
-BEAM_ROCQ_CMD="$PWD/$ROCQ_LSP" .lake/build/bin/beam-daemon-rocq-smoke-test > /dev/null
+.lake/build/bin/beam-daemon-rocq-smoke-test > /dev/null

From dc608f09245d46a1815276ae324f4fd5cbed1496 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <emilio@lean-fro.org>
Date: Mon, 16 Mar 2026 16:36:24 +0100
Subject: [PATCH 2/6] Cache Rocq CI dependencies via setup-ocaml

---
 .github/workflows/ci.yml | 8 ++++++--
 tests/rocq-ci.opam       | 9 +++++++++
 tests/setup-rocq-opam.sh | 2 +-
 3 files changed, 16 insertions(+), 3 deletions(-)
 create mode 100644 tests/rocq-ci.opam

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 2a38b422..f397a9bb 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -97,9 +97,13 @@ jobs:
         uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: 4.14.2
+          opam-repositories: |
+            default: git+https://github.com/ocaml/opam-repository.git
+            coq-released: https://coq.inria.fr/opam/released
+          opam-local-packages: tests/rocq-ci.opam
 
-      - name: Install Rocq Tooling
-        run: bash tests/setup-rocq-opam.sh
+      - name: Install Rocq CI Dependencies
+        run: opam install -y ./tests/rocq-ci.opam --deps-only
 
       - name: Broker Rocq Test
         run: bash tests/test-broker-rocq.sh
diff --git a/tests/rocq-ci.opam b/tests/rocq-ci.opam
new file mode 100644
index 00000000..941e462e
--- /dev/null
+++ b/tests/rocq-ci.opam
@@ -0,0 +1,9 @@
+opam-version: "2.0"
+synopsis: "CI-only Rocq dependencies for lean-beam broker tests"
+maintainer: "Emilio J. Gallego Arias"
+license: "Apache-2.0"
+depends: [
+  "rocq-core" {= "9.1.1"}
+  "rocq-stdlib"
+  "coq-lsp" {= "0.2.5+9.1"}
+]
diff --git a/tests/setup-rocq-opam.sh b/tests/setup-rocq-opam.sh
index 390d56a4..98ce3d8f 100755
--- a/tests/setup-rocq-opam.sh
+++ b/tests/setup-rocq-opam.sh
@@ -26,4 +26,4 @@ fi
 
 opam update
 
-opam install -y rocq-core.9.1.1 rocq-stdlib coq-lsp.0.2.5+9.1
+opam install -y ./tests/rocq-ci.opam --deps-only

From 9fffc13275c7f40406e6a14835885c5bbee20f14 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <emilio@lean-fro.org>
Date: Mon, 16 Mar 2026 16:47:04 +0100
Subject: [PATCH 3/6] Add PATH fallback for Rocq LSP

---
 Beam/Cli.lean                   | 8 +++++++-
 docs/TESTING.md                 | 2 +-
 tests/test-beam-wrapper-rocq.sh | 9 +--------
 3 files changed, 9 insertions(+), 10 deletions(-)

diff --git a/Beam/Cli.lean b/Beam/Cli.lean
index e32b2423..e54339e2 100644
--- a/Beam/Cli.lean
+++ b/Beam/Cli.lean
@@ -636,13 +636,19 @@ private def leanBin (root : System.FilePath) : IO String := do
 private def rocqCandidates (root : System.FilePath) : List System.FilePath :=
   [root / "_opam" / "bin" / "coq-lsp", root / "_opam" / "_opam" / "bin" / "coq-lsp"]
 
+private def pathCmd? (cmd : String) : IO (Option String) := do
+  try
+    return some (← readCmdTrim "sh" #["-c", s!"command -v {shellQuote cmd}"])
+  catch _ =>
+    return none
+
 private def maybeRocqCmd (root : System.FilePath) : IO (Option String) := do
   for candidate in rocqCandidates root do
     if ← candidate.pathExists then
       return some candidate.toString
   match ← IO.getEnv "BEAM_ROCQ_CMD" with
   | some cmd => pure (some cmd)
-  | none => pure none
+  | none => pathCmd? "coq-lsp"
 
 private def rocqCmd (root : System.FilePath) : IO String := do
   match ← maybeRocqCmd root with
diff --git a/docs/TESTING.md b/docs/TESTING.md
index c3b51e08..e6fdb126 100644
--- a/docs/TESTING.md
+++ b/docs/TESTING.md
@@ -96,7 +96,7 @@ correctness regression, not yet a performance benchmark.
 - add [tests/test-broker-slow.sh](../tests/test-broker-slow.sh) when the change touches wrapper,
   install, or bundle-resolution behavior
 - use [tests/test-broker-rocq.sh](../tests/test-broker-rocq.sh) for Rocq broker and wrapper
-  coverage, including project-local `coq-lsp` discovery
+  coverage, including `coq-lsp` discovery from project-local `_opam` roots and the active PATH
 - use [tests/test-broker.sh](../tests/test-broker.sh) to execute both suites together before
   landing a broader broker-facing change
 - use [scripts/lint-shell.sh](../scripts/lint-shell.sh) when you change shell wrappers, installer,
diff --git a/tests/test-beam-wrapper-rocq.sh b/tests/test-beam-wrapper-rocq.sh
index 7363eaff..ce500010 100755
--- a/tests/test-beam-wrapper-rocq.sh
+++ b/tests/test-beam-wrapper-rocq.sh
@@ -10,18 +10,13 @@ cd "$(dirname "$0")/.."
 
 beam_script="$PWD/scripts/lean-beam"
 rocq_cmd="${BEAM_ROCQ_CMD:-}"
-path_rocq_cmd=""
 
 if [ ! -x "$beam_script" ]; then
   echo "missing lean-beam wrapper at $beam_script" >&2
   exit 1
 fi
 
-if [ -z "$rocq_cmd" ]; then
-  path_rocq_cmd="$(command -v coq-lsp || true)"
-fi
-
-if [ -z "$rocq_cmd" ] && [ -z "$path_rocq_cmd" ]; then
+if [ -z "$rocq_cmd" ] && ! command -v coq-lsp > /dev/null 2>&1; then
   echo "missing coq-lsp; set BEAM_ROCQ_CMD or install it in PATH" >&2
   exit 1
 fi
@@ -74,8 +69,6 @@ rsync -a \
   if [ -n "$rocq_cmd" ]; then
     BEAM_ROCQ_CMD="$rocq_cmd" "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" doctor rocq > /dev/null
   else
-    mkdir -p "$tmp_repo/tests/rocq/Minimal/_opam/bin"
-    ln -sf "$path_rocq_cmd" "$tmp_repo/tests/rocq/Minimal/_opam/bin/coq-lsp"
     "$tmp_repo/scripts/lean-beam" --root "$tmp_repo/tests/rocq/Minimal" doctor rocq > /dev/null
   fi
   if [ -x ".lake/build/bin/beam-daemon" ] || [ -x ".lake/build/bin/beam-client" ]; then

From fbf8036f3be59ff17e72d60cc46e5f264fc269b9 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <emilio@lean-fro.org>
Date: Mon, 16 Mar 2026 16:54:26 +0100
Subject: [PATCH 4/6] Enable dune cache for Rocq CI

---
 .github/workflows/ci.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index f397a9bb..cb64ab6e 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -97,6 +97,7 @@ jobs:
         uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: 4.14.2
+          dune-cache: true
           opam-repositories: |
             default: git+https://github.com/ocaml/opam-repository.git
             coq-released: https://coq.inria.fr/opam/released

From 75889f624be4510e9cd9faf8214b811abab2cf4a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <emilio@lean-fro.org>
Date: Mon, 16 Mar 2026 17:32:40 +0100
Subject: [PATCH 5/6] docs: tighten lean workflow details

---
 .../lean-beam/references/workflow-details.md  | 138 +++++++++---------
 1 file changed, 70 insertions(+), 68 deletions(-)

diff --git a/skills/lean-beam/references/workflow-details.md b/skills/lean-beam/references/workflow-details.md
index 217a9e9c..0289bb44 100644
--- a/skills/lean-beam/references/workflow-details.md
+++ b/skills/lean-beam/references/workflow-details.md
@@ -26,24 +26,50 @@ Use this reference when the task needs more than the default loop in `SKILL.md`.
 - known-good proof probe in this repo:
   `lean-beam run-at "tests/interactive/proofBasisBefore.lean" 2 2 "exact trivial"`
 
-## Command Details
-
-Continue from a stored handle:
-
-```bash
-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" -
-```
+## Source-File And Execution Model
 
-Short search helper:
+- `lean-beam run-at` and `lean-beam deps` do not edit `Foo.lean`
+- `lean-beam hover` is the stable read-only semantic inspection command for an existing position
+- `lean-beam goals-prev` and `lean-beam goals-after` are the stable read-only proof-state
+  inspection commands for an existing tactic position
+- `lean-beam goals-prev` / `lean-beam goals-after` return `result.goals`, not speculative execution output,
+  and do not accept speculative text
+- `beam` only sees the on-disk file, not unsaved editor buffers
+- actual source edits happen through the normal file-edit workflow
+- after every real source edit to a Lean file, save the file in the normal editor/file sense and
+  then run `lean-beam sync "Foo.lean"`
+- use `lean-beam refresh "Foo.lean"` when a tracked file needs `lean-beam close` plus `lean-beam sync`
+  as one step, especially after saving an upstream dependency
+- treat `lean-beam sync` as the explicit supported boundary between real file edits and Beam daemon
+  session state
+- `lean-beam sync` returns compact JSON on stdout, including final `result.errorCount` /
+  `result.warningCount`, and streams human diagnostics on stderr
+- if imported targets are stale or the Lean worker cannot finish that diagnostics barrier,
+  `lean-beam sync` fails; do not treat a failed sync as safe to follow with `lean-beam save`
+- `lean-beam sync` keeps machine-readable JSON on stdout; interactive progress text goes to stderr
+- every `lean-beam run-at` request is an isolated read-only probe against one on-disk document
+  version
+- `lean-beam run-at-handle` is the same style of isolated probe, but asks Lean to retain follow-up
+  state
+- `lean-beam run-with` preserves the current handle and branches from it
+- `lean-beam run-with-linear` consumes the current handle and returns a successor handle for linear
+  continuation
+- `lean-beam release` explicitly drops a preserved handle
+- `lean-beam-search` is a small convenience wrapper around these same commands
+- the request may wait for the Lean snapshot at the requested position to finish elaborating; this
+  is normal
+- the probe does not mutate the document's real elaboration state and does not create hidden state
+  for the next probe
+- the Beam daemon may implicitly open or resync the file from disk before a probe, but that is not
+  the supported readiness barrier after edits
+- use `lean-beam sync` when the workflow needs an explicit ready/fresh boundary; `lean-beam run-at` only
+  waits for the snapshot it needs
+- if the same document changes while a request or stored handle is pending, expect
+  `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
 
-```bash
-lean-beam-search mint "Foo.lean" 10 2 "constructor"
-printf '%s\n' "$HANDLE_JSON" | lean-beam-search branch "Foo.lean" "constructor"
-printf '%s\n' "$HANDLE_JSON" | lean-beam-search playout "Foo.lean" "exact trivial" "exact trivial"
-printf '%s\n' "$HANDLE_JSON" | lean-beam-search release "Foo.lean"
-```
+## Command Details
 
 Inspect dependency order for multi-file edits:
 
@@ -78,6 +104,23 @@ These commands require a synced file that belongs to the current Lake workspace
 module in the package graph. A standalone `.lean` file that the daemon can open but Lake cannot map
 to a module is a valid `lean-beam sync` target, but not a valid `lean-beam save` target.
 
+Continue from a stored handle:
+
+```bash
+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" -
+```
+
+Short search helper:
+
+```bash
+lean-beam-search mint "Foo.lean" 10 2 "constructor"
+printf '%s\n' "$HANDLE_JSON" | lean-beam-search branch "Foo.lean" "constructor"
+printf '%s\n' "$HANDLE_JSON" | lean-beam-search playout "Foo.lean" "exact trivial" "exact trivial"
+printf '%s\n' "$HANDLE_JSON" | lean-beam-search release "Foo.lean"
+```
+
 ## Save Eligibility
 
 When `lean-beam save` is valid:
@@ -93,60 +136,18 @@ What is not a valid checkpoint target:
 - a standalone `.lean` file at repo root that is outside the package module graph
 - any file the daemon can open but Lake cannot map to a workspace module
 
-## Source-File And Execution Model
-
-- `lean-beam run-at` and `lean-beam deps` do not edit `Foo.lean`
-- `lean-beam hover` is the stable read-only semantic inspection command for an existing position
-- `lean-beam goals-prev` and `lean-beam goals-after` are the stable read-only proof-state
-  inspection commands for an existing tactic position
-- `lean-beam goals-prev` / `lean-beam goals-after` return `result.goals`, not speculative execution output,
-  and do not accept speculative text
-- `beam` only sees the on-disk file, not unsaved editor buffers
-- actual source edits happen through the normal file-edit workflow
-- after every real source edit to a Lean file, save the file in the normal editor/file sense and
-  then run `lean-beam sync "Foo.lean"`
-- use `lean-beam refresh "Foo.lean"` when a tracked file needs `lean-beam close` plus `lean-beam sync`
-  as one step, especially after saving an upstream dependency
-- treat `lean-beam sync` as the explicit supported boundary between real file edits and Beam daemon
-  session state
-- `lean-beam sync` returns compact JSON on stdout, including final `result.errorCount` /
-  `result.warningCount`, and streams human diagnostics on stderr
-- if imported targets are stale or the Lean worker cannot finish that diagnostics barrier,
-  `lean-beam sync` fails; do not treat a failed sync as safe to follow with `lean-beam save`
-- `lean-beam sync` keeps machine-readable JSON on stdout; interactive progress text goes to stderr
-- every `lean-beam run-at` request is an isolated read-only probe against one on-disk document
-  version
-- `lean-beam run-at-handle` is the same style of isolated probe, but asks Lean to retain follow-up
-  state
-- `lean-beam run-with` preserves the current handle and branches from it
-- `lean-beam run-with-linear` consumes the current handle and returns a successor handle for linear
-  continuation
-- `lean-beam release` explicitly drops a preserved handle
-- `lean-beam-search` is a small convenience wrapper around these same commands
-- the request may wait for the Lean snapshot at the requested position to finish elaborating; this
-  is normal
-- the probe does not mutate the document's real elaboration state and does not create hidden state
-  for the next probe
-- the Beam daemon may implicitly open or resync the file from disk before a probe, but that is not
-  the supported readiness barrier after edits
-- use `lean-beam sync` when the workflow needs an explicit ready/fresh boundary; `lean-beam run-at` only
-  waits for the snapshot it needs
-- if the same document changes while a request or stored handle is pending, expect
-  `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
-  request
+- `lean-beam sync`, `lean-beam refresh`, `lean-beam save`, and `lean-beam close-save` always stream fresh
+  diagnostics for the current request
 - by default they stream only errors
 - add `+full` to widen the current request to warnings, info, and hints
 - the final JSON does not replay streamed diagnostics
 - when `lean-beam save` or `lean-beam close-save` returns `invalidParams` for document errors, the transport
   `error.message` includes a compact preview of underlying diagnostics and/or command messages
 - wrapper `stderr` is the human-facing diagnostic surface
-- `beam-client request-stream ...` is the machine-facing streamed surface
+- for lower-level machine-facing streamed integration, `beam-client request-stream ...` exposes the raw
+  stream
 - do not parse wrapper `stderr` in tooling
 - `BEAM_PROGRESS` controls stderr progress output for slow calls
 - by default, progress prints when stderr is a TTY
@@ -155,7 +156,7 @@ What is not a valid checkpoint target:
 - the final stdout JSON echoes it as `clientRequestId`
 - streamed stderr progress/diagnostic lines are annotated as `beam[<id>]: ...`
 - a second live request using the same id is rejected with `invalidParams`
-- `beam cancel <id>` cancels an in-flight broker request by that `clientRequestId`
+- `lean-beam cancel <id>` cancels an in-flight broker request by that `clientRequestId`
 - when `BEAM_REQUEST_ID` is set, `Ctrl-C` asks the broker to cancel that request before the local
   CLI exits
 
@@ -176,9 +177,10 @@ Interpretation:
 
 - after `lean-beam sync`, expect top-level `fileProgress.done = true`
 - successful `lean-beam sync` transport does not mean the file is error-free; inspect
-  `result.errorCount` / `result.warningCount` for fresh streamed diagnostics in this request, and
-  inspect `result.saveReady` plus `result.stateErrorCount` / `result.stateCommandErrorCount` for
-  current save-readiness
+  `result.errorCount` for fresh streamed diagnostics in this request, and inspect `result.saveReady`
+  plus `result.stateErrorCount` / `result.stateCommandErrorCount` for current save-readiness
+- inspect `result.warningCount` only when the current request used `+full`; without `+full`, that
+  field may still be `0` even when the file has warnings
 - if `lean-beam sync` fails with an incomplete diagnostics barrier, inspect the JSON
   `error.data.staleDirectDeps`, `error.data.saveDeps`, and `error.data.recoveryPlan`; those hints are
   based on direct imports whose saved checkpoint is newer than the target file's last successful
@@ -274,8 +276,8 @@ lean-beam reset-stats
 along with `saved` / `notSaved`, direct Lean deps when available, whether the current synced version
 has been checkpointed with `lean-beam save`, and Lean save preflight fields `saveEligible`,
 `saveReason`, and, when applicable, `saveModule`. For files the Beam daemon already knows about, the
-wrapper checks that status incrementally against the current on-disk text, and `open-files` also
-reports the last compact `fileProgress` observed for that tracked version.
+wrapper checks that status against the current on-disk text, and `open-files` also reports the last
+compact `fileProgress` observed for that tracked version.
 
 Stats are in-memory only and scoped to the current project Beam daemon.
 

From 2a3ab86dee55f1b05cfa53a56f7c8d1a4cbd1c1c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <emilio@lean-fro.org>
Date: Sun, 22 Mar 2026 02:23:14 +0100
Subject: [PATCH 6/6] Harden wrapper text and handle inputs

---
 Beam/Cli.lean                                 | 367 +++++++++++++-----
 README.md                                     |  24 ++
 scripts/install-beam-notes.txt                |   3 +
 scripts/lean-beam                             |  13 +-
 skills/lean-beam/SKILL.md                     |  13 +
 .../references/lean-run-at-semantics.md       |   8 +-
 skills/lean-beam/references/mcts-search.md    |  25 +-
 .../lean-beam/references/workflow-details.md  |   6 +
 tests/test-beam-wrapper.sh                    | 223 ++++++++++-
 9 files changed, 578 insertions(+), 104 deletions(-)

diff --git a/Beam/Cli.lean b/Beam/Cli.lean
index e54339e2..4f591799 100644
--- a/Beam/Cli.lean
+++ b/Beam/Cli.lean
@@ -7,6 +7,7 @@ Author: Emilio J. Gallego Arias
 import Lean
 import Beam.Broker.Client
 import Beam.Broker.Transport
+import RunAt.Protocol
 import Std.Internal.UV.Signal
 
 open Lean
@@ -73,6 +74,10 @@ private structure CliOptions where
   requestedSocket? : Option System.FilePath := none
   args : List String := []
 
+private structure ParsedTextArg where
+  text? : Option String := none
+  source : String := "argv"
+
 private def parseNatArg (name value : String) : IO Nat := do
   let some n := value.toNat?
     | throw <| IO.userError s!"invalid {name} '{value}'"
@@ -81,6 +86,35 @@ private def parseNatArg (name value : String) : IO Nat := do
 private def joinTextArgs (args : List String) : Option String :=
   if args.isEmpty then none else some <| String.intercalate " " args
 
+private def hasSubstring (text needle : String) : Bool :=
+  match text.splitOn needle with
+  | [_] => false
+  | _ => true
+
+private def textArgUsage (cmdHead : String) : String :=
+  s!"usage: beam [--root PATH] [--socket PATH | --port N] {cmdHead} [--stdin | --text-file <path> | -- <text...> | <text...>]"
+
+private def textArgReadsStdin (args : List String) : Bool :=
+  match args with
+  | ["--stdin"] => true
+  | _ => false
+
+private def parseTextArg (cmdHead : String) (args : List String) : IO ParsedTextArg := do
+  match args with
+  | [] => pure {}
+  | ["--stdin"] =>
+      pure { text? := some (← (← IO.getStdin).readToEnd), source := "stdin" }
+  | ["--text-file", path] =>
+      pure { text? := some (← IO.FS.readFile (System.FilePath.mk path)), source := s!"text-file:{path}" }
+  | "--" :: rest =>
+      pure { text? := joinTextArgs rest, source := "argv" }
+  | "--stdin" :: _ =>
+      throw <| IO.userError (textArgUsage cmdHead)
+  | "--text-file" :: _ =>
+      throw <| IO.userError (textArgUsage cmdHead)
+  | _ =>
+      pure { text? := joinTextArgs args, source := "argv" }
+
 private def parseJsonText (label text : String) : IO Json := do
   match Json.parse text with
   | .ok json => pure json
@@ -94,6 +128,14 @@ private def parseJsonArg (label arg : String) : IO Json := do
       pure arg
   parseJsonText label raw
 
+private def handleArgUsage (cmdHead : String) : String :=
+  s!"usage: beam [--root PATH] [--socket PATH | --port N] {cmdHead} <handle-json|-|--handle-file <path>>"
+
+private def handleArgReadsStdin (args : List String) : Bool :=
+  match args with
+  | "-" :: _ => true
+  | _ => false
+
 private def extractHandleJson (json : Json) : Json :=
   match json.getObjVal? "handle" with
   | .ok handle => handle
@@ -105,17 +147,31 @@ private def extractHandleJson (json : Json) : Json :=
           | .error _ => json
       | .error _ => json
 
+private def parseHandleText (raw : String) : IO Handle := do
+  let json ← parseJsonText "handle json" raw
+  match fromJson? (extractHandleJson json) with
+  | .ok handle => pure handle
+  | .error err =>
+      throw <| IO.userError s!"invalid handle payload: {err}"
+
 private def parseHandleArg (arg : String) : IO Handle := do
   let raw ←
     if arg == "-" then
       (← IO.getStdin).readToEnd
     else
       pure arg
-  let json ← parseJsonText "handle json" raw
-  match fromJson? (extractHandleJson json) with
-  | .ok handle => pure handle
-  | .error err =>
-      throw <| IO.userError s!"invalid handle payload: {err}"
+  parseHandleText raw
+
+private def parseHandleInput (cmdHead : String) (args : List String) : IO (Handle × List String) := do
+  match args with
+  | [] =>
+      throw <| IO.userError (handleArgUsage cmdHead)
+  | "--handle-file" :: path :: rest =>
+      pure ((← parseHandleText (← IO.FS.readFile (System.FilePath.mk path))), rest)
+  | "--handle-file" :: _ =>
+      throw <| IO.userError (handleArgUsage cmdHead)
+  | arg :: rest =>
+      pure ((← parseHandleArg arg), rest)
 
 private def parseLeanSyncArgs (args : List String) : IO Bool := do
   match args with
@@ -282,6 +338,32 @@ private def ensureSupportedLeanToolchain (home : System.FilePath) (toolchain : S
 private def boolText (value : Bool) : String :=
   if value then "true" else "false"
 
+private def parseEnvFlag (raw : String) : Bool :=
+  let normalized := raw.trimAscii.toString.toLower
+  !(normalized.isEmpty || normalized == "0" || normalized == "false" || normalized == "no")
+
+private def envFlag? (name : String) : IO (Option Bool) := do
+  match ← IO.getEnv name with
+  | some raw => pure <| some (parseEnvFlag raw)
+  | none => pure none
+
+private def hexDigit (n : Nat) : Char :=
+  if n < 10 then
+    Char.ofNat (48 + n)
+  else
+    Char.ofNat (87 + n)
+
+private def hexByte (byte : UInt8) : String :=
+  let n := byte.toNat
+  String.singleton (hexDigit (n / 16)) ++ String.singleton (hexDigit (n % 16))
+
+private def utf8Hex (bytes : ByteArray) : String :=
+  String.intercalate " " <| Id.run do
+    let mut parts : Array String := #[]
+    for byte in bytes do
+      parts := parts.push (hexByte byte)
+    return parts.toList
+
 private def bundleWorkspaceFor (bundleDir : System.FilePath) : System.FilePath :=
   bundleDir / "workspace"
 
@@ -1025,6 +1107,62 @@ private def annotateRunatMessage (clientRequestId? : Option String) (msg : Strin
   | none =>
       msg
 
+private def debugTextEnabled : IO Bool := do
+  pure <| (← envFlag? "BEAM_DEBUG_TEXT").getD false
+
+private def maybeEmitTextDebug (clientRequestId? : Option String) (action source : String) (text? : Option String) : IO Unit := do
+  if !(← debugTextEnabled) then
+    pure ()
+  else
+    match text? with
+    | none => pure ()
+    | some text =>
+        let bytes := text.toUTF8
+        let containsLiteralBackslashN := hasSubstring text "\\n"
+        IO.eprintln <| annotateRunatMessage clientRequestId?
+          s!"beam: debug text for {action}: source={source} utf8Bytes={bytes.size} containsNewline={boolText (text.contains '\n')} containsLiteralBackslashN={boolText containsLiteralBackslashN}"
+        IO.eprintln <| annotateRunatMessage clientRequestId?
+          s!"beam: debug text escaped={(Json.str text).compress}"
+        IO.eprintln <| annotateRunatMessage clientRequestId?
+          s!"beam: debug text utf8Hex={utf8Hex bytes}"
+
+private def decodeRunAtResult? (resp : Response) : Option RunAt.Result :=
+  match resp.result? with
+  | none => none
+  | some result =>
+      match fromJson? result with
+      | .ok payload => some payload
+      | .error _ => none
+
+private def responseErrorSummary? (action failureBoundary : String) (resp : Response) : Option String :=
+  resp.error?.map fun err =>
+    s!"beam: {action} request failed {failureBoundary} ({err.code}): {err.message}"
+
+private def runAtPayloadSummary? (action noun : String) (resp : Response) : Option String :=
+  match decodeRunAtResult? resp with
+  | some result =>
+      if result.success then
+        none
+      else
+        some s!"beam: {action} {noun} failed inside Lean; the request completed and returned result.success=false"
+  | none =>
+      none
+
+private def maybeEmitLiteralBackslashNewlineHint (req : Request) (resp : Response) : IO Unit := do
+  match req.op with
+  | .runAt | .runWith =>
+      match req.text?, decodeRunAtResult? resp with
+      | some text, some result =>
+          if !result.success && hasSubstring text "\\n" && !text.contains '\n' then
+            IO.eprintln <| annotateRunatMessage req.clientRequestId?
+              "beam: hint: the probe text contains the literal characters '\\n'; if you meant a real newline, use --stdin or --text-file."
+          else
+            pure ()
+      | _, _ =>
+          pure ()
+  | _ =>
+      pure ()
+
 private def withBrokerErrorContext {α} (root : System.FilePath) (action : IO α) : IO α := do
   try
     action
@@ -1063,20 +1201,22 @@ private def syncFileProgressSuffix (progress? : Option SyncFileProgress) : Strin
       s!", fp updates={progress.updates}{doneSuffix}"
 
 private structure BrokerWaitSpec where
+  action : String
   startMsg : String
   progressMsg : SyncFileProgress → String
   stillWaitingMsg : Nat → String
   completeMsg : Response → String
+  failureBoundary : String := "before the request completed"
+  responseNote? : Response → Option String := fun _ => none
 
 private structure InterruptWatcher where
   signal : Std.Internal.UV.Signal
   task : Task (Except IO.Error Unit)
 
 private def progressEnabled : IO Bool := do
-  match ← IO.getEnv "BEAM_PROGRESS" with
-  | some raw =>
-      let normalized := raw.trimAscii.toString.toLower
-      pure <| !(normalized.isEmpty || normalized == "0" || normalized == "false" || normalized == "no")
+  match ← envFlag? "BEAM_PROGRESS" with
+  | some enabled =>
+      pure enabled
   | none =>
       (← IO.getStderr).isTty
 
@@ -1136,6 +1276,7 @@ private def awaitBrokerResponse
 
 private def syncWaitSpec (path : String) : BrokerWaitSpec :=
   {
+    action := "lean-sync"
     startMsg := s!"beam: syncing {path} and waiting for Lean diagnostics"
     progressMsg := fun progress => s!"beam: sync progress for {path}{syncFileProgressSuffix (some progress)}"
     stillWaitingMsg := fun seconds => s!"beam: still syncing {path} ({seconds}s)"
@@ -1148,15 +1289,17 @@ private def syncWaitSpec (path : String) : BrokerWaitSpec :=
               ""
             else
               s!", saveReady=false ({result.saveReadyReason}, " ++
-                s!"stateErrorCount={result.stateErrorCount}, " ++
+              s!"stateErrorCount={result.stateErrorCount}, " ++
                 s!"stateCommandErrorCount={result.stateCommandErrorCount})"
           s!"beam: sync complete for {path} (version {result.version}{suffix}{readinessSuffix})"
       | none =>
-          s!"beam: sync complete for {path}"
+        s!"beam: sync complete for {path}"
+    failureBoundary := "before a complete diagnostics barrier was available"
   }
 
 private def refreshWaitSpec (path : String) : BrokerWaitSpec :=
   {
+    action := "lean-refresh"
     startMsg := s!"beam: refreshing {path} by closing and resyncing"
     progressMsg := fun progress => s!"beam: refresh progress for {path}{syncFileProgressSuffix (some progress)}"
     stillWaitingMsg := fun seconds => s!"beam: still refreshing {path} ({seconds}s)"
@@ -1169,33 +1312,39 @@ private def refreshWaitSpec (path : String) : BrokerWaitSpec :=
               ""
             else
               s!", saveReady=false ({result.saveReadyReason}, " ++
-                s!"stateErrorCount={result.stateErrorCount}, " ++
+              s!"stateErrorCount={result.stateErrorCount}, " ++
                 s!"stateCommandErrorCount={result.stateCommandErrorCount})"
           s!"beam: refresh complete for {path} (version {result.version}{suffix}{readinessSuffix})"
       | none =>
-          s!"beam: refresh complete for {path}"
+        s!"beam: refresh complete for {path}"
+    failureBoundary := "before a complete diagnostics barrier was available"
   }
 
-private def leanRunAtWaitSpec (path : String) (line character : Nat) : BrokerWaitSpec :=
+private def leanRunAtWaitSpec (action path : String) (line character : Nat) : BrokerWaitSpec :=
   let pos := s!"{path}:{line}:{character}"
   {
-    startMsg := s!"beam: running lean-run-at on {pos} and waiting for a ready Lean snapshot"
+    action := action
+    startMsg := s!"beam: running {action} on {pos} and waiting for a ready Lean snapshot"
     progressMsg := fun progress => s!"beam: snapshot progress for {pos}{syncFileProgressSuffix (some progress)}"
     stillWaitingMsg := fun seconds =>
-      s!"beam: still waiting for a ready Lean snapshot for {pos} ({seconds}s)"
+      s!"beam: still waiting for a ready Lean snapshot for {action} on {pos} ({seconds}s)"
     completeMsg := fun resp =>
-      s!"beam: lean-run-at complete for {pos}{syncFileProgressSuffix (responseFileProgress? resp)}"
+      s!"beam: {action} complete for {pos}{syncFileProgressSuffix (responseFileProgress? resp)}"
+    failureBoundary := "before probe execution"
+    responseNote? := runAtPayloadSummary? action "probe"
   }
 
 private def leanHoverWaitSpec (path : String) (line character : Nat) : BrokerWaitSpec :=
   let pos := s!"{path}:{line}:{character}"
   {
+    action := "lean-hover"
     startMsg := s!"beam: running lean-hover on {pos} and waiting for a ready Lean snapshot"
     progressMsg := fun progress => s!"beam: hover progress for {pos}{syncFileProgressSuffix (some progress)}"
     stillWaitingMsg := fun seconds =>
       s!"beam: still waiting for lean-hover on {pos} ({seconds}s)"
     completeMsg := fun resp =>
       s!"beam: lean-hover complete for {pos}{syncFileProgressSuffix (responseFileProgress? resp)}"
+    failureBoundary := "before hover data was available"
   }
 
 private def leanGoalsWaitSpec (path : String) (line character : Nat) (mode : GoalMode) : BrokerWaitSpec :=
@@ -1205,44 +1354,53 @@ private def leanGoalsWaitSpec (path : String) (line character : Nat) (mode : Goa
     | .after => "lean-goals-after"
     | .prev => "lean-goals-prev"
   {
+    action := action
     startMsg := s!"beam: running {action} on {pos} and waiting for a ready Lean snapshot"
     progressMsg := fun progress => s!"beam: goals progress for {pos}{syncFileProgressSuffix (some progress)}"
     stillWaitingMsg := fun seconds =>
       s!"beam: still waiting for {action} on {pos} ({seconds}s)"
     completeMsg := fun resp =>
       s!"beam: {action} complete for {pos}{syncFileProgressSuffix (responseFileProgress? resp)}"
+    failureBoundary := "before goal inspection completed"
   }
 
 private def leanRequestAtWaitSpec (path : String) (line character : Nat) (method : String) : BrokerWaitSpec :=
   let pos := s!"{path}:{line}:{character}"
   {
+    action := s!"lean-request-at {method}"
     startMsg := s!"beam: forwarding experimental {method} at {pos} and waiting for a ready Lean snapshot"
     progressMsg := fun progress => s!"beam: request-at progress for {pos}{syncFileProgressSuffix (some progress)}"
     stillWaitingMsg := fun seconds =>
       s!"beam: still waiting for experimental {method} at {pos} ({seconds}s)"
     completeMsg := fun resp =>
       s!"beam: experimental {method} complete for {pos}{syncFileProgressSuffix (responseFileProgress? resp)}"
+    failureBoundary := s!"before experimental {method} completed"
   }
 
 private def leanRunWithWaitSpec (path : String) (linear : Bool := false) : BrokerWaitSpec :=
   let action := if linear then "lean-run-with-linear" else "lean-run-with"
   {
+    action := action
     startMsg := s!"beam: running {action} on {path} and waiting for a ready Lean snapshot"
     progressMsg := fun progress => s!"beam: {action} progress for {path}{syncFileProgressSuffix (some progress)}"
     stillWaitingMsg := fun seconds =>
       s!"beam: still waiting for {action} on {path} ({seconds}s)"
     completeMsg := fun resp =>
       s!"beam: {action} complete for {path}{syncFileProgressSuffix (responseFileProgress? resp)}"
+    failureBoundary := "before speculative continuation completed"
+    responseNote? := runAtPayloadSummary? action "continuation"
   }
 
 private def leanSaveWaitSpec (path : String) (closeAfter : Bool := false) : BrokerWaitSpec :=
   let action := if closeAfter then "lean-close-save" else "lean-save"
   let verb := if closeAfter then "closing and saving" else "saving"
   {
+    action := action
     startMsg := s!"beam: {verb} {path} and waiting for Lean diagnostics/artifacts"
     progressMsg := fun progress => s!"beam: {action} progress for {path}{syncFileProgressSuffix (some progress)}"
     stillWaitingMsg := fun seconds => s!"beam: still waiting for {action} on {path} ({seconds}s)"
     completeMsg := fun resp => s!"beam: {action} complete for {path}{syncFileProgressSuffix (responseFileProgress? resp)}"
+    failureBoundary := "before save artifacts were finalized"
   }
 
 private def callBrokerWithProgress
@@ -1266,6 +1424,17 @@ private def callBrokerWithProgress
         awaitBrokerResponse task endpoint req spec
       else
         sendRequestWithCallbacks endpoint req callbacks
+    match responseErrorSummary? spec.action spec.failureBoundary resp with
+    | some note =>
+        IO.eprintln <| annotateRunatMessage req.clientRequestId? note
+    | none =>
+        pure ()
+    match spec.responseNote? resp with
+    | some note =>
+        IO.eprintln <| annotateRunatMessage req.clientRequestId? note
+    | none =>
+        pure ()
+    maybeEmitLiteralBackslashNewlineHint req resp
     printResponse resp
     failOnError resp
 
@@ -1274,14 +1443,14 @@ private def usage : String :=
     "usage:",
     "  beam [--root PATH] [--socket PATH | --port N] ensure lean|rocq",
     "  beam [--root PATH] cancel <request-id>",
-    "  beam [--root PATH] [--socket PATH | --port N] lean-run-at <path> <line> <character> <text...>",
-    "  beam [--root PATH] [--socket PATH | --port N] lean-run-at-handle <path> <line> <character> <text...>",
+    "  beam [--root PATH] [--socket PATH | --port N] lean-run-at <path> <line> <character> [--stdin | --text-file <path> | -- <text...> | <text...>]",
+    "  beam [--root PATH] [--socket PATH | --port N] lean-run-at-handle <path> <line> <character> [--stdin | --text-file <path> | -- <text...> | <text...>]",
     "  beam [--root PATH] [--socket PATH | --port N] lean-hover <path> <line> <character>",
     "  beam [--root PATH] [--socket PATH | --port N] lean-goals-after <path> <line> <character>",
     "  beam [--root PATH] [--socket PATH | --port N] lean-goals-prev <path> <line> <character>",
-    "  beam [--root PATH] [--socket PATH | --port N] lean-run-with <path> <handle-json|-> <text...>",
-    "  beam [--root PATH] [--socket PATH | --port N] lean-run-with-linear <path> <handle-json|-> <text...>",
-    "  beam [--root PATH] [--socket PATH | --port N] lean-release <path> <handle-json|->",
+    "  beam [--root PATH] [--socket PATH | --port N] lean-run-with <path> <handle-json|-|--handle-file <path>> [--stdin | --text-file <path> | -- <text...> | <text...>]",
+    "  beam [--root PATH] [--socket PATH | --port N] lean-run-with-linear <path> <handle-json|-|--handle-file <path>> [--stdin | --text-file <path> | -- <text...> | <text...>]",
+    "  beam [--root PATH] [--socket PATH | --port N] lean-release <path> <handle-json|-|--handle-file <path>>",
     "  beam [--root PATH] [--socket PATH | --port N] lean-deps <path>",
     "  beam [--root PATH] [--socket PATH | --port N] lean-sync <path> [+full]",
     "  beam [--root PATH] [--socket PATH | --port N] lean-refresh <path> [+full]",
@@ -1306,10 +1475,15 @@ private def usage : String :=
     "Separate lean-run-at calls are independent probes on the current saved file snapshot.",
     "For exact speculative chaining, use lean-run-at-handle and then lean-run-with /",
     "lean-run-with-linear.",
+    "For multiline text-carrying Lean probes, prefer --stdin or --text-file <path>; use -- before",
+    "text that itself starts with --.",
+    "For handle-based commands, use --handle-file <path> when you do not want to inline handle json.",
     "For lean-sync / lean-refresh / lean-save / lean-close-save, diagnostics always stream for the",
     "current request;",
     "default is errors only, and +full widens the stream to warnings, info, and hints.",
     "Wrapper diagnostics and progress are human-facing on stderr.",
+    "Set BEAM_DEBUG_TEXT=1 to print the exact escaped text and UTF-8 bytes sent for text-carrying",
+    "Lean probe requests.",
     "For machine-readable streaming diagnostics/progress, use beam-client request-stream.",
     "",
     "Expert-only experimental commands are documented in docs/experimental.md.",
@@ -1322,6 +1496,81 @@ private def printExperimentalInfo (home : System.FilePath) : IO Unit := do
   IO.println "This is an unstable broker escape hatch, not part of the stable runAt contract."
   IO.println "Current experimental entry point: lean-request-at"
 
+private def runLeanRunAt
+    (home : System.FilePath)
+    (opts : CliOptions)
+    (action path lineText characterText : String)
+    (textArgs : List String)
+    (storeHandle : Bool := false) : IO Unit := do
+  let root ← projectRoot opts .lean
+  let (endpoint, _) ← ensureProjectDaemon home root .lean opts
+  let line ← parseNatArg "line" lineText
+  let character ← parseNatArg "character" characterText
+  let parsedText ← parseTextArg s!"{action} <path> <line> <character>" textArgs
+  let req ← withEnvClientRequestId {
+    op := .runAt
+    backend := .lean
+    root? := some root.toString
+    path? := some path
+    line? := some line
+    character? := some character
+    text? := parsedText.text?
+    storeHandle? := if storeHandle then some true else none
+  }
+  maybeEmitTextDebug req.clientRequestId? action parsedText.source parsedText.text?
+  callBrokerWithProgress root endpoint req (leanRunAtWaitSpec action path line character)
+
+private def runLeanRunWith
+    (home : System.FilePath)
+    (opts : CliOptions)
+    (action path : String)
+    (args : List String)
+    (linear : Bool := false) : IO Unit := do
+  let textArgs :=
+    match args with
+    | [] => []
+    | "--handle-file" :: _ :: rest => rest
+    | _ :: rest => rest
+  if handleArgReadsStdin args && textArgReadsStdin textArgs then
+    throw <| IO.userError <| String.intercalate "\n" [
+      textArgUsage s!"{action} <path> <handle-json|-|--handle-file <path>>",
+      "cannot read both handle json and continuation text from stdin; pass the handle inline, use --handle-file, or use --text-file for the text"
+    ]
+  let root ← projectRoot opts .lean
+  let (endpoint, _) ← ensureProjectDaemon home root .lean opts
+  let (handle, textArgs) ← parseHandleInput s!"{action} <path>" args
+  let parsedText ← parseTextArg s!"{action} <path> <handle-json|-|--handle-file <path>>" textArgs
+  let req ← withEnvClientRequestId {
+    op := .runWith
+    backend := .lean
+    root? := some root.toString
+    path? := some path
+    handle? := some handle
+    text? := parsedText.text?
+    storeHandle? := some true
+    linear? := some linear
+  }
+  maybeEmitTextDebug req.clientRequestId? action parsedText.source parsedText.text?
+  callBrokerWithProgress root endpoint req (leanRunWithWaitSpec path (linear := linear))
+
+private def runLeanRelease
+    (home : System.FilePath)
+    (opts : CliOptions)
+    (path : String)
+    (args : List String) : IO Unit := do
+  let root ← projectRoot opts .lean
+  let (endpoint, _) ← ensureProjectDaemon home root .lean opts
+  let (handle, extra) ← parseHandleInput "lean-release <path>" args
+  unless extra.isEmpty do
+    throw <| IO.userError (handleArgUsage "lean-release <path>")
+  callBroker root endpoint {
+    op := .release
+    backend := .lean
+    root? := some root.toString
+    path? := some path
+    handle? := some handle
+  }
+
 private partial def parseCliOptions (opts : CliOptions) : List String → IO CliOptions
   | [] => pure opts
   | "--root" :: root :: rest => do
@@ -1476,34 +1725,9 @@ private def runCommand (home : System.FilePath) (opts : CliOptions) : IO Unit :=
       let (endpoint, _) ← ensureProjectDaemon home root backend opts
       callBroker root endpoint { op := .ensure, backend := backend, root? := some root.toString }
   | "lean-run-at" :: path :: line :: character :: text =>
-      let root ← projectRoot opts .lean
-      let (endpoint, _) ← ensureProjectDaemon home root .lean opts
-      let line ← parseNatArg "line" line
-      let character ← parseNatArg "character" character
-      callBrokerWithProgress root endpoint {
-        op := .runAt
-        backend := .lean
-        root? := some root.toString
-        path? := some path
-        line? := some line
-        character? := some character
-        text? := joinTextArgs text
-      } (leanRunAtWaitSpec path line character)
+      runLeanRunAt home opts "lean-run-at" path line character text
   | "lean-run-at-handle" :: path :: line :: character :: text =>
-      let root ← projectRoot opts .lean
-      let (endpoint, _) ← ensureProjectDaemon home root .lean opts
-      let line ← parseNatArg "line" line
-      let character ← parseNatArg "character" character
-      callBrokerWithProgress root endpoint {
-        op := .runAt
-        backend := .lean
-        root? := some root.toString
-        path? := some path
-        line? := some line
-        character? := some character
-        text? := joinTextArgs text
-        storeHandle? := some true
-      } (leanRunAtWaitSpec path line character)
+      runLeanRunAt home opts "lean-run-at-handle" path line character text (storeHandle := true)
   | "lean-hover" :: path :: line :: character :: [] =>
       let root ← projectRoot opts .lean
       let (endpoint, _) ← ensureProjectDaemon home root .lean opts
@@ -1566,45 +1790,12 @@ private def runCommand (home : System.FilePath) (opts : CliOptions) : IO Unit :=
         method? := some method
         params? := params?
       } (leanRequestAtWaitSpec path line character method)
-  | "lean-run-with" :: path :: handleArg :: text =>
-      let root ← projectRoot opts .lean
-      let (endpoint, _) ← ensureProjectDaemon home root .lean opts
-      let handle ← parseHandleArg handleArg
-      callBrokerWithProgress root endpoint {
-        op := .runWith
-        backend := .lean
-        root? := some root.toString
-        path? := some path
-        handle? := some handle
-        text? := joinTextArgs text
-        storeHandle? := some true
-        linear? := some false
-      } (leanRunWithWaitSpec path)
-  | "lean-run-with-linear" :: path :: handleArg :: text =>
-      let root ← projectRoot opts .lean
-      let (endpoint, _) ← ensureProjectDaemon home root .lean opts
-      let handle ← parseHandleArg handleArg
-      callBrokerWithProgress root endpoint {
-        op := .runWith
-        backend := .lean
-        root? := some root.toString
-        path? := some path
-        handle? := some handle
-        text? := joinTextArgs text
-        storeHandle? := some true
-        linear? := some true
-      } (leanRunWithWaitSpec path (linear := true))
-  | "lean-release" :: path :: handleArg :: [] =>
-      let root ← projectRoot opts .lean
-      let (endpoint, _) ← ensureProjectDaemon home root .lean opts
-      let handle ← parseHandleArg handleArg
-      callBroker root endpoint {
-        op := .release
-        backend := .lean
-        root? := some root.toString
-        path? := some path
-        handle? := some handle
-      }
+  | "lean-run-with" :: path :: args =>
+      runLeanRunWith home opts "lean-run-with" path args
+  | "lean-run-with-linear" :: path :: args =>
+      runLeanRunWith home opts "lean-run-with-linear" path args (linear := true)
+  | "lean-release" :: path :: args =>
+      runLeanRelease home opts path args
   | "lean-deps" :: path :: [] =>
       let root ← projectRoot opts .lean
       let (endpoint, _) ← ensureProjectDaemon home root .lean opts
diff --git a/README.md b/README.md
index 2f45f444..7c9cb8e6 100644
--- a/README.md
+++ b/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`.
diff --git a/scripts/install-beam-notes.txt b/scripts/install-beam-notes.txt
index 51a3965b..479384e5 100644
--- a/scripts/install-beam-notes.txt
+++ b/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
diff --git a/scripts/lean-beam b/scripts/lean-beam
index 4a4e63de..90ea13ad 100755
--- a/scripts/lean-beam
+++ b/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
 }
 
diff --git a/skills/lean-beam/SKILL.md b/skills/lean-beam/SKILL.md
index 47de089a..ed05de10 100644
--- a/skills/lean-beam/SKILL.md
+++ b/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
 
diff --git a/skills/lean-beam/references/lean-run-at-semantics.md b/skills/lean-beam/references/lean-run-at-semantics.md
index e7cd1725..e14deed3 100644
--- a/skills/lean-beam/references/lean-run-at-semantics.md
+++ b/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'
 ```
 
diff --git a/skills/lean-beam/references/mcts-search.md b/skills/lean-beam/references/mcts-search.md
index 2b654698..70432774 100644
--- a/skills/lean-beam/references/mcts-search.md
+++ b/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.
diff --git a/skills/lean-beam/references/workflow-details.md b/skills/lean-beam/references/workflow-details.md
index 0289bb44..7d4aecfa 100644
--- a/skills/lean-beam/references/workflow-details.md
+++ b/skills/lean-beam/references/workflow-details.md
@@ -107,6 +107,12 @@ to a module is a valid `lean-beam sync` target, but not a valid `lean-beam save`
 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" -
diff --git a/tests/test-beam-wrapper.sh b/tests/test-beam-wrapper.sh
index 99cbf92f..e9d84a51 100755
--- a/tests/test-beam-wrapper.sh
+++ b/tests/test-beam-wrapper.sh
@@ -274,6 +274,120 @@ fi
     exit 1
   fi
   rm -f "$cmd_err"
+  multiline_stdin_out="$(printf 'def stdinProbe : Nat :=\n  42' | "$beam_script" lean-run-at PositionEmptyLine.lean 1 0 --stdin)"
+  if [ "$(RUNAT_JSON_PAYLOAD="$multiline_stdin_out" read_json_text_field ok)" != "true" ]; then
+    echo "expected wrapper lean-run-at --stdin probe to succeed" >&2
+    printf '%s\n' "$multiline_stdin_out" >&2
+    exit 1
+  fi
+  if [ "$(RUNAT_JSON_PAYLOAD="$multiline_stdin_out" read_json_text_field result.success)" != "true" ]; then
+    echo "expected wrapper lean-run-at --stdin payload success" >&2
+    printf '%s\n' "$multiline_stdin_out" >&2
+    exit 1
+  fi
+  if [ "$(RUNAT_JSON_PAYLOAD="$multiline_stdin_out" read_json_array_len result.messages)" != "0" ]; then
+    echo "expected wrapper lean-run-at --stdin multiline declaration to produce no messages" >&2
+    printf '%s\n' "$multiline_stdin_out" >&2
+    exit 1
+  fi
+  probe_text_file="multiline-probe.lean"
+  printf 'def fileProbe : Nat :=\n  42' > "$probe_text_file"
+  multiline_file_out="$("$beam_script" lean-run-at PositionEmptyLine.lean 1 0 --text-file "$probe_text_file")"
+  if [ "$(RUNAT_JSON_PAYLOAD="$multiline_file_out" read_json_text_field ok)" != "true" ]; then
+    echo "expected wrapper lean-run-at --text-file probe to succeed" >&2
+    printf '%s\n' "$multiline_file_out" >&2
+    exit 1
+  fi
+  if [ "$(RUNAT_JSON_PAYLOAD="$multiline_file_out" read_json_text_field result.success)" != "true" ]; then
+    echo "expected wrapper lean-run-at --text-file payload success" >&2
+    printf '%s\n' "$multiline_file_out" >&2
+    exit 1
+  fi
+  if [ "$(RUNAT_JSON_PAYLOAD="$multiline_file_out" read_json_array_len result.messages)" != "0" ]; then
+    echo "expected wrapper lean-run-at --text-file multiline declaration to produce no messages" >&2
+    printf '%s\n' "$multiline_file_out" >&2
+    exit 1
+  fi
+  delimiter_out="$("$beam_script" lean-run-at PositionEmptyLine.lean 1 0 -- $'--stdin\n#check answer')"
+  if [ "$(RUNAT_JSON_PAYLOAD="$delimiter_out" read_json_text_field ok)" != "true" ]; then
+    echo "expected wrapper lean-run-at -- delimiter path to treat leading --stdin as text" >&2
+    printf '%s\n' "$delimiter_out" >&2
+    exit 1
+  fi
+  if ! printf '%s\n' "$delimiter_out" | grep -q 'answer : Nat'; then
+    echo "expected wrapper lean-run-at -- delimiter path to keep the leading --stdin text as a comment" >&2
+    printf '%s\n' "$delimiter_out" >&2
+    exit 1
+  fi
+  debug_text_err="$(mktemp /tmp/beam-wrapper-debug-text-XXXXXX)"
+  debug_text_out="$(printf 'def debugProbe : Nat :=\n  42' | BEAM_DEBUG_TEXT=1 "$beam_script" lean-run-at PositionEmptyLine.lean 1 0 --stdin 2>"$debug_text_err")"
+  if [ "$(RUNAT_JSON_PAYLOAD="$debug_text_out" read_json_text_field ok)" != "true" ]; then
+    echo "expected wrapper debug-text probe to succeed" >&2
+    printf '%s\n' "$debug_text_out" >&2
+    cat "$debug_text_err" >&2
+    rm -f "$debug_text_err"
+    exit 1
+  fi
+  if ! grep -q 'debug text for lean-run-at: source=stdin' "$debug_text_err"; then
+    echo "expected wrapper debug-text mode to report stdin as the text source" >&2
+    cat "$debug_text_err" >&2
+    rm -f "$debug_text_err"
+    exit 1
+  fi
+  if ! grep -q 'containsNewline=true' "$debug_text_err"; then
+    echo "expected wrapper debug-text mode to report a real newline" >&2
+    cat "$debug_text_err" >&2
+    rm -f "$debug_text_err"
+    exit 1
+  fi
+  if ! grep -q 'containsLiteralBackslashN=false' "$debug_text_err"; then
+    echo "expected wrapper debug-text mode to distinguish literal backslash-n from a real newline" >&2
+    cat "$debug_text_err" >&2
+    rm -f "$debug_text_err"
+    exit 1
+  fi
+  if ! grep -q 'escaped="def debugProbe : Nat :=\\n  42"' "$debug_text_err"; then
+    echo "expected wrapper debug-text mode to print the escaped probe text" >&2
+    cat "$debug_text_err" >&2
+    rm -f "$debug_text_err"
+    exit 1
+  fi
+  if ! grep -q 'utf8Hex=' "$debug_text_err" || ! grep -q '0a' "$debug_text_err"; then
+    echo "expected wrapper debug-text mode to print UTF-8 bytes including the newline byte" >&2
+    cat "$debug_text_err" >&2
+    rm -f "$debug_text_err"
+    exit 1
+  fi
+  rm -f "$debug_text_err"
+  literal_newline_err="$(mktemp /tmp/beam-wrapper-literal-newline-XXXXXX)"
+  literal_newline_out="$("$beam_script" lean-run-at PositionEmptyLine.lean 1 0 'def _probe_tmp : Nat := 0\n' 2>"$literal_newline_err")"
+  if [ "$(RUNAT_JSON_PAYLOAD="$literal_newline_out" read_json_text_field ok)" != "true" ]; then
+    echo "expected wrapper literal-\\n probe to stay a payload failure, not a transport error" >&2
+    printf '%s\n' "$literal_newline_out" >&2
+    cat "$literal_newline_err" >&2
+    rm -f "$literal_newline_err"
+    exit 1
+  fi
+  if [ "$(RUNAT_JSON_PAYLOAD="$literal_newline_out" read_json_text_field result.success)" != "false" ]; then
+    echo "expected wrapper literal-\\n probe to fail in the run-at payload" >&2
+    printf '%s\n' "$literal_newline_out" >&2
+    cat "$literal_newline_err" >&2
+    rm -f "$literal_newline_err"
+    exit 1
+  fi
+  if ! grep -q "literal characters '\\\\n'" "$literal_newline_err"; then
+    echo "expected wrapper literal-\\n probe to print a newline hint" >&2
+    cat "$literal_newline_err" >&2
+    rm -f "$literal_newline_err"
+    exit 1
+  fi
+  if ! grep -q 'probe failed inside Lean; the request completed and returned result.success=false' "$literal_newline_err"; then
+    echo "expected wrapper literal-\\n probe to distinguish a probe failure from a request failure" >&2
+    cat "$literal_newline_err" >&2
+    rm -f "$literal_newline_err"
+    exit 1
+  fi
+  rm -f "$literal_newline_err"
   blank_ok_out="$("$beam_script" lean-run-at PositionEmptyLine.lean 1 0 "#check answer")"
   if [ "$(RUNAT_JSON_PAYLOAD="$blank_ok_out" read_json_text_field ok)" != "true" ]; then
     echo "expected wrapper blank-line probe at character 0 to succeed" >&2
@@ -298,6 +412,12 @@ fi
     rm -f "$blank_err"
     exit 1
   fi
+  if ! grep -q 'lean-run-at request failed before probe execution (invalidParams)' "$blank_err"; then
+    echo "expected wrapper blank-line invalid position path to distinguish request failure from probe failure" >&2
+    cat "$blank_err" >&2
+    rm -f "$blank_err"
+    exit 1
+  fi
   rm -f "$blank_err"
   utf16_ok_out="$("$beam_script" lean-run-at PositionUtf16.lean 1 5 "#check Nat")"
   if [ "$(RUNAT_JSON_PAYLOAD="$utf16_ok_out" read_json_text_field ok)" != "true" ]; then
@@ -924,6 +1044,34 @@ EOF
 example : True ∧ True := by
 EOF
 
+  mint_handle_stdin="$(printf 'constructor' | "$beam_script" lean-run-at-handle HandleSmoke.lean 0 27 --stdin)"
+  if [ "$(RUNAT_JSON_PAYLOAD="$mint_handle_stdin" read_json_text_field ok)" != "true" ]; then
+    echo "expected wrapper handle mint via --stdin to succeed" >&2
+    printf '%s\n' "$mint_handle_stdin" >&2
+    exit 1
+  fi
+  if [ "$(RUNAT_JSON_PAYLOAD="$mint_handle_stdin" read_json_text_field result.handle.backend)" != "lean" ]; then
+    echo "expected wrapper handle mint via --stdin to return a lean handle" >&2
+    printf '%s\n' "$mint_handle_stdin" >&2
+    exit 1
+  fi
+
+  handle_mint_file="handle-mint.txt"
+  printf 'constructor' > "$handle_mint_file"
+  mint_handle_file="$("$beam_script" lean-run-at-handle HandleSmoke.lean 0 27 --text-file "$handle_mint_file")"
+  if [ "$(RUNAT_JSON_PAYLOAD="$mint_handle_file" read_json_text_field ok)" != "true" ]; then
+    echo "expected wrapper handle mint via --text-file to succeed" >&2
+    printf '%s\n' "$mint_handle_file" >&2
+    exit 1
+  fi
+  if [ "$(RUNAT_JSON_PAYLOAD="$mint_handle_file" read_json_text_field result.handle.backend)" != "lean" ]; then
+    echo "expected wrapper handle mint via --text-file to return a lean handle" >&2
+    printf '%s\n' "$mint_handle_file" >&2
+    exit 1
+  fi
+  branch_handle_file="branch-handle.json"
+  printf '%s\n' "$mint_handle_file" > "$branch_handle_file"
+
   mint_handle="$("$beam_script" lean-run-at-handle HandleSmoke.lean 0 27 "constructor")"
   if [ "$(RUNAT_JSON_PAYLOAD="$mint_handle" read_json_text_field ok)" != "true" ]; then
     echo "expected wrapper handle mint to succeed" >&2
@@ -936,6 +1084,57 @@ EOF
     exit 1
   fi
 
+  branch_step_stdin_err="$(mktemp /tmp/beam-wrapper-run-with-stdin-XXXXXX)"
+  branch_step_stdin="$(printf 'exact trivial' | BEAM_DEBUG_TEXT=1 "$beam_script" lean-run-with HandleSmoke.lean "$mint_handle_stdin" --stdin 2>"$branch_step_stdin_err")"
+  if [ "$(RUNAT_JSON_PAYLOAD="$branch_step_stdin" read_json_text_field ok)" != "true" ]; then
+    echo "expected wrapper non-linear handle continuation via --stdin to succeed" >&2
+    printf '%s\n' "$branch_step_stdin" >&2
+    cat "$branch_step_stdin_err" >&2
+    rm -f "$branch_step_stdin_err"
+    exit 1
+  fi
+  if [ "$(RUNAT_JSON_PAYLOAD="$branch_step_stdin" read_json_text_field result.handle.backend)" != "lean" ]; then
+    echo "expected wrapper non-linear handle continuation via --stdin to return a successor handle" >&2
+    printf '%s\n' "$branch_step_stdin" >&2
+    cat "$branch_step_stdin_err" >&2
+    rm -f "$branch_step_stdin_err"
+    exit 1
+  fi
+  if ! grep -q 'debug text for lean-run-with: source=stdin' "$branch_step_stdin_err"; then
+    echo "expected wrapper run-with debug-text mode to report stdin as the continuation text source" >&2
+    cat "$branch_step_stdin_err" >&2
+    rm -f "$branch_step_stdin_err"
+    exit 1
+  fi
+  rm -f "$branch_step_stdin_err"
+
+  branch_step_file="$(printf 'exact trivial' | "$beam_script" lean-run-with HandleSmoke.lean --handle-file "$branch_handle_file" --stdin)"
+  if [ "$(RUNAT_JSON_PAYLOAD="$branch_step_file" read_json_text_field ok)" != "true" ]; then
+    echo "expected wrapper non-linear handle continuation via --handle-file to succeed" >&2
+    printf '%s\n' "$branch_step_file" >&2
+    exit 1
+  fi
+  if [ "$(RUNAT_JSON_PAYLOAD="$branch_step_file" read_json_text_field result.handle.backend)" != "lean" ]; then
+    echo "expected wrapper non-linear handle continuation via --handle-file to return a successor handle" >&2
+    printf '%s\n' "$branch_step_file" >&2
+    exit 1
+  fi
+
+  stdin_conflict_err="$(mktemp /tmp/beam-wrapper-run-with-stdin-conflict-XXXXXX)"
+  if printf '%s\n' "$mint_handle" | "$beam_script" lean-run-with HandleSmoke.lean - --stdin >"$stdin_conflict_err" 2>&1; then
+    echo "expected wrapper run-with to reject reading both handle json and text from stdin" >&2
+    cat "$stdin_conflict_err" >&2
+    rm -f "$stdin_conflict_err"
+    exit 1
+  fi
+  if ! grep -q 'cannot read both handle json and continuation text from stdin' "$stdin_conflict_err"; then
+    echo "expected wrapper run-with stdin conflict to explain the single-stdin limitation" >&2
+    cat "$stdin_conflict_err" >&2
+    rm -f "$stdin_conflict_err"
+    exit 1
+  fi
+  rm -f "$stdin_conflict_err"
+
   branch_step="$(printf '%s\n' "$mint_handle" | "$beam_script" lean-run-with HandleSmoke.lean - "exact trivial")"
   if [ "$(RUNAT_JSON_PAYLOAD="$branch_step" read_json_text_field ok)" != "true" ]; then
     echo "expected wrapper non-linear handle continuation to succeed" >&2
@@ -967,14 +1166,18 @@ EOF
     exit 1
   fi
 
-  linear_step="$(printf '%s\n' "$mint_linear" | "$beam_script" lean-run-with-linear HandleSmoke.lean - "exact trivial")"
+  linear_text_file="linear-continuation.txt"
+  printf 'exact trivial' > "$linear_text_file"
+  linear_handle_file="linear-handle.json"
+  printf '%s\n' "$mint_linear" > "$linear_handle_file"
+  linear_step="$("$beam_script" lean-run-with-linear HandleSmoke.lean --handle-file "$linear_handle_file" --text-file "$linear_text_file")"
   if [ "$(RUNAT_JSON_PAYLOAD="$linear_step" read_json_text_field ok)" != "true" ]; then
-    echo "expected wrapper linear handle continuation to succeed" >&2
+    echo "expected wrapper linear handle continuation via --handle-file and --text-file to succeed" >&2
     printf '%s\n' "$linear_step" >&2
     exit 1
   fi
   if [ "$(RUNAT_JSON_PAYLOAD="$linear_step" read_json_text_field result.handle.backend)" != "lean" ]; then
-    echo "expected wrapper linear handle continuation to return a successor handle" >&2
+    echo "expected wrapper linear handle continuation via --handle-file and --text-file to return a successor handle" >&2
     printf '%s\n' "$linear_step" >&2
     exit 1
   fi
@@ -994,9 +1197,11 @@ EOF
   fi
   rm -f "$linear_reuse_err"
 
-  release_out="$(printf '%s\n' "$linear_step" | "$beam_script" lean-release HandleSmoke.lean -)"
+  release_handle_file="release-handle.json"
+  printf '%s\n' "$linear_step" > "$release_handle_file"
+  release_out="$("$beam_script" lean-release HandleSmoke.lean --handle-file "$release_handle_file")"
   if [ "$(RUNAT_JSON_PAYLOAD="$release_out" read_json_text_field ok)" != "true" ]; then
-    echo "expected wrapper handle release to succeed" >&2
+    echo "expected wrapper handle release via --handle-file to succeed" >&2
     printf '%s\n' "$release_out" >&2
     exit 1
   fi
@@ -1576,6 +1781,14 @@ fi
     rm -f "$stale_sync_err"
     exit 1
   fi
+  if ! grep -q 'lean-sync request failed before a complete diagnostics barrier was available (syncBarrierIncomplete)' "$stale_sync_err"; then
+    echo "expected stale-import lean-sync failure to distinguish request failure from ordinary sync diagnostics" >&2
+    cat "$stale_sync_json" >&2
+    cat "$stale_sync_err" >&2
+    rm -f "$stale_sync_json"
+    rm -f "$stale_sync_err"
+    exit 1
+  fi
   if [ "$(RUNAT_JSON_PAYLOAD="$(cat "$stale_sync_json")" read_json_text_field error.code)" != "syncBarrierIncomplete" ]; then
     echo "expected stale-import lean-sync failure to expose syncBarrierIncomplete" >&2
     cat "$stale_sync_json" >&2