Validate REPL imports with the selected Lean toolchain

[Deicyde]

Problem

The disposable path found imports with a string splitter. A leading comment hid import Unsafe from the allowlist, and prefixing warmup imports onto a module or prelude header turned a valid file into an invalid one. A project target named repl could also shadow the REPL executable.

Fix

• LeanRepl._check_header runs the Lake toolchain's lean --deps-json on the submitted code. A launcher execs $LEAN_SYSROOT/bin/lean, so a PATH shadow cannot substitute the parser.
• The parser runs as the slot's process generation: same close(), same pool retry, same is_clean() gate as the REPL child. No separate cleanup path.
• Time and combined output are bounded; a strict decoder fails closed on rejected, unknown, duplicate-key, or nonstandard output.
• The allowlist checks Lean's complete import set plus the warmup roots.
• Warmup imports are prefixed only when current-schema metadata proves an ordinary header. module, prelude, and legacy-schema headers are sent unchanged.
• The default REPL command is lake exe @repl/repl. Setup states that neither project new nor init adds the REPL, requires an immutable, toolchain-tested REPL revision, and the bundled example pins one.

Invariant

No REPL child starts for a header Lean rejects or Autoform cannot decode, and the parser process is reaped before the slot is reused.

Tests

• tests/test_repl_core_protocol.py: current and legacy schemas, launcher ignores a PATH shadow, fail-closed parametrization (Lean errors, nonzero exit, garbage, duplicate keys, NaN), header checked before the warmup prefix, warmup prefix only on proven ordinary headers (5 cases), disallowed warmup root.
• tests/test_shared_lean_runtime.py: package-qualified default command.
• tests/test_skill_examples.py: docs and the example lakefile pin the REPL revision.
• Exact-head GitHub CI: Python 3.10/3.13, Windows, real Lean, CLA.

Stack

10 files, +609/-8 against #105 (was +847/-9 before golfing; most remaining data lines are the example's lake-manifest.json). Merge after or together with #105.

Behavior note: if a request is cancelled while the parser runs and the parser's cleanup also fails, the wrapper stays dirty and the pool's _settle reaps it, the same as for a REPL child.

[Deicyde]

Exact-head review is complete at 76c6eb05. Lean remains the sole header parser; current-schema metadata prevents speculative warmup imports from corrupting module or prelude, while legacy output remains allowlist-compatible and is never rewritten without proof. The reviewed parser patch is byte-identical after the #105 restack, focused tests pass, and every required check is green. Ready after #105.

[Deicyde]

Swarm pass on header validation, the middle of the #105 → #106 → #107 stack.

What changed and why

• 4552041 (golf): _check_header runs lean --deps-json as the slot's own process generation (self.process), so the parser shares close(), the pool's _settle retry, and the is_clean() gate with the REPL child. That removed the module-level parser helpers, _HeaderProcessCleanupError, and a second cleanup path. Decoder errors collapse into one fail-closed ValueError.
• f3da058 (golf): parametrized the warmup-prefix cases (5) and the fail-closed cases, and added a nonzero-exit case.
• Merged Isolate and validate public REPL calls #105 forward (097168f, 1fe0d62, 208e48d, f96c69e), which carries main at 4cf7f9e. f96c69e resolves the skills/setup/SKILL.md conflict with Create Lean projects atomically with catalog-backed defaults #96: main's project new text stays verbatim, and the REPL paragraph now says that neither project new nor init adds the REPL.

Diff vs #105: +847/-9 → +609/-8 (10 files; 106 lines are the example lake-manifest.json).

Checks: exact-head CI on f96c69e: Python 3.10/3.13, Windows, real Lean, CLA (pull_request, push). Locally: ruff, plus the REPL core, pool, shared-runtime, and skill-example tests (daemon timing tests excluded locally because of machine load; CI ran them).

Remaining risks

• Behavior change at LeanRepl level: a request cancelled during parsing whose parser cleanup also fails leaves the wrapper dirty for the pool to reap, instead of retrying inline. Under the pool this is the same path as a REPL child.
• Header parsing adds one lake env spawn per call inside the call's timeout.
• Legacy deps-json output is accepted for the allowlist but never gets the warmup prefix.
• project new (Create Lean projects atomically with catalog-backed defaults #96) does not declare the REPL dependency, so a new project needs the manual pin the setup docs describe before the REPL tool works. Having the creator pin a tested REPL revision per catalog release is a separate change.

Posted by PR swarm: Swarm · REPL #105-107