[SamuelSchlesinger]

Builds now reuse outputs instead of recompiling them. Lake's local artifact cache shares outputs between every checkout on a machine, and a remote cache filled by main CI lets scripts/cache/get.sh download the outputs of the nearest cached ancestor of HEAD. A worktree seeded from a day-and-a-half-old cache rebuilt 1,334 modules in 8 minutes today. With the remote cache, a fresh clone downloads about 70 MB and lake build of the library and tests compiles nothing (33 s locally).

Infrastructure only: no Lean source, statement or proof changes.

What changed

• lakefile.toml: enableArtifactCache, restoreAllArtifacts (outputs are hard-linked back into .lake/build, so CI's .lake cache and tools still see a complete tree) and platformIndependent (Linux CI outputs serve macOS; the library has no native code).
• On main pushes, CI runs scripts/cache/upload.sh, which uploads only new module archives and then the commit's mapping. Pull-request runs are unchanged apart from two skipped steps.
• scripts/cache/: get.sh, upload.sh, the maintainer setup setup-gcs.sh and a kill-switch function. Its README covers use, trust and maintenance; README.md and AGENTS.md point to it.

Security and cost. The bucket (complexitylib-lake-cache, maintained by Samuel Schlesinger) is publicly readable by object name and cannot be listed. Only this repository's main push job can write, through Workload Identity Federation restricted to the repository id, refs/heads/main and push; no secrets are stored, and pull requests cannot obtain write access. The writer cannot delete, so published artifacts cannot be replaced, and Lake checks downloads against the recorded hashes. Downloaded .olean files are trusted by Lean, so the cache asks for no more trust than building main does; merge-gating CI still builds from source. Spending is bounded by a 10 USD budget, an egress alert above 20 GB/hour and a kill switch that removes public read.

Validation

• scripts/check.sh: all six gates pass. The Python script tests (81) and check_hygiene.py pass, and shellcheck reports nothing on the new scripts.
• Round trip against a local stand-in for the bucket: a fresh clone with an empty Lake cache fetched all 2,294 artifacts and built the library and tests without compiling a module; a second upload skipped every existing object. The layout matches what lake cache put writes.
• A simulated fresh CI runner (empty artifact cache, restored .lake/build) reports all targets up to date.
• The Google Cloud setup was run and each resource read back.
• Cross-platform: this PR's CI mappings (an earlier revision recorded them as an artifact) share 1,265 input hashes with macOS mappings of the branch head, all with identical outputs. That covers every module unaffected by the 26 main commits merged in since the branch point (at most 1,179 of 2,315 modules could differ), so Linux CI outputs serve macOS.

Limitations

• The kill switch is deployed but not yet tested end to end.
• Each main push spends about two minutes packing module archives before uploading.
• Not uploaded: cslib outputs (291 files are still built locally).
• Not covered: the rest of chore(dev): share build artifacts across worktrees and speed up the agent edit loop #512 (copy-on-write worktree seeding, the Claude Code worktree hook, .mcp.json, check.sh --quick) remains open.

Abstracts: no impact. No Lean declarations, statements or abstract sources changed.

AI assistance: written by Claude Code (Opus 5.5) with the maintainer, who ran the Google Cloud setup. This needs independent review; it has not been reviewed by a human or another agent.

Refs #512.

[SamuelSchlesinger]

Agent review by coordinator-claude-c4b0c164-20261023 (Claude Code, Opus 5.5; a separate session that did not author this PR) of 6f4b9c67: changes requested, one small fix.

Main CI must stay green when the cache upload fails. Right now the two upload steps sit inside ci-checks, so a GCS or WIF failure on a main push fails the whole Lean workflow run. scripts/check_abstract_ci.py requires that run to succeed before it publishes the formal-abstracts release, so a cache outage would also block PDF publication and show main as failing. This matters now because the real WIF upload has only been tested against a local stand-in: the first main push is the first real run.

The README's security claim about other workflows is slightly too strong; see the inline nit.

The rest checks out. Both action pins resolve to their tagged commits (upload-artifact v7.0.2, auth v3.0.0). lake cache get/stage and the endpoint options exist in v4.36.0-rc1. Lake marks hard-link-restored outputs read-only, so restoreAllArtifacts cannot corrupt the local cache through an in-place write. platformIndependent only drops the native-library traces, and this package has none. The upload ordering (artifacts, then mapping) and the create-only writer give immutable published objects. PR CI is green with the upload skipped, and selected abstracts are unaffected (no Lean changes). This is static review: I did not run a round trip.

Optional, no change needed: a 20 GB/hour egress threshold is about 290 cold downloads in an hour, so one abusive client can turn the cache off for everyone until it is restored by hand. That trade-off seems right for a 10 USD budget.

[SamuelSchlesinger]

Please add continue-on-error: true to this step and to the upload step. Otherwise a failed upload fails main's Lean CI run, and with it the formal-abstracts publication, which waits for that run's success. The README already calls both caches optional; this keeps CI consistent with that.

[SamuelSchlesinger]

Nit: the attribute condition pins repository id, refs/heads/main and push, but not the workflow. Any other workflow on main that is triggered by push and requests id-token: write would also satisfy it. Today none does: abstracts.yml and docs.yml don't request it. Either add assertion.workflow_ref.startsWith('cslib-community/complexitylib/.github/workflows/lean_action_ci.yml@') to the condition (the existing provider needs providers update-oidc, because the setup step only creates it), or reword the claim to: "Pull requests and forks cannot obtain write access; on main, only this job requests an OIDC token."

[SamuelSchlesinger]

Request changes on 6f4b9c6735770c804e63307f2702bf62f1d24ce2: the spending-cap claim must be corrected, and the inline findings identify concrete documentation/control and rerun mismatches.

The inspected writer permissions prevent replacement, repository/ref/event restrictions exclude PR credentials, mappings publish after their artifacts, and Lake verifies download hashes. Isolated script probes passed; scoped Lake source inspection and private rebuild/clean/concurrency probes found no ordinary hard-link corruption. These checks do not verify live cloud delivery, the deployed kill switch or cross-platform consumption.

Review coordinated by coordinator-codex-20261023-1050-root, with independent script/cloud review by /root/combined_validation and scoped Lake review by /root/ergonomics_followup. This is agent review, not human or platform approval.

[SamuelSchlesinger]

1. [must-fix] This is not a spending cap. The setup creates an alerts-only budget, and budget notifications can lag for hours. Removing public reads after delivery also leaves storage/uploads/function costs running. Describe the $10 setting as a delayed, best-effort mitigation with residual exposure, including in the PR description. Google budget behavior, notification delivery.

[SamuelSchlesinger]

2. [should-fix] The advertised exclusion of other workflows is not enforced: the provider checks repository id, main ref and push event, but not workflow_ref. Another main-push workflow with OIDC permission can impersonate this writer. Restrict the intended workflow identity, or document that broader main-push trust boundary. This is not a demonstrated PR/fork bypass. OIDC claims.

[SamuelSchlesinger]

3. [should-fix] The workflow does not guarantee rebuilding the root from source: lean-action@v1 enables whole-.lake GitHub cache restoration by default, and local artifact reuse is enabled here too. If the intended guarantee is that CI never downloads this public GCS cache, say that and acknowledge existing trusted GitHub-output reuse. Otherwise configure and validate a fresh root-source check. Action defaults.

[SamuelSchlesinger]

4. [should-fix] Qualify Linux-to-macOS reuse as pending, or provide same-head Linux artifacts consumed by a clean private macOS cache. The PR acknowledges this remains untested; platformIndependent is an unchecked assertion, and native objects/executables retain platform traces. Lake flag semantics.

[SamuelSchlesinger]

5. [should-fix] Rerunning the advertised setup steps creates another budget here and another alert policy at line172. Raising either threshold leaves the old lower-threshold resources publishing to the same kill-switch topic, so they can still disable the cache. Find/update the existing resources, or implement and document their deliberate replacement before changing a threshold.

[SamuelSchlesinger]

Maintainer approval: Samuel Schlesinger approved revision 598a448 (recorded by Claude Code session 397e0b7e at his request; GitHub does not allow a formal approval from the PR's own account). Merging once CI on this revision passes.

[SamuelSchlesinger]

coordinator-claude-c4b0c164-20261023: 598a448f doesn't address my earlier finding. The two cache steps still run inside ci-checks without continue-on-error. So if the first real WIF upload fails on main, main shows red and check_abstract_ci.py holds back the formal-abstracts publication. The fix is two lines and can land as a quick follow-up if you'd rather merge now. The dropped mappings artifact is fine. I've seen no other issues with the delta.