[Vilin97]

Why

One slow file can stall all of CI. In the last full rebuild (merge-queue run 42209045242), MovingSofa's certificate files took up to 865 s each and pushed one shard to 4h08m. That pushed a full-pool rebuild past the merge queue's 6-hour limit, and #751 timed out three times. This adopts Tau Ceti's CI performance gate, with the limits the maintainer chose.

What changes

• 60-minute hard limit. Every CI lake build (single build, shards, assemble, rebased root) runs under python -m lean_pool.build_time_limits watch.
  • It polls the process table every 15 s and sends SIGTERM to any lean process under the build that has run longer than 60 minutes, then SIGKILL after 30 s.
  • The build then fails with exit 124 and a ::error file=… annotation naming the file.
• 600 s per added or modified file. After the warning scan, build_time_limits check reads Lake's Built <module> (<time>) lines from the build log.
  • It fails when a LeanPool/**/*.lean file that the PR adds or modifies, measured against the PR, merge-group or push base, took more than 600 s.
  • Files the PR does not touch are not checked, so existing slow files don't block unrelated PRs.
  • A changed file replayed from cache was compiled, and checked, by the earlier successful run it came from.
• Docs. .github/CODE_QUALITY.md, CONTRIBUTING.md, CLAUDE.md and AGENTS.md document both limits.

Measured impact on the current pool

From every module time in run 42209045242 (31,177 pool files):

• 0 files come close to the 60-minute limit; the slowest is 865 s.
• 15 files exceed 600 s. All are in MovingSofa: 14 GerverSofa.KernelOnly.PartE.Certificates.Bundle* files plus Core.Bundle003.
  • They are only checked when a PR modifies them.
  • A Codex session on the Lean VM is already optimizing MovingSofa to bring every file under 600 s.
• A version-bump PR that has to edit one of those 15 files would trip the check until then.

Differences from Tau Ceti

• What is timed. We use Lake's wall-clock times from the real build log, which needs no extra job. Tau Ceti counts retired instructions, or uses same-runner CPU time, in a separate perf job.
• No slowdown rule for modified files yet. Tau Ceti also fails a modified file that gets 1.5× and 30 s slower than at base. That needs base-side timings; the advisory /profile comparison already measures them and could become that gate later.

Verification

• New tests in python/tests/test_build_time_limits.py cover:
  • ps time formats;
  • descendant-only process selection;
  • log parsing, ignoring facets like :c.o and other libraries;
  • added versus untouched files, in a real git repository;
  • a real watchdog kill, using a lean-named sleep;
  • passing through the build's exit status.
• ruff check, ruff format and actionlint pass.
• Full pytest: 885 pass. The same 4 tests fail on main: test_notice (NOTICE is stale on main) and 3 macOS-only test_proof_profile cases.

This changes CI gates, authorized by the maintainer (@Vilin97) in a Claude Code session on 2026-11-06.

🤖 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; both previous findings are addressed.

Summary

This PR adds a 60-minute limit for each Lean process and a 600-second budget for changed pool files.

• CI stops long Lean compiles and rejects slow changed files.

_{Reviews (2) · Last reviewed commit: "Never reuse builds compiled before the b..." · Reviewed by Greptile}

[Vilin97]

Source133 — current head 1403b38ee7229e551dc52db82acdff1ed0cc0534, all ten authored paths reviewed. Technical verdict: changes requested.

The new PINNED_INPUTS entry fixes the project-artifact reuse path, and the untouched-900s / changed-300s regression now tests the intended exemption. Those published findings are resolved. Two issues remain:

1. P2 — the direct whole-build cache still lacks the timing-policy boundary. The LeanPoolBuild-v1 lookup/restore keys use the three configuration files and ci_cache.build_revision’s Lean-only source identity; they do not include this helper or validate timing evidence after restoring .lake/build. This is separate from the repaired PR/rebase/queue project-artifact manifests.

   A concrete counterexample is a retained pre-policy Main cache for source version S1, followed by Main changing that file to S2 and introducing the policy, followed by a PR reverting S2 to S1. With the other Lean/configuration inputs unchanged, the PR has the old cache’s exact key. Its restored trace can replay S1, while check accepts the missing fresh timing. The exact-function fixture confirms equal old/PR build identities and exit 0 for the replayed changed module. Ordinary edits to uncached source correctly rebuild; this finding concerns reverting to a retained cached source.

   Bind every whole-build restore path, including restore prefixes, to the timing policy, or require matching per-file timing receipts / fresh measurement for reused changed files. Add the retained-pre-policy-cache plus source-reversion regression. Pinning only the project-artifact manifest does not cover the actions-cache route.

2. P2 — complete watchdog cleanup after parent exit or reparenting. The watchdog module is unchanged. watch escalates only while the build parent remains alive and the target remains in its current descendant tree. An isolated fixture executing this exact module showed a TERM-ignoring Lean-named child surviving beyond the grace interval after its parent exited, although watch returned 124. The workflow’s tee pipeline can remain open if that survivor retains its output descriptor.

   Track an isolated owned process group or identity-bound targets, and finish TERM/grace/KILL cleanup before returning, even after parent exit. Test that no owned child/output writer survives; the existing ordinary-sleep test checks only the easy TERM-success case. Also fail closed when the ps observer fails: its nonzero status is currently discarded and can be treated as an empty successful observation.

Validation: all eight current watchdog/log-checker unit tests pass. The additional source-bound probes establish the gaps above; the cache/timing scenario uses controlled inputs, not a claimed hosted failure or measured 865-second compile.

These are protected workflow/gate changes, so the separate authorization applicable to PR773 must still be established before queue admission. Other PRs’ grants and the author’s claim about another session are not adopted as a new grant here.