Speed up CI and preserve completed checks through PR updates and merges

[Vilin97]

CI spends substantial time checking unchanged projects, and repeated automatic branch updates can cancel that work before its results are saved. One recent removal PR lost its saved results and repeated all 283 lint checks and 847 quality checks. Another reused most checks but still spent 10.9 minutes on linting and 26.6 minutes on quality checks. PR exposition verification was also waiting for a complete build archive that PR runs never publish.

This PR combines the performance improvements and repairs in one place. The maintainer explicitly requested packaging all CI speedups in one PR, then authorized further CI and merge-throughput repairs and shipping once ready. These workflow and checker implementation edits are within that request. Every existing build, warning, style, and quality requirement remains in place.

1. Spend less time deciding what needs checking. Read each compiler-generated list of imported files once per validation process, reuse source comparisons between checks, and track the Lean linter separately from the Python quality checker. Successful results are reused only when the project files, imported files, metadata, dependencies, and relevant checker settings match. Changing one checker does not repeat the other checker's work.
2. Scan Lean files faster. Find comments and strings in larger steps rather than examining every character in Python. Run detailed forbidden-code checks only on lines that could contain a violation. Preserve nested comments, escaped strings, line numbers, rules, and diagnostics.
3. Keep small successful-check results available when large caches disappear. Publish the approximately 150 KB of saved results as a separate GitHub artifact. Recover them from successful main runs when the cache has been evicted. Carry results through an already verified automatic rebase and from a successfully checked, just-merged PR to main. Downloading results does not make a check pass: the normal validator still compares them with the current inputs.
4. Reuse compiled work after a merge. On main, try the existing verified project artifact from the merged PR before building. Verify its project sources and pinned dependencies, then run the normal Lake build. Missing or incompatible artifacts use the normal build.
5. Stop unnecessary waits and duplicate downloads. PR consumers immediately use the normal Lake build instead of waiting for a full archive that PR CI does not publish. Documentation skips an archive download when the exact compiled build is already cached. Exposition verification uses the same build-cache name as Lean CI.
6. Package documentation builds faster. Use faster compression, unpack once into a temporary directory, verify the source/configuration match and archive integrity, then move the finished directory into place. Existing compressed downloads remain readable; invalid downloads fall back to the normal Lean build.
7. Upload large caches only when their actual build inputs change. Identify compiled builds from Lean sources and the index generator, together with the existing Lean/Mathlib/build settings. README, project-card, license, profiling, extraction, and validation-script edits do not cause another upload of an identical compiled build. Lake still checks its normal build records.
8. Retain one current main copy per cache kind safely. Remove older copies only after GitHub lists the replacement as available. A failed upload preserves the old copy, and an older overlapping job cannot delete a newer copy. Keep dependency, compiled-build, validation, documentation, and extraction caches separate; leave PR caches alone. Only save compiled builds after compilation succeeds. GitHub's own storage eviction can still remove caches, which is why check results also have the independent artifact copy.
9. Let CI finish before updating a PR. Automatic updates from main defer drafts and branches with unfinished checks. Retry after CI completes, with a periodic fallback for other check providers. Recheck the branch revision and check state immediately before pushing, and keep infrastructure PRs stable while unrelated content merges. Existing conflict handling and non-forced pushes remain.
10. Avoid wasting advisory profiling on unfinished drafts. Automatic profiling starts when a PR is ready. Explicit /profile and manual requests remain available for drafts.
11. Let an active main CI run finish. A newer main commit no longer cancels its build and checks. Superseded PR runs still cancel. GitHub retains one active and the latest pending run for this group.

The source review's stale-result defect is repaired: retain local imported files discovered before a later compiler-inventory error triggers the conservative fallback. Tests reproduce the problem for all four check kinds across separate cache instances; all four failed before the repair and pass afterward. The reviewed early cache deletion and overly broad script inputs are also repaired.

The controlled pre-merge comparison passed on GitHub runners. Both cases used identical project sources and the exact same restored compiled-project cache. Neither restored a dependency cache. Each ran all 283 lint and 847 quality checks freshly, then repeated using only its own verified successful results, with zero fresh checks in the repeat.

Work measured on GitHub	Before	After
Build, lint, style, and quality with every check fresh	110.4 min	71.5 min
Repeated build, lint, style, and quality with saved successful checks	23.9 min	3.4 min
Documentation build packaging	4.74 min	2.35 min
Documentation build unpacking	10.42 min	3.93 min
Documentation build upload	47 s	43 s
Compressed documentation build	5.763 GB	5.189 GB

This is 35% less time for fresh validation and 86% less for unchanged-project validation. It measures build and validation with an existing compiled build, not cold compilation. Totals exclude runner waiting, setup/downloads, documentation transfer, and production cache saving. This is one paired run, so machine variation remains possible. Both cases performed the same checks; the experiment did not save or prune production caches. Fresh-check peak memory remained about 12 GiB. The comparison used an earlier revision: the later cache transport and branch-update repairs are tested but are not included in those measured savings.

Local comparisons also found source comparisons for 20 project units fell from 36.5 to 4.06 seconds with all 40 comparison results identical, and full static quality checks fell from 181.7 to 34.7 seconds with zero errors. The comment/string scanner agrees with the original on all 15,394 project files and 10,000 generated edge cases. The forbidden-code scan agrees across all 15,395 pool files.

Validation: the full local Python suite passed 596 tests with 2 skips, plus Ruff checks/formatting and Actionlint across all workflows. After the final cache-input refinement, all 15 cache tests pass, including two additional metadata/license cases. Tests cover changed imported sources, additions/deletions, malformed or oversized artifacts, preservation on download/upload failure, successful-run selection, branch/check races, active-CI deferral, infrastructure exclusion, both compression formats, and damaged archives. Existing Linux-oriented profiling tests on macOS use a temporary nproc adapter to sysctl.

Current-head GitHub CI must pass before merging. This PR changes no Lean proofs, branch protection, required check names, or review requirements. Parallel project validation and prebuilt Lean checker programs remain deferred. Cold compilation of a large new project can still take substantial time.

[Vilin97]

Source review update for 99f43f807ded7d70c6ed764841979e994c55be34 against 793672ba73955be0db012f451714a796e5be9a7a

Changes requested: the P2 below remains. The two-file update separates Lean-linter and Python-quality cache inputs and memoizes comparisons by their dependency set. It leaves _module_sources and the inventory-fallback path unchanged. The new tests cover checker-specific invalidation, ordinary source changes, and comparison reuse; the combined missing-pool-import/external-local-dependency regression remains absent.

Preserve dependencies discovered before an inventory error and add that combined test across fresh cache instances. A concrete repair can pass the caller discovery set into _module_sources, add each resolved import before the next import can fail, and retain separate sets for successfully memoized module inventories. The saved repair proposal has not been applied to this PR.

The other eight current file blobs match the reviewed ten-file expansion at 976707c. Source review found no additional concrete correctness defect in the checker-input partition or those archive/cache additions: unknown check kinds retain all inputs; source/configuration and archive member checks plus decompressor completion precede installation; normal Lake builds remain. Cache deletion retains PR entries and other cache families. The workflows expand job permissions to actions: write; protected infrastructure policy still applies.

The author-reported tests, Actionlint results, scanner comparisons, component timings and running measurement experiment were not independently reproduced or observed. Current CI and end-to-end performance are not established by this source-only review. The PR remains a draft.

---

Original review at 93592c2ce94a52ee47d5f10328c180f0854729ce, retained in full:

Changes requested — read-only source review

Reviewed 93592c2ce94a52ee47d5f10328c180f0854729ce against 793672ba73955be0db012f451714a796e5be9a7a, including the complete four-file diff and affected implementation/callers. Two independent source reviews corroborated the finding below.

P2: Preserve discovered local dependencies when inventory parsing falls back. At validation_cache.py:82, _module_sources accumulates paths privately. If importArts lists an existing local Aux.Support before missing LeanPool.Missing, it records Aux/Support.lean and then raises. The caller loses that entire set; its fallback includes only LeanPool/**/*.lean and the pool root. The previous implementation retained the already discovered local dependency in the outer set. A pass receipt created on this fallback path can consequently remain a cache hit after Aux/Support.lean changes, even with a fresh ValidationCache instance. This affects cached declaration and environment audits, not just performance.

Preserve those discovered dependencies on failure and add the combined missing-pool-import/local-dependency invalidation case. The separate new tests for outside-pool imports and missing imports do not cover their interaction.

The scanner changes and valid-inventory memoization otherwise appear consistent with the existing rules and immutable-checkout assumption. The reported test/corpus comparisons and component timings were not reproduced in this source-only review. Current CI and end-to-end performance are not established here.

[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] Modifies CI workflows and build caching infrastructure.

The PR should not merge until the existing contribution-instruction objection to the unrequested quality-gate and workflow changes is resolved.

Findings

1.  Old cache deleted before replacement ▶
2.  Unrelated scripts change build identity ▶
3.  Unrequested gate changes ▶

Summary

The PR speeds validation and documentation builds through reused source comparisons, content-addressed compiled-build caches, faster artifact packaging, and post-upload cache pruning. It also adds recovery of saved validation results and adjusts rebase scheduling.

• The earlier findings about deleting caches before replacement and hashing unrelated scripts are fixed.
• The existing contribution-instruction finding about unrequested changes to quality gates and workflows remains outstanding.

_{Reviews (3) · Last reviewed commit: "Preserve completed CI work through cache..."}