Add and activate disposable REPL execution

.github/workflows/tests.yml

@@ -2,6 +2,7 @@ name: tests
 
 on:
   push:
+    branches: [main, execution]
   pull_request:
 
 permissions:
@@ -24,3 +25,23 @@ jobs:
       - run: uv run ruff check autoform_cli servers tests
       - run: uv run pytest -q
       - run: make check-example
+
+  real-repl:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+      - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0
+        with:
+          version: "0.12.1"
+          python-version: "3.13"
+          enable-cache: true
+      - uses: leanprover/lean-action@50fcf42d2e460296f1a34b402e990d1b24f8b596 # v1
+        with:
+          auto-config: false
+          build: true
+          build-args: "Mathlib @repl/repl"
+          lake-package-directory: tests/fixtures/repl-smoke
+      - run: uv sync --extra dev --extra repl
+      - run: uv run pytest -q tests/test_real_repl.py
+        env:
+          AUTOFORM_RUN_REAL_REPL_TESTS: "1"

README.md

@@ -45,7 +45,10 @@ manifest is included, but Muse installation is not covered here.
 ## Quick start
 
 Work from an existing Lean repository. First scaffold the blueprint and site
-configuration from an Autoform checkout:
+configuration from an Autoform checkout. The project must declare
+`leanprover-community/repl` at an immutable revision compatible with its Lean
+toolchain; verify it first with `lake build @repl/repl` (the Setup skill selects
+and checks this pin):
 
 ```bash
 uv run autoform init /path/to/lean-project \

servers/README.md

@@ -10,16 +10,34 @@ when useful.
 Plugin hosts start the two stdio MCP processes automatically. They are
 lightweight adapters: the first Lean tool call race-safely starts a detached
 runtime for the current AutoformBot installation, Unix user, and compute node.
-That runtime owns one resident REPL pool and LSP session per active Lean
-project, so sessions using that installation reuse the same warmed processes.
-Closing the session that started it does not stop it; after a crash, the next
-tool call starts it again. Runtime sockets include a code fingerprint, so an
-in-place upgrade gracefully replaces the older build.
+That runtime owns one REPL admission pool and LSP session per active Lean
+project. Every public REPL call starts a fresh child and reaps it before
+returning, so environments, proof states, and stream contents cannot cross
+independent successful calls. If cleanup cannot be confirmed, Autoform returns
+an explicit no-replay error, quarantines that project pool, and blocks its
+replacement until cleanup succeeds. Before a child starts, Lean itself parses
+the submitted header (`lean --deps-json`) and imports outside the allowed roots
+(`Mathlib`, `Aesop`, `Batteries`, `LeanSearchClient` by default) are rejected.
+This keeps calls on known libraries; it is not a security sandbox, because the
+submitted Lean code can still run arbitrary `IO`. LSP sessions remain resident
+because their protocol is explicitly stateful. Closing the session that started
+the runtime does not stop it; after a crash, the next tool call starts it again.
+Runtime sockets include a code fingerprint, so an in-place upgrade gracefully
+replaces the older build.
 
-REPL and LSP processes remain lazy. A cold tool call stays pending while Lean
-warms up, so no `/repl-start`, `/lsp-start`, or model-side sleep is needed. Idle
-project processes are closed after 30 minutes by default, while the small
-runtime remains available. Its lifecycle is also explicit:
+Each consumer Lake project must declare `leanprover-community/repl` at an
+immutable revision compatible with its Lean toolchain. Autoform invokes the
+qualified target with `lake exe @repl/repl`, so a same-named executable in the
+root project cannot shadow the pinned dependency. `lake build @repl/repl`
+checks this contract when the toolchain or dependency revision changes.
+
+Lean subprocesses remain lazy. A REPL call stays pending while its fresh child
+starts, and the first LSP call stays pending while its session starts, so no
+`/repl-start`, `/lsp-start`, or model-side sleep is needed. Idle project slots
+and LSP sessions are closed after 30 minutes by default, while the small runtime
+remains available. The runtime currently requires POSIX process groups and Unix
+domain sockets; unsupported platforms fail before starting Lean. Its lifecycle
+is also explicit:
 
 ```bash
 uv run autoform-lean-runtime start
@@ -30,11 +48,27 @@ uv run autoform-lean-runtime stop
 `stop` is graceful: it waits for admitted tool calls and Lean children to
 finish shutting down before a subsequent `start` can replace the runtime.
 
+REPL transport retries are limited to failures detected before the complete
+request frame is dispatched. Once the final frame delimiter may have reached
+Lean, replay could execute the command twice, so Autoform retires the process
+and reports that the outcome is unknown instead of retrying.
+The REPL per-call timeout starts before the shared daemon is connected or
+started, then covers project admission, header validation, fresh child startup,
+idle-worker wait, and Lean execution. Verified process cleanup and response
+delivery get a separate bounded grace period before the RPC returns.
+
+`LEAN_REPL_CMD` is a trusted local command. Its descendants must remain in the
+dedicated process group Autoform creates; a command that deliberately detaches
+with a new session escapes that operating-system cleanup boundary.
+
 The private socket lives below `$XDG_RUNTIME_DIR/autoform`, falling back to a
 uid-specific directory in `/tmp`; the rotating runtime log is beside it.
 `AUTOFORM_RUNTIME_DIR` overrides that location. Node-wide limits are controlled
 by `AUTOFORM_REPL_TOTAL_WORKERS`, `AUTOFORM_REPL_WORKERS_PER_PROJECT`,
 `AUTOFORM_MAX_LEAN_PROJECTS`, and `AUTOFORM_LEAN_IDLE_SECONDS`. The first
 process to start the runtime supplies those settings until it is stopped.
+`get_repl_status` reports a project pool as `warm` when its admission slots are
+cached; it does not mean a Lean REPL child is resident between calls.
 `AUTOFORM_RUNTIME_RESPONSE_TIMEOUT` can raise the client/daemon response budget
-when unusually large worker pools need more than the default 15 minutes to warm.
+when a Lean operation and its verified child cleanup need more than the default
+15 minutes.