Execute structured Lean imports in isolated REPLs

.github/workflows/tests.yml

@@ -22,5 +22,35 @@ jobs:
           enable-cache: true
       - run: uv sync --extra dev --extra repl
       - run: uv run ruff check autoform_cli servers tests
-      - run: uv run pytest -q
+      - run: make test
       - run: make check-example
+
+  real-lean:
+    name: real Lean (pinned v4.32.2)
+    runs-on: ubuntu-latest
+    timeout-minutes: 45
+    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
+      - run: uv sync --frozen --extra dev --extra repl
+      - name: Install pinned Lean
+        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"
+          timeout --signal=TERM --kill-after=30s 10m \
+            "$HOME/.elan/bin/elan" toolchain install leanprover/lean4:v4.32.2
+          version="$("$HOME/.elan/bin/elan" run leanprover/lean4:v4.32.2 lean --version)"
+          grep -Fq "Lean (version 4.32.2" <<<"$version"
+      - name: Run mandatory real-Lean tests
+        run: timeout --signal=TERM --kill-after=30s 25m make test-real-lean

Makefile

@@ -1,12 +1,15 @@
-.PHONY: setup test lint check-example
+.PHONY: setup test test-real-lean lint check-example
 
 THESIS_EXAMPLE := skills/setup/assets/cabannes-thesis-project
 
 setup:
 	uv sync --extra dev --extra repl
 
 test:
-	uv run pytest -q
+	uv run pytest -q -m "not real_lean"
+
+test-real-lean:
+	uv run pytest -q -m real_lean
 
 lint:
 	uv run ruff check autoform_cli servers tests

pyproject.toml

@@ -43,5 +43,12 @@ dev = [
 [tool.hatch.build.targets.wheel]
 packages = ["autoform_cli", "servers"]
 
+[tool.pytest.ini_options]
+addopts = "--strict-markers"
+markers = [
+    "daemon: detached shared Lean runtime lifecycle and process tests",
+    "real_lean: integration tests that require the pinned Lean/Lake toolchain",
+]
+
 [tool.ruff]
 line-length = 120

servers/README.md

@@ -36,5 +36,11 @@ uid-specific directory in `/tmp`; the rotating runtime log is beside it.
 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_REPL_REQUEST_TIMEOUT` sets the default end-to-end REPL call budget
+(180 seconds), bounded by `AUTOFORM_MAX_REPL_REQUEST_SECONDS`. The client-side
+`AUTOFORM_RUNTIME_RESPONSE_TIMEOUT` must remain above the node-wide request
+limits.
+
+`run_lean_code` accepts an optional ordered `imports` list for project modules
+that Lake has already built. Nonempty lists are validated against the project,
+executed in a fresh REPL process, and retired after that request.

servers/__init__.py

@@ -6,9 +6,85 @@
 
 from __future__ import annotations
 
+import os
+from dataclasses import dataclass
 from pathlib import Path
 
 LAKE_PROJECT_MARKERS = ("lakefile.lean", "lakefile.toml", "lake-manifest.json")
+LEAN_PROJECT_CONFIG_FILES = (
+    "lean-toolchain",
+    "lake-manifest.json",
+    "lakefile.toml",
+    "lakefile.lean",
+)
+_SCRUBBED_LAKE_ENVIRONMENT = frozenset(
+    {
+        "ELAN_TOOLCHAIN",
+        "LAKE",
+        "LAKE_ARTIFACT_CACHE",
+        "LAKE_CACHE_ARTIFACT_ENDPOINT",
+        "LAKE_CACHE_DIR",
+        "LAKE_CACHE_KEY",
+        "LAKE_CACHE_REVISION_ENDPOINT",
+        "LAKE_CACHE_SERVICE",
+        "LAKE_CONFIG",
+        "LAKE_HOME",
+        "LAKE_NO_CACHE",
+        "LAKE_PKG_URL_MAP",
+        "LAKE_RESTORE_ARTIFACTS",
+        "LEAN",
+        "LEAN_AR",
+        "LEAN_CC",
+        "LEAN_GITHASH",
+        "LEAN_PATH",
+        "LEAN_SRC_PATH",
+        "LEAN_SYSROOT",
+        "PYTHONPATH",
+    }
+)
+
+
+def clean_lake_environment() -> dict[str, str]:
+    """Return the host environment without ambient Lean/Lake path overrides."""
+    environment = os.environ.copy()
+    for name in _SCRUBBED_LAKE_ENVIRONMENT:
+        environment.pop(name, None)
+    return environment
+
+
+@dataclass(frozen=True, slots=True)
+class ProjectFingerprint:
+    """Filesystem identity of a project root and its Lean configuration."""
+
+    root: tuple[int, int, int]
+    files: tuple[tuple[str, int, int, int, int, int, int], ...]
+
+
+def lean_project_fingerprint(project_dir: Path) -> ProjectFingerprint:
+    """Return the project metadata that makes resident Lean state stale."""
+    root = project_dir.stat()
+    fingerprint: list[tuple[str, int, int, int, int, int, int]] = []
+    for name in LEAN_PROJECT_CONFIG_FILES:
+        path = project_dir / name
+        try:
+            info = path.stat()
+        except FileNotFoundError:
+            continue
+        fingerprint.append(
+            (
+                name,
+                info.st_dev,
+                info.st_ino,
+                info.st_mode,
+                info.st_size,
+                info.st_mtime_ns,
+                info.st_ctime_ns,
+            )
+        )
+    return ProjectFingerprint(
+        root=(root.st_dev, root.st_ino, root.st_mode),
+        files=tuple(fingerprint),
+    )
 
 
 def resolve_lean_project_dir(project_dir: str) -> Path:

servers/lean_client.py

@@ -28,20 +28,23 @@
 DEFAULT_STARTUP_TIMEOUT = 15.0
 PACKAGE_ROOT = Path(__file__).resolve().parent.parent
 INSTALL_PATH_ID = hashlib.sha256(os.fsencode(PACKAGE_ROOT)).hexdigest()[:10]
+_RUNTIME_FILES = (
+    PACKAGE_ROOT / "servers" / "__init__.py",
+    Path(__file__).resolve(),
+    PACKAGE_ROOT / "servers" / "lean_runtime.py",
+    PACKAGE_ROOT / "servers" / "lsp" / "server.py",
+    PACKAGE_ROOT / "servers" / "repl" / "__init__.py",
+    PACKAGE_ROOT / "servers" / "repl" / "server.py",
+    PACKAGE_ROOT / "servers" / "repl" / "core.py",
+    PACKAGE_ROOT / "servers" / "repl" / "imports.py",
+    PACKAGE_ROOT / "servers" / "repl" / "pool.py",
+)
 
 
 def _build_id() -> str:
     """Fingerprint code that can change persistent runtime behavior."""
     digest = hashlib.sha256()
-    runtime_files = (
-        PACKAGE_ROOT / "servers" / "__init__.py",
-        Path(__file__).resolve(),
-        PACKAGE_ROOT / "servers" / "lean_runtime.py",
-        PACKAGE_ROOT / "servers" / "lsp" / "server.py",
-        PACKAGE_ROOT / "servers" / "repl" / "core.py",
-        PACKAGE_ROOT / "servers" / "repl" / "pool.py",
-    )
-    for path in runtime_files:
+    for path in _RUNTIME_FILES:
         try:
             digest.update(path.read_bytes())
         except OSError:
@@ -51,15 +54,8 @@ def _build_id() -> str:
 
 def _build_generation() -> int:
     """Order in-place builds so an older live wrapper cannot replace a newer one."""
-    candidates = (
-        Path(__file__).resolve(),
-        PACKAGE_ROOT / "servers" / "lean_runtime.py",
-        PACKAGE_ROOT / "servers" / "lsp" / "server.py",
-        PACKAGE_ROOT / "servers" / "repl" / "core.py",
-        PACKAGE_ROOT / "servers" / "repl" / "pool.py",
-    )
     mtimes: list[int] = []
-    for path in candidates:
+    for path in _RUNTIME_FILES:
         try:
             mtimes.append(path.stat().st_mtime_ns)
         except OSError:
@@ -337,12 +333,13 @@ def ensure_running(self) -> dict[str, Any]:
             os.close(lock_fd)
 
     def stop(self) -> dict[str, Any]:
-        """Ask a running daemon to finish active calls and shut down."""
+        """Ask a running daemon to finish active calls within one deadline."""
+        deadline = time.monotonic() + self.response_timeout
         try:
             result = self.request(
                 "daemon.shutdown",
                 autostart=False,
-                response_timeout=10.0,
+                response_timeout=min(self.response_timeout, 10.0),
             )
         except LeanRuntimeUnavailable:
             stopped = self._stop_previous_builds()
@@ -351,7 +348,6 @@ def stop(self) -> dict[str, Any]:
             raise
         if not isinstance(result, dict):
             raise LeanRuntimeProtocolError("daemon.shutdown returned a non-object result")
-        deadline = time.monotonic() + self.response_timeout
         while self.paths.socket.exists() and time.monotonic() < deadline:
             time.sleep(0.025)
         if self.paths.socket.exists():