doc: clarify sandbox recovery and record setup fixes

CHANGELOG.md

@@ -12,10 +12,25 @@ This project keeps a lightweight, reverse-chronological changelog. Dates use `YY
 
 ### Fixed
 
+- When the selected Lean compiler has no Beam runtime, setup guidance identifies the compiler
+  and bound installation. Reinstall commands retain every target from the confirmed current
+  standalone generation; older or unconfirmed generations get manual guidance. Unsupported
+  official targets now point to a compatible Beam revision while preserving the project's
+  `lean-toolchain` and dependency pins
+  ([#409](https://github.com/leanprover/lean-beam/pull/409), @ejgallego).
 - `sync` and `refresh` now return `internalError` when a diagnostic burst exhausts pending
   delivery capacity between complete output frames, rather than losing the terminal response.
   Recovery replies observe daemon shutdown; existing delivery budgets remain unchanged
   ([#412](https://github.com/leanprover/lean-beam/pull/412), @ejgallego).
+- `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).
 - Clarify that installer skill and MCP setup summaries describe only actions performed during
   the current run, so skipped registration does not imply that existing client setup is absent
   ([#394](https://github.com/leanprover/lean-beam/pull/394), @ejgallego).

docs/SETUP.md

@@ -45,6 +45,37 @@ 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.
 
+**Use the registered Beam MCP tools when each shell command runs in a separate network namespace.**
+For CLI use, the owner and every attaching command must share a network namespace.
+
+Claude Code's Bash sandbox on Linux and WSL2 is one such environment. A healthy `lean-beam serve`
+owner is then unreachable from later commands: they report `sessionRecoveryRequired`, and `doctor`
+reports that recovery is required.
+
+**Do not run `recover` until you have independently confirmed that the matching owner, daemon,
+and every other producer have stopped.** Connection refusal, `sessionRecoveryRequired`, and a
+returned `error.data.remedy_command` do not establish this. If you cannot confirm shutdown, stop
+and coordinate with the operator.
+
+To move an existing session out of the sandbox, stop its foreground owner and confirm cleanup
+before starting a replacement. In Claude Code, request an unsandboxed Bash retry with the Bash tool
+parameter `dangerouslyDisableSandbox: true`. For repeated direct `lean-beam` calls, merge this into
+your `.claude/settings.local.json`:
+
+```json
+{
+  "sandbox": {
+    "excludedCommands": ["lean-beam *"]
+  }
+}
+```
+
+The pattern matches direct `lean-beam` calls with arguments. Absolute paths and `elan run` need
+matching patterns; a `cd` or redirect keeps the call sandboxed. Excluded commands have host
+filesystem and network access and still follow Claude Code's permission policy. If that policy
+disallows unsandboxed calls, use the registered MCP tools. See
+[Claude Code's sandbox guidance](https://code.claude.com/docs/en/sandboxing#run-commands-outside-the-sandbox-with-excludedcommands).
+
 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

skills/lean-beam/references/setup-and-recovery.md

@@ -54,6 +54,19 @@ 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.
+- **Use the registered Beam MCP tools when each shell command runs in a separate network
+  namespace** (for example Claude Code on Linux/WSL2). A healthy `serve` owner can be unreachable:
+  CLI commands report `sessionRecoveryRequired`, and `doctor` reports recovery required. For CLI
+  use, the owner and every attaching command must share a network namespace.
+- **Do not run `recover` until you have independently confirmed that the matching owner, daemon,
+  and every other producer have stopped.** Connection refusal, `sessionRecoveryRequired`, and a
+  returned `remedy_command` do not establish this. If you cannot confirm shutdown, stop and
+  coordinate with the operator.
+- For CLI use in Claude Code, run both owner and clients outside the Bash sandbox: request
+  `dangerouslyDisableSandbox: true` on each Bash call, or
+  add `"sandbox": {"excludedCommands": ["lean-beam *"]}` to `.claude/settings.local.json` for direct
+  `lean-beam` calls, where client policy permits. See
+  [Claude Code's sandbox guidance](https://code.claude.com/docs/en/sandboxing#run-commands-outside-the-sandbox-with-excludedcommands).
 - 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