Reuse unchanged PR builds during ordinary CI

[Vilin97]

A PR can spend another hour compiling unchanged Lean proofs after a metadata edit or after merging main. The existing rebase shortcut correctly falls back to full checks in these cases, but ordinary CI then loses the PR’s previously compiled files.

This change restores matching compiled files from successful earlier runs of the same PR before the ordinary Lake build. It also fills gaps for newly merged projects when main’s large build cache has not caught up, without downloading projects already present in that cache. Metadata edits no longer discard unchanged compiled proofs.

Lake still runs, including its dependency checks, and every index, warning, lint, style, quality, and minimal-file gate remains. Reuse requires matching Lean sources, complete source inventories, and pinned build settings. Changed own sources or settings, unrelated histories, failed attempts, missing artifacts, and unreadable archives fall back to normal compilation. Changes to imported modules use Lake’s normal dependency tracking. Run history is searched page by page until a matching build is found or history is exhausted, retaining the latest-attempt rule across pages. Archives are extracted completely into a temporary directory before publishing files, so interrupted extraction leaves the existing build intact. Regression tests for older runs and interrupted extraction failed before these repairs and passed afterward.

Validation: 617 Python tests passed with 2 skips; Ruff checks and formatting; Actionlint across all workflows. The Lean CI lane now requires both real-Lake tests to run with the current pinned toolchain, and fails if that toolchain is unavailable: unchanged proofs retain their restored compiled file, while a proof invalidated by a changed imported definition rebuilds and fails. The local suite uses a temporary CPU-count command for Linux-specific profiling tests on macOS; the repository scripts are unchanged.

A controlled GitHub comparison passed on identical frozen Conway PR #604 sources and the same exact compiled main and dependency caches. Both sides passed normal index, warning, lint, style and quality checks, with identical validation counts: 285 lint checks cached / 2 fresh, and 854 quality checks cached / 5 fresh.

Measured phase	Before	After
Lake build	48.6 min	42.6 sec
Recover matching PR build	—	37.2 sec
Index, build/recovery, lint, style and quality	64.4 min	14.1 min
Whole GitHub job, including setup/cache transfers	71.2 min	18.7 min

This saved 50.3 minutes in the measured checks (78%) and 52.5 minutes in the whole job (74%). It measures reuse of an unchanged PR project on a warm main cache; newly changed proofs still compile normally. Validation checks remain and account for most of the remaining time. These are one before/after pair on separate GitHub runners, rather than a promise of identical times for every PR.

Baseline: https://github.com/Vilin97/lean-pool/actions/runs/37492736518 . Reviewed implementation: https://github.com/Vilin97/lean-pool/actions/runs/37495288351 . Timing JSON and diagnostic logs are retained as workflow artifacts. Measurement helpers and workflow changes are confined to a separate branch.

[greptile-apps]

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

[High risk] CI workflow and build artifact reuse logic.

No new blocking issue was found in the changes since the previous review; the PR appears safe to merge on that basis.

Summary

The PR restores matching compiled files from earlier successful runs before ordinary PR builds, while retaining Lake and the existing validation gates. Since the previous review, the branch merged main without changing the PR’s workflow or Python implementation.

_{Reviews (3) · Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." · Reviewed by Greptile}

[Vilin97]

I completed a static review of all five changed files at 15dcc57b, including the three complete modified base versions and all five deltas. I found no demonstrated introduced correctness or security defect.

In the ordinary single-job path changed here, artifact recovery remains optional. The index check before recovery and the subsequent Lake build, warning rejection, lint, text-style and repository quality checks remain mandatory. Lookup or validation failure leaves the normal build path in place. Reuse selects a successful same-PR reachable prior head; the archive must match that head, the complete packaged project source inventory and pinned Lake settings. Payload members are restricted to project build files and extracted fully into staging before overlay.

Cached builds can replay their saved diagnostics: the pinned Lake version's trace handling replays the prior build log for up-to-date module outputs. Reusing an up-to-date trace does not by itself suppress those diagnostics. The producer workflow/helper itself is not manifest-bound; this remains an artifact provenance assumption, with no demonstrated bypass in the reviewed change.

The tests include meaningful real-Lake unchanged-build and changed-import failure cases. Their mandatory workflow step is limited to the single-job lane. I did not execute the tests, build Lean, reproduce timings or verify current CI. This review does not authorize changes to, or merging of, protected CI gates.