diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index e84f90096..4d4884b00 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.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 }}" diff --git a/AGENTS.md b/AGENTS.md index 2aaa1dabb..c005eb951 100644 --- a/AGENTS.md +++ b/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 diff --git a/README.md b/README.md index d04a8d678..52865c78b 100644 --- a/README.md +++ b/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+): diff --git a/lakefile.toml b/lakefile.toml index 561aa0627..4e2e40ee1 100644 --- a/lakefile.toml +++ b/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. diff --git a/scripts/cache/README.md b/scripts/cache/README.md new file mode 100644 index 000000000..352a1dd72 --- /dev/null +++ b/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= BILLING_ACCOUNT= ALERT_EMAIL=
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/.art` holds module archives and +`r0/cslib-community/complexitylib/tc//.jsonl` the input-to-output mappings of +each commit, as written by `scripts/cache/upload.sh` and read by `lake cache get`. diff --git a/scripts/cache/get.sh b/scripts/cache/get.sh new file mode 100755 index 000000000..aa51a381b --- /dev/null +++ b/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 diff --git a/scripts/cache/kill-switch/main.py b/scripts/cache/kill-switch/main.py new file mode 100644 index 000000000..76861b226 --- /dev/null +++ b/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]}") diff --git a/scripts/cache/kill-switch/requirements.txt b/scripts/cache/kill-switch/requirements.txt new file mode 100644 index 000000000..68a778e3a --- /dev/null +++ b/scripts/cache/kill-switch/requirements.txt @@ -0,0 +1,2 @@ +functions-framework==3.8.2 +google-cloud-storage==2.19.0 diff --git a/scripts/cache/setup-gcs.sh b/scripts/cache/setup-gcs.sh new file mode 100755 index 000000000..21951c271 --- /dev/null +++ b/scripts/cache/setup-gcs.sh @@ -0,0 +1,188 @@ +#!/usr/bin/env bash +# One-time maintainer setup of the remote build cache on Google Cloud. See scripts/cache/README.md. +# +# Usage: +# PROJECT= BILLING_ACCOUNT= [ALERT_EMAIL=
] \ +# scripts/cache/setup-gcs.sh [step...] +# +# Steps (default: all, in order): project bucket writer budget killswitch alert variables. +# Each step can be rerun on its own. Optional settings: BUCKET (complexitylib-lake-cache), +# REGION (us-east1, inside Cloud Storage's free tier), BUDGET_USD (10), EGRESS_ALERT_GB (20 per +# hour). Billing account and e-mail are arguments so that they never enter the repository. +set -euo pipefail +cd "$(dirname "$0")" + +: "${PROJECT:?set PROJECT to the id of a new, dedicated Google Cloud project}" +BUCKET="${BUCKET:-complexitylib-lake-cache}" +REGION="${REGION:-us-east1}" +BUDGET_USD="${BUDGET_USD:-10}" +EGRESS_ALERT_GB="${EGRESS_ALERT_GB:-20}" +REPO="cslib-community/complexitylib" +REPO_ID="1420662136" # `gh api repos/cslib-community/complexitylib --jq .id` +WRITER="lake-cache-writer@$PROJECT.iam.gserviceaccount.com" +KILLER="lake-cache-kill-switch@$PROJECT.iam.gserviceaccount.com" +TOPIC="lake-cache-limits" +POOL="github" +PROVIDER="complexitylib" + +gc() { echo "+ gcloud $*" >&2; gcloud "$@"; } +project_number() { gcloud projects describe "$PROJECT" --format='value(projectNumber)'; } + +step_project() { + gcloud projects describe "$PROJECT" >/dev/null 2>&1 || gc projects create "$PROJECT" + gc billing projects link "$PROJECT" --billing-account="${BILLING_ACCOUNT:?set BILLING_ACCOUNT}" + gc services enable --project="$PROJECT" storage.googleapis.com iam.googleapis.com \ + iamcredentials.googleapis.com sts.googleapis.com pubsub.googleapis.com \ + billingbudgets.googleapis.com monitoring.googleapis.com cloudfunctions.googleapis.com \ + run.googleapis.com cloudbuild.googleapis.com artifactregistry.googleapis.com \ + eventarc.googleapis.com +} + +step_bucket() { + gcloud storage buckets describe "gs://$BUCKET" >/dev/null 2>&1 || + gc storage buckets create "gs://$BUCKET" --project="$PROJECT" --location="$REGION" \ + --uniform-bucket-level-access --soft-delete-duration=0 --default-storage-class=STANDARD + # Revision mappings older than 180 days are dropped; artifacts are shared between revisions + # and are pruned separately (README: "Pruning"). + local lifecycle + lifecycle="$(mktemp)" + echo '{"rule":[{"action":{"type":"Delete"},"condition":{"age":180,"matchesPrefix":["r0/"]}}]}' \ + > "$lifecycle" + gc storage buckets update "gs://$BUCKET" --no-versioning --lifecycle-file="$lifecycle" + rm -f "$lifecycle" + # Anyone may read an object by name (Lake downloads without credentials); nobody may list. + gc storage buckets add-iam-policy-binding "gs://$BUCKET" \ + --member=allUsers --role=roles/storage.legacyObjectReader +} + +step_writer() { + gcloud iam workload-identity-pools describe "$POOL" --project="$PROJECT" --location=global \ + >/dev/null 2>&1 || + gc iam workload-identity-pools create "$POOL" --project="$PROJECT" --location=global \ + --display-name="GitHub Actions" + gcloud iam workload-identity-pools providers describe "$PROVIDER" --project="$PROJECT" \ + --location=global --workload-identity-pool="$POOL" >/dev/null 2>&1 || + gc iam workload-identity-pools providers create-oidc "$PROVIDER" --project="$PROJECT" \ + --location=global --workload-identity-pool="$POOL" \ + --issuer-uri=https://token.actions.githubusercontent.com \ + --attribute-mapping='google.subject=assertion.sub,attribute.repository_id=assertion.repository_id,attribute.ref=assertion.ref,attribute.event_name=assertion.event_name' \ + --attribute-condition="assertion.repository_id == '$REPO_ID' && assertion.ref == 'refs/heads/main' && assertion.event_name == 'push'" + gcloud iam service-accounts describe "$WRITER" --project="$PROJECT" >/dev/null 2>&1 || + gc iam service-accounts create lake-cache-writer --project="$PROJECT" \ + --display-name="Complexitylib main CI cache upload" + # Create and read, but no delete, so existing objects cannot be overwritten. + for role in roles/storage.objectCreator roles/storage.objectViewer; do + gc storage buckets add-iam-policy-binding "gs://$BUCKET" \ + --member="serviceAccount:$WRITER" --role="$role" + done + gc iam service-accounts add-iam-policy-binding "$WRITER" --project="$PROJECT" \ + --role=roles/iam.workloadIdentityUser \ + --member="principalSet://iam.googleapis.com/projects/$(project_number)/locations/global/workloadIdentityPools/$POOL/attribute.repository_id/$REPO_ID" +} + +step_budget() { + gcloud pubsub topics describe "$TOPIC" --project="$PROJECT" >/dev/null 2>&1 || + gc pubsub topics create "$TOPIC" --project="$PROJECT" + gc billing budgets create --billing-account="${BILLING_ACCOUNT:?set BILLING_ACCOUNT}" \ + --display-name="Complexitylib remote cache" --budget-amount="${BUDGET_USD}USD" \ + --filter-projects="projects/$PROJECT" \ + --threshold-rule=percent=0.5 --threshold-rule=percent=0.9 --threshold-rule=percent=1.0 \ + --notifications-rule-pubsub-topic="projects/$PROJECT/topics/$TOPIC" +} + +step_killswitch() { + gcloud iam service-accounts describe "$KILLER" --project="$PROJECT" >/dev/null 2>&1 || + gc iam service-accounts create lake-cache-kill-switch --project="$PROJECT" \ + --display-name="Complexitylib cache kill switch" + gcloud iam roles describe lakeCacheKillSwitch --project="$PROJECT" >/dev/null 2>&1 || + gc iam roles create lakeCacheKillSwitch --project="$PROJECT" \ + --title="Remove public access from the cache bucket" \ + --permissions=storage.buckets.get,storage.buckets.getIamPolicy,storage.buckets.setIamPolicy + # A new custom role takes a minute or two to become grantable. + local attempt + for attempt in 1 2 3 4 5 6; do + gc storage buckets add-iam-policy-binding "gs://$BUCKET" --member="serviceAccount:$KILLER" \ + --role="projects/$PROJECT/roles/lakeCacheKillSwitch" >/dev/null && break + [ "$attempt" -lt 6 ] || return 1 + echo "Role not yet grantable; retrying in 30 s" >&2 + sleep 30 + done + gc functions deploy lake-cache-kill-switch --project="$PROJECT" --region="$REGION" --gen2 \ + --runtime=python312 --source=kill-switch --entry-point=handle --trigger-topic="$TOPIC" \ + --service-account="$KILLER" --trigger-service-account="$KILLER" \ + --set-env-vars="BUCKET=$BUCKET" --max-instances=1 --ingress-settings=internal-only + # The trigger delivers messages as $KILLER, which must be allowed to invoke the function. + gc run services add-iam-policy-binding lake-cache-kill-switch --project="$PROJECT" \ + --region="$REGION" --member="serviceAccount:$KILLER" --role=roles/run.invoker >/dev/null +} + +# channel