Isolate and validate public REPL calls

.github/workflows/tests.yml

@@ -119,6 +119,47 @@ jobs:
           AUTOFORM_REQUIRE_REAL_LEAN_TESTS: "1"
           AUTOFORM_REAL_LEAN_MATHLIB_PROJECT: ${{ runner.temp }}/autoform-created-project
 
+  real-repl:
+    name: real REPL (fixture toolchain)
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    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
+      - name: Install pinned Elan
+        run: |
+          set -euo pipefail
+          timeout --signal=TERM --kill-after=15s 2m curl -sSfL \
+            https://github.com/leanprover/elan/releases/download/v4.2.3/elan-x86_64-unknown-linux-gnu.tar.gz \
+            -o elan.tar.gz
+          echo "df0b2b3a439961ffcbb3985214365ffe40f49bc871df04dff268c7d8e21ca8b2  elan.tar.gz" \
+            | sha256sum --check --strict
+          tar xzf elan.tar.gz
+          ./elan-init -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      - name: Build the REPL fixture
+        working-directory: tests/fixtures/repl-smoke
+        run: |
+          set -euo pipefail
+          timeout --signal=TERM --kill-after=30s 5m \
+            elan toolchain install "$(tr -d '\r\n' < lean-toolchain)"
+          timeout --signal=TERM --kill-after=30s 8m lake build Mathlib Secret @repl/repl
+      - name: Install the minimum supported Lean toolchain
+        run: |
+          set -euo pipefail
+          timeout --signal=TERM --kill-after=30s 5m \
+            elan toolchain install "$(tr -d '\r\n' < tests/fixtures/minimum-lean/lean-toolchain)"
+      - name: Install locked development environment
+        run: timeout --signal=TERM --kill-after=30s 3m uv sync --frozen --extra dev --extra repl
+      - name: Run the REPL suite against the pinned upstream REPL
+        run: timeout --signal=TERM --kill-after=30s 10m uv run pytest -q tests/test_real_repl.py
+        env:
+          AUTOFORM_RUN_REAL_REPL_TESTS: "1"
+
   windows-hardening:
     name: Windows inspection, subprocess, and publication hardening
     runs-on: windows-latest

CONTRIBUTING.md

@@ -18,7 +18,10 @@ CI (`.github/workflows/tests.yml`) runs the same four steps on Python 3.10 and
 3.13 for every push and pull request. A separate job runs
 `tests/test_skeleton.py` and one `tests/test_project_inspect.py` test against a
 real Lean toolchain; another runs the inspection, bounded-subprocess, and
-transactional-output tests on Windows. Locally, tests that need Lean skip when
+transactional-output tests on Windows; a third builds
+`tests/fixtures/repl-smoke` and runs `tests/test_real_repl.py` against the
+pinned upstream REPL, also checking the header parser on the oldest Lean release
+Autoform supports. Locally, tests that need Lean skip when
 `lake` is not on `PATH`. The `tests/test_skeleton.py` ones also skip when the
 toolchain pinned in `tests/fixtures/skeleton-project/lean-toolchain` is
 missing; the others let elan download it. The `tests/test_library_generate.py`
@@ -28,6 +31,15 @@ job does; a missing toolchain or a failed download then fails them. Run
 `lake build` in `skills/setup/assets/cabannes-thesis-project` when you change
 the example's Lean sources or declarations.
 
+`tests/test_real_repl.py` skips unless `AUTOFORM_RUN_REAL_REPL_TESTS=1`. To run
+it locally, build its fixture and install the oldest supported toolchain first:
+
+```bash
+(cd tests/fixtures/repl-smoke && lake build Mathlib Secret @repl/repl)
+elan toolchain install "$(cat tests/fixtures/minimum-lean/lean-toolchain)"
+AUTOFORM_RUN_REAL_REPL_TESTS=1 uv run pytest -q tests/test_real_repl.py
+```
+
 ## Pull Requests
 We actively welcome your pull requests.
 

servers/README.md

@@ -10,16 +10,37 @@ 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 slot pool and LSP session per active Lean
+project. 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:
+LSP sessions stay warm; each public REPL call gets a fresh child and no
+process-owned environment or proof-state handle survives the response. Before
+that child starts, the selected Lake toolchain runs Lean's own header parser,
+which the REPL also uses, on the submitted source. Every import it reports must
+have one of the allowlisted roots `Mathlib`, `Aesop`, `Batteries`, or
+`LeanSearchClient` (a plain `Init` import is ignored), and a rejected or
+unrecognized parser response fails closed.
+Allowlisted imports require plain, nonempty canonical module components; names
+that remain quoted or path-like after Lean parsing are refused instead of being
+reduced to a misleading allowlisted root. The allowlist is a policy check, not a
+sandbox: each call runs with the runtime user's privileges, and `Init` alone
+provides file and process IO, for example `#eval IO.Process.run`. The header
+check runs as one extra short Lean process per call. Execution names the
+package-qualified `@repl/repl` target so a project target cannot shadow it.
+
+REPL children and LSP processes remain lazy. A tool call stays pending while
+Lean starts, so no `/repl-start`, `/lsp-start`, or model-side sleep is needed.
+Every REPL call starts Lean afresh and, unless its header starts with `module`
+or `prelude`, imports Mathlib, so it takes at least as long as `import Mathlib`
+on the node. Calls to the same project run one at a time unless
+`AUTOFORM_REPL_WORKERS_PER_PROJECT` is raised. The REPL `timeout` is one total
+post-admission budget for an idle-slot wait, header validation, child startup,
+generated imports, and submitted code; it and its cap default to 240 seconds.
+Project-cache admission uses the daemon response budget separately. Idle project
+state is closed after 30 minutes by default, while the small runtime remains
+available. Its lifecycle is also explicit:
 
 ```bash
 uv run autoform-lean-runtime start
@@ -45,7 +66,40 @@ 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.
-`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.
+`AUTOFORM_MAX_LEAN_PROJECTS`, and `AUTOFORM_LEAN_IDLE_SECONDS`. A REPL worker is
+one concurrent call slot; an idle slot holds no Lean process. The first process
+to start the runtime supplies those settings until it is stopped.
+
+`LEAN_REPL_CMD` selects the disposable child command. Its default,
+`lake exe @repl/repl`, finds the REPL only through a require named `repl`. For a
+require with any other name, rename the require to `repl`, or restart the
+runtime with `LEAN_REPL_CMD="lake exe @<name>/repl"` for a require named
+`<name>`, which applies to every project the runtime serves. A project with no
+REPL require, as `autoform project new` and `init` leave it, fails every REPL
+call until it adds one as the [setup skill](../skills/setup/SKILL.md) describes.
+When `LEAN_REPL_HEADER_CMD` is unset and `LEAN_REPL_CMD` starts with a `lake`
+executable, absolute or not, header validation reuses that executable without
+the command's other arguments. A container or other wrapper must also set
+`LEAN_REPL_HEADER_CMD` to a command that runs `servers/repl/parse_header.lean`
+with the matching toolchain's `lean --run`, passing the source on standard
+input. Like the limits above, `LEAN_REPL_CMD` and `LEAN_REPL_HEADER_CMD` are
+node-wide and read only when the runtime starts; after changing either, run
+`uv run autoform-lean-runtime stop`. The next process to start the runtime, an
+MCP adapter serving a tool call or `uv run autoform-lean-runtime start`, must
+have the new values in its environment, and
+`uv run autoform-lean-runtime status` shows the resolved commands under
+`config`.
+
+`AUTOFORM_MAX_REPL_REQUEST_SECONDS` caps the REPL `timeout`; when
+`AUTOFORM_REPL_REQUEST_TIMEOUT` is unset, the default `timeout` is the lower of
+240 seconds and that cap. If `LEAN_REPL_CMD` does not start with a `lake`
+executable and `LEAN_REPL_HEADER_CMD` is unset, if an explicit
+`AUTOFORM_REPL_REQUEST_TIMEOUT` exceeds that cap, or if that cap does not fit
+the response budget below, the runtime refuses to start, so the LSP tools are
+unavailable as well.
+
+`AUTOFORM_RUNTIME_RESPONSE_TIMEOUT` (default 15 minutes) bounds project
+admission, the tool operation, and a safety margin. Failed cleanup transfers to
+a retained background reaper and may continue past that response budget rather
+than allowing an overlapping replacement. A `warm` REPL project means its REPL
+slot pool is cached; it does not mean a REPL subprocess remains resident.

servers/lean_client.py

@@ -1,8 +1,8 @@
 """Client and bootstrap logic for Autoform's node-local Lean runtime.
 
 The two public MCP processes are intentionally short-lived stdio adapters.  A
-small detached process owns the expensive Lean REPL pools and LSP sessions and
-is reached through a private Unix-domain socket.
+small detached process owns the warm LSP sessions and the per-project REPL slot
+pools, and is reached through a private Unix-domain socket.
 """
 
 from __future__ import annotations

servers/lean_runtime.py

@@ -45,10 +45,9 @@
     LeanLspSession,
     format_lsp_diagnostics,
 )
-from servers.repl.core import DEFAULT_REPL_STARTUP_TIMEOUT, format_repl_response
+from servers.repl.core import default_header_command, format_repl_response
 from servers.repl.pool import (
     DEFAULT_RAM_FRACTION,
-    DEFAULT_STARTUP_STAGGER_SECONDS,
     LeanReplPool,
     LeanReplPoolConfig,
     LeanReplPoolStartupError,
@@ -62,7 +61,7 @@
 DEFAULT_IDLE_SECONDS = 30 * 60
 DEFAULT_LSP_TIMEOUT = 60.0
 DEFAULT_MAX_LSP_REQUEST_SECONDS = 600.0
-DEFAULT_REPL_REQUEST_TIMEOUT = 30.0
+DEFAULT_REPL_REQUEST_TIMEOUT = 240.0
 DEFAULT_MAX_REPL_REQUEST_SECONDS = 240.0
 DEFAULT_RPC_READ_TIMEOUT = 10.0
 DEFAULT_MAX_CONNECTIONS = 64
@@ -88,12 +87,8 @@ class _FailedResourceCreation:
 
 
 def _repl_creation_budget(worker_count: int) -> float:
-    """Bound victim cleanup, cold startup, and failed-start cleanup."""
-    return (
-        worker_count * DEFAULT_REPL_STARTUP_TIMEOUT
-        + max(0, worker_count - 1) * DEFAULT_STARTUP_STAGGER_SECONDS
-        + 2 * worker_count * REPL_WORKER_CLOSE_BUDGET
-    )
+    """Bound cleanup of an evicted pool; cold slots spawn no subprocesses."""
+    return worker_count * REPL_WORKER_CLOSE_BUDGET
 
 
 def _positive_int(name: str, default: int) -> int:
@@ -147,6 +142,7 @@ class LeanRuntimeConfig:
     repl_workers_per_project: int
     repl_project_limit: int
     repl_command: tuple[str, ...]
+    repl_header_command: tuple[str, ...]
     lsp_command: tuple[str, ...]
     lsp_timeout: float
     max_lsp_request_seconds: float
@@ -185,20 +181,33 @@ def from_environment(cls) -> "LeanRuntimeConfig":
                 "AUTOFORM_REPL_TOTAL_WORKERS"
             )
         repl_project_limit = min(max_projects, total_workers // workers_per_project)
-        repl_command = tuple(shlex.split(os.environ.get("LEAN_REPL_CMD", "lake exe repl")))
+        repl_command = tuple(shlex.split(os.environ.get("LEAN_REPL_CMD", "lake exe @repl/repl")))
+        raw_header_command = os.environ.get("LEAN_REPL_HEADER_CMD")
         lsp_command = tuple(shlex.split(os.environ.get("LEAN_LSP_CMD", "lake serve")))
         if not repl_command:
             raise ValueError("LEAN_REPL_CMD must not be empty")
+        if raw_header_command is not None:
+            repl_header_command = tuple(shlex.split(raw_header_command))
+            if not repl_header_command:
+                raise ValueError("LEAN_REPL_HEADER_CMD must not be empty")
+        elif Path(repl_command[0]).name == "lake":
+            repl_header_command = tuple(default_header_command(repl_command[0]))
+        else:
+            raise ValueError(
+                "LEAN_REPL_HEADER_CMD must be set when LEAN_REPL_CMD does not "
+                "start with a `lake` executable"
+            )
         if not lsp_command:
             raise ValueError("LEAN_LSP_CMD must not be empty")
-        repl_request_timeout = _positive_float(
-            "AUTOFORM_REPL_REQUEST_TIMEOUT",
-            DEFAULT_REPL_REQUEST_TIMEOUT,
-        )
         max_repl_request_seconds = _positive_float(
             "AUTOFORM_MAX_REPL_REQUEST_SECONDS",
             DEFAULT_MAX_REPL_REQUEST_SECONDS,
         )
+        # The default follows a lowered maximum, so the maximum can be set alone.
+        repl_request_timeout = _positive_float(
+            "AUTOFORM_REPL_REQUEST_TIMEOUT",
+            min(DEFAULT_REPL_REQUEST_TIMEOUT, max_repl_request_seconds),
+        )
         if repl_request_timeout > max_repl_request_seconds:
             raise ValueError(
                 "AUTOFORM_REPL_REQUEST_TIMEOUT cannot exceed "
@@ -226,7 +235,7 @@ def from_environment(cls) -> "LeanRuntimeConfig":
         ):
             raise ValueError(
                 "AUTOFORM_RUNTIME_RESPONSE_TIMEOUT is too small for the configured "
-                "REPL worker startup and request limits"
+                "REPL pool replacement and request limits"
             )
         if (
             LSP_CLOSE_BUDGET
@@ -246,6 +255,7 @@ def from_environment(cls) -> "LeanRuntimeConfig":
             repl_workers_per_project=workers_per_project,
             repl_project_limit=max(1, repl_project_limit),
             repl_command=repl_command,
+            repl_header_command=repl_header_command,
             lsp_command=lsp_command,
             lsp_timeout=lsp_timeout,
             max_lsp_request_seconds=max_lsp_request_seconds,
@@ -270,6 +280,7 @@ def as_dict(self) -> dict[str, Any]:
             "repl_workers_per_project": self.repl_workers_per_project,
             "repl_project_limit": self.repl_project_limit,
             "repl_command": list(self.repl_command),
+            "repl_header_command": list(self.repl_header_command),
             "lsp_command": list(self.lsp_command),
             "lsp_timeout": self.lsp_timeout,
             "max_lsp_request_seconds": self.max_lsp_request_seconds,
@@ -818,8 +829,8 @@ def default_repl_factory(
                     LeanReplPoolConfig(
                         cwd=str(project_dir),
                         repl_command=list(self.config.repl_command),
+                        header_command=list(self.config.repl_header_command),
                         num_repls=self.config.repl_workers_per_project,
-                        max_retries=0,
                     )
                 )
             except LeanReplPoolStartupError as error:
@@ -846,6 +857,7 @@ def default_lsp_factory(
             lambda pool: pool.shutdown(),
             max_entries=self.config.repl_project_limit,
             idle_seconds=self.config.idle_seconds,
+            is_valid=lambda pool: not pool.requires_retirement,
             start_sweeper=start_sweepers,
         )
         try:
@@ -886,13 +898,19 @@ def dispatch(self, method: str, params: dict[str, Any]) -> Any:
                     "timeout exceeds the node-wide limit of "
                     f"{self.config.max_repl_request_seconds:g} seconds"
                 )
-            with self.repl_projects.lease(
-                project_dir,
+            root = resolve_lean_project_dir(project_dir)
+            with self.repl_projects.lease_resolved(
+                root,
                 acquisition_timeout=self._acquisition_timeout(effective_timeout),
                 creation_budget=self.repl_creation_budget,
             ) as pool:
                 assert pool is not None
-                return format_repl_response(pool.run(code, timeout=effective_timeout))
+                try:
+                    result = pool.run(code, timeout=effective_timeout)
+                finally:
+                    if pool.requires_retirement:
+                        self.repl_projects.invalidate_resolved(root, pool)
+                return format_repl_response(result)
         if method == "repl.status":
             project_dir = self._string_param(params, "project_dir")
             with self.repl_projects.observe(project_dir) as (pool, state):

servers/repl/__init__.py

@@ -1,4 +1,4 @@
-"""Lean REPL server and process pool."""
+"""Lean REPL server and per-project slot pool."""
 
 from .core import LeanRepl, LeanReplConfig
 from .pool import LeanReplPool, LeanReplPoolConfig, LeanReplPoolStartupError