Reuse main build caches with project-only PR artifacts

[Vilin97]

Minimal-file verification PRs currently publish a full pool build even when they change no Lean sources, and sharded assembly does not recover prior PR project outputs. This duplicates several gigabytes of unchanged outputs and can repeat project compilation after a branch update.

Keep the full pool and dependency caches owned by main. Publish only PR-owned project outputs for minimal verification, selected from the author's merge-base diff; infrastructure-only PRs publish a manifest without compiled pool files. Consumers validate the exact checkout tree and pinned configuration before overlaying those files onto the shared main build. Assembly restores matching successful PR project artifacts once, before layering fresh shard outputs, rather than duplicating downloads on every shard. Queue assembly retains its project-artifact recovery before the normal Lake build. Transient shard assembly archives keep their existing one-day retention.

Lake compilation, warning rejection, index checks, linters, quality checks and baseline-214 minimal verification still run. Missing caches or incompatible artifacts fall back to normal compilation. No cache allowance or billing setting changes.

Validation: 684 Python tests passed, 2 skipped; 96 focused artifact/cache/queue tests passed, including pinned-Lean replay and dependency invalidation tests. The new project-only archive regressions failed before the implementation. Ruff, formatting, Actionlint and diff checks passed.

Rebuilt on actual main after #610 and #611 merged, with only these five infrastructure and test files changed. The full suite also passed on the merged project-card layout. Hosted validation uses the warmed main cache and the protected merge queue; all current-head gates, including minimal verification, remain required.

[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] Changes build cache strategy and artifact handling in CI.

The PR appears safe to merge; no new actionable issue remains.

Summary

Main keeps publishing full builds. Minimal-verifier PRs publish only changed projects, or a manifest when no Lean sources changed.

• Consumers check the checkout tree and pinned inputs before installing files.
• Assembly restores prior PR outputs once, before fresh shard outputs.
• Added tests cover shared-cache preservation, invalid archives, recovery order, and pinned-Lean replay.
• Both earlier unnumbered findings are addressed: recovery now happens in assembly, and shards no longer download prior project archives.

_{Reviews (4) · Last reviewed commit: "Restore prior PR outputs once during sha..." · Reviewed by Greptile}

[Vilin97]

Source review at 07ec396dee2ac7263b5ff4aa27f3b36957148492:

I reviewed the complete five-file diff and the cache producer/consumer paths, with an independent second source review. I found no additional concrete defect in this version. Project-only artifacts preserve the shared main build, while the manifest still checks the exact checkout tree and pinned toolchain, Lake configuration and dependency inputs. Restoration stages and validates archive contents before installation; ordinary Lake compilation and the existing validation steps remain required. Project overlay publication is atomic per file, without a whole-overlay rollback guarantee.

The two earlier Greptile findings are addressed in the current source: assembly restores reused PR projects once before applying fresh shard outputs.

The initial source review inspected the three test files. Subsequent focused validation at this same head passed all three cases: both parameters of test_project_archive_preserves_shared_main_build and test_project_overlay_rejects_unowned_outputs_before_install (zero failures, errors or skips). These ran against the unchanged source files in an isolated harness with synthetic Git repositories and fake build outputs. Full repository and workflow CI remains required.

PR610 has merged. The rollout policy requires both PR610 and PR611 merged and green current-main CI before any competing merge or auto-merge. Current-head checks and integration must still be reconciled before this PR can enter the protected queue.