chore(build): share build outputs through local and remote Lake caches

.github/workflows/lean_action_ci.yml

@@ -11,6 +11,11 @@ on:
 jobs:
   ci-checks:
     runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      # Only the remote-cache upload on `main` pushes uses this; the Google Cloud identity pool
+      # also refuses tokens for any other repository, ref or event (scripts/cache/README.md).
+      id-token: write
     steps:
       - uses: actions/checkout@v4
       - name: Test documentation checker
@@ -31,3 +36,16 @@ jobs:
         run: |
           set -e
           lake exe checkInitImports
+      # Publish the build outputs to the remote cache read by scripts/cache/get.sh. Skipped until
+      # the maintainer sets the repository variables described in scripts/cache/README.md.
+      - name: "Authenticate to the remote cache"
+        if: github.event_name == 'push' && github.ref == 'refs/heads/main' && vars.LAKE_CACHE_BUCKET != ''
+        uses: google-github-actions/auth@7c6bc770dae815cd3e89ee6cdf493a5fab2cc093 # v3
+        with:
+          workload_identity_provider: ${{ vars.LAKE_CACHE_WIF_PROVIDER }}
+          service_account: ${{ vars.LAKE_CACHE_SERVICE_ACCOUNT }}
+      - name: "Upload to the remote cache"
+        if: github.event_name == 'push' && github.ref == 'refs/heads/main' && vars.LAKE_CACHE_BUCKET != ''
+        run: |
+          set -e
+          scripts/cache/upload.sh "${{ vars.LAKE_CACHE_BUCKET }}"

AGENTS.md

@@ -186,6 +186,12 @@ campaign or separate design study for every small improvement.
 Use MCP goal inspection, diagnostics and theorem search while iterating; reserve `lake` commands
 for validation checkpoints. If MCP tools are unavailable, say so and use the smallest shell check.
 
+In a fresh checkout or worktree, run `scripts/cache/get.sh` before the first build. Lake's local
+artifact cache then shares outputs between all checkouts on the machine, so a module is compiled
+once per machine for given inputs. Proof-only edits do not rebuild dependents; statement and
+definition changes in widely imported modules do. [scripts/cache/README.md](scripts/cache/README.md)
+describes both caches.
+
 ## Validation sequence
 
 ```bash

README.md

@@ -57,10 +57,14 @@ namespaces begin with `Cslib`, and Turing-machine declarations use `Turing`. Use
 From a checkout:
 
 ```bash
-lake exe cache get
+scripts/cache/get.sh   # prebuilt Mathlib and Complexitylib outputs
 lake build --wfail --iofail
 ```
 
+`scripts/cache/get.sh` downloads the outputs CI built for `main`, so `lake build` compiles only
+local changes; without it the first build compiles the whole library. See
+[scripts/cache/README.md](scripts/cache/README.md) for how the caches work and what they trust.
+
 Import the specific modules you need. `import Complexity` imports the whole library.
 
 To build searchable API documentation from the module docstrings (Python 3.11+):

lakefile.toml

@@ -3,6 +3,15 @@ version = "0.2.0"
 defaultTargets = ["Complexity"]
 testDriver = "ComplexityTests"
 lintDriver = "batteries/runLinter"
+# Share build outputs between local checkouts (worktrees, agent sandboxes) through Lake's
+# content-addressed artifact cache, so a module built in one checkout is reused by every other
+# checkout with the same inputs. Restoring hard-links cached outputs back into `.lake/build`, so
+# tools and CI caches that read the build directory still see a complete tree.
+enableArtifactCache = true
+restoreAllArtifacts = true
+# The library has no native code, so its build outputs are the same on every platform and the
+# remote cache (see `scripts/cache/README.md`) built on Linux CI also serves macOS checkouts.
+platformIndependent = true
 
 # Linter settings are copied verbatim from cslib's lakefile so that every module here
 # compiles unchanged when it is upstreamed.

scripts/cache/README.md

@@ -0,0 +1,81 @@
+# Build caches
+
+Complexitylib's build has two caches. Both are optional: `lake build` without them compiles
+everything it needs.
+
+**Local artifact cache.** `lakefile.toml` enables Lake's content-addressed artifact cache, so a
+module built in one checkout (a worktree, an agent sandbox, a second clone) is reused by every
+other checkout on the same machine with the same inputs. Outputs are hard-linked back into
+`.lake/build`. `lake cache clean` empties it; it lives in the Lean toolchain's directory under
+`~/.elan` unless `LAKE_CACHE_DIR` says otherwise.
+
+**Remote cache.** CI uploads the build outputs of every commit on `main`; `scripts/cache/get.sh`
+downloads them for the nearest cached ancestor of your `HEAD`:
+
+```bash
+scripts/cache/get.sh   # Mathlib's cache, then Complexitylib's outputs
+lake build             # compiles only what you changed
+```
+
+A complete set of library and test outputs is about 70 MB compressed. Outputs are platform
+independent (`platformIndependent = true`), so Linux CI builds serve macOS checkouts.
+`COMPLEXITYLIB_CACHE_URL` overrides the location; set it to an empty string to skip the
+Complexitylib download.
+
+## Trust and privacy
+
+Downloaded `.olean` files are trusted by Lean: imported modules are not re-checked by the
+kernel, and their compiled code (tactics, macros, initializers) runs during your build. Whoever
+can write to the cache could therefore make a false theorem appear proved or run code on your
+machine. The cache is set up so that this is no more trust than building `main` already
+requires:
+
+- Only the `main` push job of this repository can write. It authenticates with GitHub's OIDC
+  token through Workload Identity Federation, restricted to this repository's numeric id, the
+  `main` ref and the `push` event; no credentials are stored in GitHub. Pull requests, forks and
+  other workflows cannot obtain write access.
+- The writer can create objects but not delete them, so a published artifact can never be
+  replaced. Lake checks every downloaded artifact against the hash recorded in the mapping.
+- Merge-gating CI always builds from source; the cache only saves local build time.
+
+The cache contains only build outputs of commits on `main` (sources that are public in this
+repository); build logs and machine paths are not uploaded. Downloads are anonymous HTTPS
+requests to Google Cloud Storage; the bucket keeps no access logs.
+
+## Maintainer runbook
+
+The cache runs in a dedicated Google Cloud project maintained by Samuel Schlesinger.
+
+**Setup.** `PROJECT=<id> BILLING_ACCOUNT=<id> ALERT_EMAIL=<address> scripts/cache/setup-gcs.sh`
+creates, in order (each step can be rerun alone, e.g. `setup-gcs.sh alert`):
+
+| Step | Creates |
+| --- | --- |
+| `project` | the project, billing link and APIs |
+| `bucket` | `gs://complexitylib-lake-cache` (`us-east1`), public read by object name without listing, no soft delete or versioning, revision mappings expire after 180 days |
+| `writer` | the GitHub identity pool and provider, and the `lake-cache-writer` service account (create + read on the bucket only) |
+| `budget` | a monthly budget (default 10 USD) with alerts at 50/90/100 % and a Pub/Sub topic |
+| `killswitch` | a Cloud Run function that removes public read when the budget is reached or the egress alert fires |
+| `alert` | an alert on more than 20 GB sent per hour, to the kill switch and `ALERT_EMAIL` |
+| `variables` | prints the `gh variable set` commands for the three repository variables |
+
+CI skips the upload until the repository variable `LAKE_CACHE_BUCKET` is set.
+
+**Costs.** Storage and egress are small at this size: each `main` push uploads only modules whose
+outputs changed, and Cloud Storage's free tier covers 5 GB of storage and 100 GB of egress per
+month in `us-east1`. The budget alerts and the kill switch bound abuse of the public bucket.
+
+**After the kill switch fires.** Downloads fail and builds fall back to compiling. Check the egress
+graph and the function's log, then restore public read:
+
+```bash
+gcloud storage buckets add-iam-policy-binding gs://complexitylib-lake-cache \
+  --member=allUsers --role=roles/storage.legacyObjectReader
+```
+
+**Pruning.** Artifacts are shared between revisions, so they are not expired by age. When storage
+grows, delete the artifacts that no revision mapping still in the bucket refers to.
+
+**Layout.** `a0/cslib-community/complexitylib/<hash>.art` holds module archives and
+`r0/cslib-community/complexitylib/tc/<toolchain>/<commit>.jsonl` the input-to-output mappings of
+each commit, as written by `scripts/cache/upload.sh` and read by `lake cache get`.

scripts/cache/get.sh

@@ -0,0 +1,22 @@
+#!/usr/bin/env bash
+# Download prebuilt build outputs, so that `lake build` only compiles what you changed.
+#
+# Usage: scripts/cache/get.sh            (from the repository root or any worktree)
+#
+# Fetches Mathlib's cache, then Complexitylib's outputs for the nearest ancestor of HEAD that
+# `main` CI has uploaded (Lake looks back up to 100 commits). Missing outputs are not an error:
+# `lake build` compiles whatever the cache did not provide. See scripts/cache/README.md.
+set -u
+cd "$(dirname "$0")/../.." || exit 1
+
+url="${COMPLEXITYLIB_CACHE_URL-https://storage.googleapis.com/complexitylib-lake-cache}"
+
+lake exe cache get || echo "warning: Mathlib cache download failed; lake build will compile Mathlib" >&2
+if [ -z "$url" ]; then
+  echo "COMPLEXITYLIB_CACHE_URL is empty; skipping the Complexitylib cache." >&2
+  exit 0
+fi
+if ! LAKE_CACHE_ARTIFACT_ENDPOINT="$url/a0" LAKE_CACHE_REVISION_ENDPOINT="$url/r0" \
+    lake cache get --repo=cslib-community/complexitylib; then
+  echo "note: no cached Complexitylib outputs found for this history; lake build will compile them" >&2
+fi

scripts/cache/kill-switch/main.py

@@ -0,0 +1,45 @@
+"""Stop public downloads from the remote cache when spending or egress crosses its limit.
+
+Deployed as a Pub/Sub-triggered Cloud Run function by scripts/cache/setup-gcs.sh. It receives
+two kinds of message on the same topic:
+
+* Cloud Billing budget notifications (`costAmount`, `budgetAmount`): acts once the cost reaches
+  the budget;
+* Cloud Monitoring alert notifications (`incident.state`): acts when the egress alert opens.
+
+Acting means removing `allUsers` from the bucket's IAM policy. Objects are kept, so the
+maintainer restores service by re-granting public read (see scripts/cache/README.md).
+"""
+
+import base64
+import json
+import os
+
+import functions_framework
+from google.cloud import storage
+
+BUCKET = os.environ["BUCKET"]
+
+
+def should_stop(message: dict) -> bool:
+    if "costAmount" in message and "budgetAmount" in message:
+        return float(message["costAmount"]) >= float(message["budgetAmount"])
+    return message.get("incident", {}).get("state") == "open"
+
+
+@functions_framework.cloud_event
+def handle(cloud_event) -> None:
+    message = json.loads(base64.b64decode(cloud_event.data["message"]["data"]))
+    if not should_stop(message):
+        return
+    bucket = storage.Client().bucket(BUCKET)
+    policy = bucket.get_iam_policy(requested_policy_version=3)
+    changed = False
+    for binding in policy.bindings:
+        if "allUsers" in binding["members"]:
+            binding["members"].discard("allUsers")
+            changed = True
+    policy.bindings = [b for b in policy.bindings if b["members"]]
+    if changed:
+        bucket.set_iam_policy(policy)
+        print(f"Removed public read from gs://{BUCKET}: {json.dumps(message)[:500]}")

scripts/cache/kill-switch/requirements.txt

@@ -0,0 +1,2 @@
+functions-framework==3.8.2
+google-cloud-storage==2.19.0