[Vilin97]

Stacked on #820 and #821 (their commits show here until they merge). This is the "use the spare runners" part of the CI speedup work.

Why

Lint and the quality audits reuse per-project pass receipts, so an ordinary PR validates only what it touches. But a change to any checker input (the workflow, validation_cache.py, quality.py, the no-lint lists, the pins) invalidates every receipt. One job then validates the whole pool, one project at a time. In run 42594711151 "Assemble and lint" spent 36.4 min in Lint and 67.8 min in Repository quality checks. The merge queue and the push to main repeat it.

In-job concurrency does not fix the lint half: #785 measured that one lint process already saturates a 4-vCPU runner (35 min with 4 concurrent units against 34 serially). The org has 60 concurrent runners and typically uses about 5.

What

• Shards validate what they build. After uploading its build outputs, each shard job runs python -m lean_pool.shard_validation --units <its projects>: the per-project lint, declaration, axiom and option-backdoor checks, through the same functions the whole-pool run uses. It uploads only its pass receipts (ci-validation-NN).
• finalize still decides. It merges the shards' passes (validation_cache merge) and then runs the unchanged Lint and Repository quality steps. Those recompute every fingerprint, reuse matching passes, and run anything without one, plus the repository-wide checks and the root unit. The shard validation and upload steps are continue-on-error, so a shard can neither fail nor pass the run by itself; a real failure is re-run and reported in finalize. A shard keeps the passes it earned even when one of its projects fails.
• The planner fans out when checker inputs change, even with a warm build cache. Shards replay the build and spend their time validating. It reads the input list from validation_cache.py itself, with a test that it equals GLOBAL_INPUTS.
• MAX_SHARDS goes from 10 to 14. Past that the costliest project (MovingSofa) fills a shard alone, so more shards stop lowering the maximum.

quality.py is not modified. No check changes what it accepts: a receipt only counts where finalize computes the same fingerprint for the same modules.

Relation to #785

#785 runs quality audits 4-wide inside one job (62 → 36 min) and is still open. The two are complementary, and both edit ValidationCache.check; whichever merges second needs the small units filter moved into the other's loop.

Verification (Azure VM, Lean v4.35.0)

• Ran python -m lean_pool.shard_validation --units Champernowne on a real build: 4 fresh checks (lint, declarations, axioms, backdoors) in 28 s, every other unit skipped. After merge, a whole-pool cache re-validated none of that unit's lint, axiom or backdoor checks.
• New tests cover the unit filter, shard runs keeping passes when one unit fails, merge by fingerprint (an edited project is checked again), corrupt fragments, the planner trigger, and the workflow contract (step order, continue-on-error, no cache saves in shards).
• Full Python suite on the VM: 953 passed. The 5 failures (4 process-watchdog tests and test_repository_notice_is_current) fail the same way without this change in that environment.

This PR's own CI is the first real fan-out: it edits the workflow, so every receipt is invalid. Its shard and finalize timings are the measurement to compare against the 104 minutes above.

🤖 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 latest change appears safe to merge; both earlier import findings are fixed.

Summary

The PR spreads project lint and quality checks across build shards. finalize checks each receipt against current inputs and runs checks without matching passes.

• Checker changes send project validation across parallel build shards.
• Later PR builds reuse unchanged modules with recorded build times.
• CI trims Lake setup files while keeping local import names.

_{Reviews (3) · Last reviewed commit: "Move a test import to the top of the fil..." · Reviewed by Greptile}

[Vilin97]

Changes needed at 64b3fad333f4171ea0b4a6dc994bfb46eafaa34c — the new shard-validation logic is supported, but the stacked timing repairs remain necessary.

I reviewed all eight complete incremental patches from PR821's 53136ce, their current cache/shard/planner/workflow implementations and the unchanged quality-check provider. I also reconciled the author's one-file import cleanup from c2bd07d to this head. Both existing import discussions are now resolved; I made no branch change.

The shard design preserves the final decision: unselected units issue no pass, only successful checks enter the used receipts, merging a fragment does not certify it, and unrestricted assembly recomputes fingerprints and runs missing checks. Global/root checks remain with assembly. In-memory execution of the published code confirmed exact-pass reuse, changed-input rechecking, rejection of malformed/failed receipts and the planner's agreement with all 16 current fingerprint inputs. This is source and contract evidence; it does not claim a hosted CI or Lean build.

The stack still contains both Source275 findings: the null-output receipt reader is unchanged, and assembly still excludes shard projects from both timing passes. Apply the non-null digest guard and remove the assembly exclusions, with the missing-output and fallback-over-limit regressions, before integration. The new parallel validation code does not repair those inherited timing gaps.

Fresh checks on the repaired head and the separately required direct gate/workflow authorization remain necessary. No older head's CI or advisory verdict is transferred here.