[Vilin97]

Stacked on #820 (its three commits show here until it merges). This is the next CI speedup; it changes how the build-time gate decides what to recompile, and updates .github/CODE_QUALITY.md to match. The 600 s limit itself is unchanged.

Why

Two branches account for most recent PR CI time: codex/daily-superharmonic-20261111 (33 runs, median 65 min) and codex/daily-goldberg-seymour-20261105 (13 runs, median 57 min).

• Every push recompiles the whole project. build_time_limits prepare deleted the output of every file the PR changed relative to main, so each run timed it afresh. The last 12 pushes to the superharmonic PR edited 1–67 of its 1,304 files; each run recompiled all 1,304 (about 38 min). The merge queue and the push to main repeat that.
• A stale base makes merged projects look changed. The plan and the gate diffed against github.event.pull_request.base.sha. In run 43622384721 that was 313783a11 (Nov 12) while the tested merge commit's first parent was 5dd712603 (Nov 14). The 10 commits in between made 10 other projects count as this PR's change: the run went sharded and rebuilt them.

What

1. Timing receipts (build_time_limits.py). check writes <Module>.timing.json beside each changed module's output: the measured seconds, bound to a SHA-256 of its .olean, .olean.private and .olean.server. prepare invalidates only changed modules whose output has no matching receipt. check uses this job's measurement when the module was compiled here, otherwise the recorded time of the exact output being reused, and applies the limit either way. A changed module with neither still fails.
2. Partial reuse of the PR's earlier build (ci_pr_build.py, rebase_fastpath.py). Reuse used to require the project's sources to be identical to the earlier run. It now restores the outputs of modules whose own source is unchanged; Lake's traces decide which of those are still valid after their imports changed. Shard jobs restore them too. Queue and rebase reuse keep the exact-source requirement.
3. Fresh base (lean_action_ci.yml). For a PR, changes are measured from the tested merge commit's first parent (verified by HEAD^2 == pull_request.head.sha, else the event base as before). The plan and all four BUILD_TIME_BASE uses share one diff_base output.

Receipts sit next to the outputs, so they travel with every cache and artifact that carries those outputs: PR archives, queue archives, shard uploads and main's cache.

What stays guaranteed

• Output that was compiled without being timed as a changed file has no receipt, so it is still rebuilt. That covers the revert-to-a-cached-source case the existing tests pin down.
• A receipt certifies only the bytes it was measured for. Any rebuild that changes an olean invalidates it.
• A recorded time over the limit fails, so reuse cannot launder a slow file.
• Receipts are only written by check in CI, and only artifacts of successful runs are reused, as before. build_time_limits.py is a pinned input of PR archives, so archives from before this change are not reused.

Verification (Azure VM, Lean v4.35.0)

• New pinned-Lean tests, which also run in CI's dependency-tracking step:
  • test_lake_recompiles_only_the_edited_module_of_an_earlier_pr_build: after an edit to one of two PR modules, Lake builds only that one, and the gate passes with the other's recorded time.
  • test_lake_output_restored_without_a_recorded_time_is_recompiled.
• Unit tests for receipts (binding to each olean file, malformed receipts, over-limit recorded time, fresh time replacing a recorded one) and for partial restore (edited, added and deleted modules; changed build settings still skip the download).
• Full Python suite on the VM: 944 passed. The failures are 4 process-watchdog tests and test_repository_notice_is_current, which fail the same way without this change in that environment.

Not yet measured on a real PR: the first run after merge has no receipts or compatible archives, so the saving shows from the second push to a PR onward.

🤖 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 defects were found.

Summary

This PR reduces repeat compilation while keeping the build-time limits.

• Changed modules reuse times tied to their compiled outputs.
• PR builds reuse earlier outputs for modules whose source is unchanged.
• PR builds measure changes from the tested main revision.
• CI trims Lake setup files before saving or uploading builds.

Review was based on source and test inspection. No tests were run during this review.

_{Reviews (1) · Last reviewed commit: "Recompile only what a PR push changed, a..." · Reviewed by Greptile}

[Vilin97]

Changes needed at 53136ced9414a8de0c0b26cd6ec007d78d29b861 — two small timing-gate repairs.

• Cover assembly fallback compilation (P2). Shard recovery happens before the build stamp, and shard packaging uploads only files newer than that stamp. An unchanged output replayed from an earlier PR run therefore need not reach assembly through the shard archive. Assembly's independent recovery is optional and may fail. Its full build can then compile that module, but both timing passes exclude every shard project, so even an assembly log containing an 865-second changed file passes the 600-second check. With the new receipts, remove those assembly exclusions: valid delivered receipts avoid recompilation, while missing outputs rebuild and their fresh timings are checked. See shard delivery and assembly.
• Reject a receipt when its output is missing (P2). recorded_seconds accepts outputs: null when output_digest also returns None. Against the published functions, that receipt returns 1.0, prevents invalidation and lets an empty build log pass. Require a non-null current digest before comparing it with the receipt, and add a missing-output/null-receipt regression.

I read all 11 complete patches and the current receipt, partial-restore and queue-provider paths. The partial restore preserves the exact-input checks for queue/rebase callers and leaves changed-import validity to Lake; no additional source defect was found there. I independently replayed the two cases above using the captured public functions in memory. The proposed digest guard makes the missing-output check fail; including the shard project makes the 865-second check fail.

These results establish the reader and timing-coverage defects. They do not demonstrate a compilation, lint or kernel bypass, or validate the author's VM/test/performance claims. Fresh protected checks are required after repair.

[Vilin97]

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

Reviewed head: 53136ced9414a8de0c0b26cd6ec007d78d29b861

Verdict: ✅ approve

This refactors CI reuse through output-bound timing receipts, per-module restoration, current-main diff selection, and smaller Lake setup files. Cache validation remains explicit, and Lake still checks dependencies. All 168 targeted tests passed, including seven using pinned Lean 4.35.0; a synthetic merge also verified base selection. Full-pool performance was not measured.

Aspect	Value
Scope	CI cache and timing refactor
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	➖ unchanged
Risk	✅ low

The refactor reduces repeated CI work while preserving dependency checks and timing enforcement, with no actionable maintenance regression found.

---

Tokens: 1,635,878 in / 8,577 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $6.6722 (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.