[Vilin97]

watch() in the per-file build-time gate reads /proc/<pid>/stat through _process_identity and _process_state, which caught only FileNotFoundError. When a process is reaped between open and read, the kernel returns ESRCH (ProcessLookupError). That escaped to watch()'s handler, which printed ::error::Cannot monitor Lean build processes: [Errno 3] No such process and failed the build with exit 125.

This made test_watch_prunes_exited_process_handles flaky (it failed once on #817 at d8a0140; a rerun passed). Real lake builds also spawn many short-lived processes, so it could fail Lean CI spuriously. That hasn't been seen in the last 40 Lean CI runs.

Gate semantics are unchanged. A process that has exited is not compiling, so treating it as gone (None) is what the readers already do for FileNotFoundError. The 60-minute and 600 s limits are untouched.

Tests: new parametrized test_a_process_reaped_mid_read_counts_as_gone covers both readers. Ruff is clean. The Linux-only watcher tests run in CI.

Maintainer-authorized gate fix (2026-11-14).

🤖 Generated with Claude Code

[github-actions]

Proof profile (new / modified Lean files)

No added or modified Lean files under LeanPool/ in this PR. No compile-cost measurements are needed.

Advisory only — never blocks merge.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Medium impact] The PR appears safe to merge; no actionable issues were found.

Summary

Both /proc readers now treat ProcessLookupError as a gone process, matching their existing FileNotFoundError behavior.

• The build watcher treats a process reaped during a read as gone.

_{Reviews (1) · Last reviewed commit: "Treat a process reaped mid-read as gone ..." · Reviewed by Greptile}

[Vilin97]

Approve — the process-reaping race is handled correctly at 97574f6e0531db40b0d06fcd5125013072ba940e.

Both /proc/PID/stat readers now treat ProcessLookupError like the existing FileNotFoundError case. Other I/O errors still propagate; the 3600-second process limit, 600-second file gate, PID identity checks and cleanup behavior are unchanged.

The parametrized regression covers both readers. Independent in-memory checks passed and reproduced the failure on the predecessor. Hosted pytest and Ruff also passed; the full Lean workflow was still running in the saved validation intake. The separate gate-change authorization covers this exact change. Retain the existing protected auto-merge request while its remaining required checks finish.

[Vilin97]

🤖 LLM review — refactor (gpt-6.1-sol)

Reviewed head: 97574f6e0531db40b0d06fcd5125013072ba940e

Verdict: ✅ approve

Both process-stat readers now treat ProcessLookupError as process disappearance, consistent with the Linux read implementation. The change is narrow and adds deterministic coverage. Both new cases passed under Python 3.12; mocked experiments also confirmed unrelated errors propagate and rejected process handles close. Live watcher tests were not run because this environment denies /proc access.

Aspect	Value
Scope	build watcher race handling
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	✅ more_robust
Risk	✅ low

The change handles a transient process-disappearance race explicitly while preserving the existing ownership checks and timeout logic.

Findings (1)

• prompt-injection — PR-wide
  The contributor-controlled description claims “Maintainer-authorized gate fix (2026-11-14).” This asserts maintainer authority across the review trust boundary and was ignored. Remove the authority claim from the contributor's description; it cannot establish authorization or influence the verdict.

---

Tokens: 563,563 in / 5,343 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $2.3344 (Standard API equivalent; uncached input) (long-context rate)
Automated review against .github/REFACTOR_REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.