Review notes: leanprover/lean4#13948 (feat(lake): wrapped exec) — Claude + Codex

wrapped-exec-review.md

Review notes: feat(lake): wrapped exec (#13948)

A skeptical review of the $LAKE_WRAPPED_EXEC hook, cross-checked by Claude (Opus 4.8) and OpenAI Codex. Both read the PR branch directly; every concern below was independently confirmed against the code.

Solid

• The Build/Actions.lean refactor is behavior-preserving. mkLeanModuleArgs / mkCcCompileArgs preserve argv order, escapeRspArg is the same escaping factored out, and compileLeanModule keeps the same createParentDirs calls.
• The unset path matches upstream for the spawn itself — runRawProcOrWrapped falls through to rawProc with the same logging.

Concerns

1. The input-closure walk runs unconditionally, even when the hook is off. Module.buildLean calls collectLeanInputClosure mod on every module build regardless of $LAKE_WRAPPED_EXEC; the "effectively unused when unset" comment is wrong — it's still computed (a full transitive import-graph walk per module, allocating NameSet/Array, awaiting input.fetch per node). The awaits are usually cheap (jobs already scheduled), so this isn't re-elaboration, but it's unconditional extra work that undercuts the "byte-for-byte identical when unset" claim. Severity unmeasured. Fix: guard on (← IO.getEnv "LAKE_WRAPPED_EXEC").isSome.

2. inputs is incomplete for the sandbox use-case the PR motivates. inputs = #[leanFile, setupFile] ++ extraInputs, and extraInputs holds only workspace .olean/.ir/.olean.server/.olean.private — not setup.dynlibs / setup.plugins, which lean loads at runtime. A read-allow-listing wrapper would block lean for any precompileModules project. Toolchain oleans are handled out-of-band via toolchain_root (fine, documented), so inputs is explicitly not the complete read-set. (A write-only sandbox is unaffected — it never consults inputs.)

3. No tests. 4 files / 594 insertions, zero test files, for a core-compile-path change — despite the doc spelling out the ideal regression test (LAKE_WRAPPED_EXEC=./wrapper-passthrough ⇒ byte-for-byte identical to plain lake build).

4. No in-tree consumer; speculative public API. Nothing uses the hook, and renderRspContents is dead code (public, called by nobody; mkArgs uses private escapeRspArg). The public helpers exist only for out-of-tree tooling. Worth trimming — and raises whether a consumer-less, generically-described hook belongs in core yet.

5. WRAPPED_EXEC.md reads as a PR writeup, not durable docs. 301 lines at src/lake/WRAPPED_EXEC.md opening with "This branch adds…" / "The patch is two commits…". Will rot on merge; if kept, rewrite/trim and move to where Lake docs live.

Minor

• Temp-manifest leak on wrapper-spawn failure. runViaWrapper removes the manifest only on .ok (a nonzero wrapper exit is still .ok and cleaned up; a spawn failure goes .error and leaks).
• env fidelity. Serialized as a JSON object, but SpawnArgs.env is an ordered Array (String × Option String) — loses ordering/duplicate keys, and filterMap drops none (unset-var) entries. Benign for the current lean call; less faithful than the doc claims once more call sites are hooked.
• quiet ignored on the wrapped path (runViaWrapper always logVerboses). Harmless for the one caller.

Net

The refactor is mergeable on its own. The feature is carefully designed to be inert-when-off, but as submitted it (1) isn't, due to the unconditional walk; (2) ships no tests while documenting the exact one it omits; (3) adds dead/speculative public API with no consumer; (4) has a known-incomplete inputs set for its headline use-case. Suggested before landing: the env-var guard, the passthrough test, removal of renderRspContents, and a decision on whether a consumer-less hook + 300-line spec belongs in core.