From e4bea5aeb8a9f88c0c1f5c8ee459e4833ae39a6a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 28 Oct 2026 01:24:43 +0100 Subject: [PATCH] doc: explain sandboxed CLI recovery errors and record doctor fixes A sandbox that gives each shell command its own network namespace hides a healthy serve owner, so CLI commands report sessionRecoveryRequired. Point agents at the MCP tools instead of recover, and add changelog entries for the user-visible doctor fixes from #391 and #397. --- CHANGELOG.md | 9 +++++++++ docs/SETUP.md | 7 +++++++ skills/lean-beam/references/setup-and-recovery.md | 4 ++++ 3 files changed, 20 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7d9dcc4e..4fbe92ca 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -12,6 +12,15 @@ This project keeps a lightweight, reverse-chronological changelog. Dates use `YY ### Fixed +- `lean-beam doctor` explains when a project's Lean compiler exists but its Beam runtime is + missing, including Lean source checkouts that select a local stage1 build. It prints a text + report by default or one structured response with `--json`, instead of mixing JSON with a + duplicate human explanation + ([#397](https://github.com/leanprover/lean-beam/pull/397), @ejgallego). +- `lean-beam doctor clients` no longer reports disabled integrations, or definitions that become + valid only after merging configuration layers, as checked. Unsupported conversions, incomplete + layers, and unresolved policy are reported as unverified + ([#391](https://github.com/leanprover/lean-beam/pull/391), @ejgallego). - Tactic probes that hit `maxRecDepth` or `maxHeartbeats` now return `success: false` with the original proof state and the limit diagnostic, instead of an `internalError` transport failure ([#393](https://github.com/leanprover/lean-beam/pull/393), @ejgallego). diff --git a/docs/SETUP.md b/docs/SETUP.md index 15102774..fc9b81f9 100644 --- a/docs/SETUP.md +++ b/docs/SETUP.md @@ -45,6 +45,13 @@ internet access or public network bind is needed for that communication. A writa directory alone does not make a daemon reachable across separate network namespaces. See [sessions and recovery](#sessions-and-recovery) for private-directory requirements and selectors. +Some agent sandboxes run each shell command in its own network namespace; Claude Code's Bash +sandbox is one example. A healthy `lean-beam serve` owner is then unreachable from later commands: +they report `sessionRecoveryRequired`, and `doctor` reports that recovery is required. The owner is +still running, so the recovery precondition is not met; do not run `recover`. Use the client's +registered Beam MCP tools, which need no loopback TCP, or run the owner and its clients in one +namespace. + A CLI request executes Lean in the existing owner's workers, with that owner's launch permissions. Putting only the attaching CLI command in a sandbox does not constrain an owner launched outside it. A sandbox applied to an agent's shell commands does not automatically sandbox an MCP server diff --git a/skills/lean-beam/references/setup-and-recovery.md b/skills/lean-beam/references/setup-and-recovery.md index 06a8e503..27aa0bac 100644 --- a/skills/lean-beam/references/setup-and-recovery.md +++ b/skills/lean-beam/references/setup-and-recovery.md @@ -54,6 +54,10 @@ Optional online references: the session by root/directory, not by port. IPC needs neither internet access nor a public bind. - MCP stdio creates its runtime directly and uses pipes to Lean/Lake children. It does not attach to the CLI daemon, so that path does not require CLI loopback TCP permissions. +- A sandbox that gives each shell command its own network namespace (for example Claude Code's + Bash sandbox) hides a healthy `serve` owner: CLI commands report `sessionRecoveryRequired` and + `doctor` reports recovery required. Do not run `recover`; the owner is still running. Use the + Beam MCP tools instead, or run owner and clients in one namespace. - CLI Lean work runs in the existing owner's workers with that owner's launch permissions, not the attaching command's sandbox. A sandboxed client can therefore reach a more privileged owner. - Both run Lean IO with their actual process permissions. A sandbox on agent shell commands does