Add and activate disposable REPL execution

[Deicyde]

Stack position: 2 of 3. Builds on #13 (merged as afaf215). The generation-isolation slice follows as a separate PR once this lands.

This PR introduces LeanRepl.run_disposable() and routes every public pooled REPL call through it. Each call gets a fresh child, exactly one request frame, strict response validation, and verified process-group cleanup before a result is returned.

The cutover also:

• carries one absolute operation deadline across daemon startup, project admission, header validation, worker startup, and execution, with separate bounded cleanup grace;
• validates strict private request and response envelopes;
• never replays a request after dispatch may have occurred;
• returns typed pre-dispatch errors and explicit outcome-unknown failures;
• removes process-owned env and proofState handles;
• bounds REPL responses and header-parser stdout/stderr;
• quarantines a project pool when child cleanup cannot be verified, while keeping pool-shutdown deadlines aggregate;
• validates the original submitted header with the active toolchain's lean --deps-json, before adding warmup imports, and accepts the known Lean 4.19 and current output schemas strictly;
• resolves the parser through Lake's LEAN_SYSROOT, so a project executable cannot shadow lean;
• invokes the package-qualified @repl/repl target and documents the required immutable consumer dependency;
• pins the tested upstream REPL revision for Lean 4.32.2 in the setup example and real-REPL fixture;
• exercises consecutive isolated calls through the public client, daemon, pool, and REPL path in CI.

Import filtering limits calls to known libraries; it is not a security sandbox, because submitted Lean can still run arbitrary IO.

Validation: Ruff, the full Python suite, the setup example check/render, both pinned REPL builds, and 11 real-REPL tests pass locally. The cleanup-grace fix from #13 is preserved.

[Deicyde]

Please replace the hand-written header scanner (_header_import_modules, servers/repl/core.py:298) with Lean's own header parser, via lean --deps.

Right now the allowlist check depends on a Python reimplementation of Lean's header grammar. It matches Lean on every case tried so far, but any gap between the two is an allowlist bypass, and the grammar changes across Lean versions (module, public/meta import, import all are recent). Lean already ships the parser we need:

• lean --deps file.lean parses the header with Lean's real parser and prints the resolved file for each direct import. Run it under the worker's lake env so it resolves against the same search path as the REPL.
• On Lean 4.32.0 it handled all the tricky headers correctly: comments before and between imports, several imports on one line, comments inside a module name, module/public import/import all, prelude, and an import after the body.
• An unresolvable module makes it exit nonzero, so failure rejects by default.
• Each call took well under a second, which is small next to the fresh Mathlib-importing REPL each disposable run already starts.

Suggested shape:

1. Write the submitted code to a temp file and run lake env lean --deps <file> with the remaining deadline.
2. Nonzero exit or timeout: return Rejected Lean header: ... with Lean's stderr.
3. Map each printed path back to a module name by stripping the LEAN_PATH entry it sits under and the .olean suffix, then check the root against allowed_imports as today. Skip the implicit Init entries.
4. Delete _header_import_modules and the special-case rejections for module/prelude/modifiers, since Lean now handles those.
5. Keep the existing adversarial header cases as tests against the new path. They make good regression tests for the --deps integration.

Optional, same PR or a follow-up: the stateful run() path still uses the line-based _split_imports_and_body for its allowlist check (core.py:400). It isn't exploitable today, because stripped-header code reaching Lean as body can't import anything, but using one parser for both paths would remove the second copy of the header rules.

A compiled Lean helper built on Lean.Parser.parseHeader + Elab.headerToImports also works and returns module names directly. --deps is preferred because it needs no extra build artifact tied to the toolchain.

[Deicyde]

Superseded by the direct Lean Beam persistent-session architecture in draft #46. That replacement removes the custom REPL/runtime stack instead of extending disposable child execution. The branch remains available for history; #46 is explicitly blocked from merge until its upstream Beam release gates are satisfied.

[Deicyde]

Restored for active work as draft #101 on a facebookresearch-owned branch. The replacement is merged with current main and preserves the original REPL safety design without resuming development on the old fork branch.

[Deicyde]

Update: draft #101 was decomposed and closed. Active replacements are #105 (minimal disposable lifecycle), #106 (Lean-native header validation and pinned dependency), and #107 (fault injection and real-REPL CI).