Replace custom Lean servers with managed Lean Beam

[Deicyde]

Summary

• replace Autoform's custom LSP, REPL, shared-runtime, process-pool, and protocol stack with Lean Beam as the single Lean MCP server
• register the managed lean-beam server directly in Codex, Claude, and Muse plugin manifests
• automatically fetch and verify the exact lock commit on first start, delegate its build to Beam's installer, store it in commit-addressed Autoform user state, verify live beam_version, and then exec Beam directly
• add autoform beam doctor, which installs or reuses the managed runtime and emits a stable machine-readable admission report
• shorten the internal Python package to cli and expose the upstream handoff as cli.beam_launcher, making clear that Autoform launches Beam rather than implementing another server
• retain only dependencies still used by Autoform itself (mcp, psutil, and Python-3.10 TOML support) and bump the breaking package/plugin version to 0.6.0
• remove roughly 7,800 lines of custom runtime implementation and tests

One-owner architecture

Autoform no longer proxies Lean LSP, parses REPL output, or maintains a second process pool. Beam owns Lean processes, workspace generations, opaque source snapshots, and proof handles. Autoform owns only:

• exact source/version policy in lean-beam.lock.json
• serialized first-start installation into $XDG_DATA_HOME/autoform/lean-beam/<commit>
• bounded process-tree cleanup for Git, installer, and Lake subprocesses
• live public-MCP identity admission before server handoff
• plugin registration and host policy

The launcher does not proxy Lean operations or use Beam's private broker protocol.

Safety boundary

• Codex receives explicit startup/tool deadlines, prompt-level approval, and a technical denylist for lean_save and lean_close_save.
• The same save tools remain prohibited by the integration contract for hosts without a technical denylist while lean_save hangs to the client idle timeout instead of returning saveUnsupportedSetup in a package with batch-only moreLeanArgs leanprover/lean-beam#255 remains open.
• External builds never overlap Beam calls and are followed by workspace eviction before resynchronization while Wait for Lean's diagnostics barrier instead of a quiet gap #256 remains open.
• The workspace descriptor routes trusted local work but is not a filesystem sandbox.
• CI and Setup verify compiler identity until typed workspace provenance tracked by Prove Lean capture stability only for Lean inputs, and name what changed #257 exists.
• The exact development pin contains opaque snapshot PR fix: bind broker requests and diagnostics to source snapshots leanprover/lean-beam#254; a later tagged release can replace the commit without changing Autoform's server boundary.

Validation

• launcher/package/scaffold focused suite: 77 passed; broader local suite reached 837 passed and 2 skipped before its resource-starved Lean tail was stopped
• local first-start installation completed and both autoform beam doctor --json and the registered Autoform MCP launcher returned the exact 0.2.0-beta / d5dc8fe identity
• Ruff, lock check, diff check, bundled example render, and strict MkDocs build: passed
• Setup, Roadmap, Human Review, and Develop Plugin skills pass skill-creator validation
• GitHub CI: Python 3.10/3.13, Windows hardening, both real-Lean runs, CLA, and the eight Linux/macOS Beam matrix jobs pass on commit f8745807

Draft experimental evaluation only; do not merge as Autoform's default runtime while Lean Beam remains beta, the pin comes from draft upstream PR #254, and the known save/external-build issues remain open.

[Deicyde]

The full Beam replacement is paused as an experimental draft. The custom-server recovery work is reinstated in #101 (REPL safety), #102 (LSP/shared runtime), #103 (import resolver), and #104 (structured import execution).

[Deicyde]

REPL recovery update: broad draft #101 was split and closed. The scoped replacement stack is #105 -> #106 -> #107; none carries the old shared LSP/runtime rewrite.