From 34303613ab2b14340a461211886855afd529d90b Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 23 Oct 2026 14:48:49 -0400 Subject: [PATCH 1/6] chore(build): share build outputs through local and remote Lake caches Enable Lake's local artifact cache, so a module built in one checkout is reused by every other checkout on the machine, and add a remote cache that `main` CI fills and `scripts/cache/get.sh` reads. - lakefile.toml: enableArtifactCache, restoreAllArtifacts (outputs 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). - scripts/cache/upload.sh: stages the outputs of Complexity and ComplexityTests and uploads only new artifacts, then the commit's mapping, in the layout `lake cache get` reads. - CI: records the build's mappings as an artifact; on `main` pushes, uploads once the repository variables exist (OIDC through Workload Identity Federation, no stored secrets). - scripts/cache/setup-gcs.sh and kill-switch/: maintainer setup of the bucket (public read without listing, create-only writer), budget, egress alert and a kill switch that removes public read. - README, AGENTS.md and scripts/cache/README.md document use, trust and maintenance. Refs #512. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/lean_action_ci.yml | 28 ++++ AGENTS.md | 6 + README.md | 6 +- lakefile.toml | 9 ++ scripts/cache/README.md | 81 +++++++++++ scripts/cache/get.sh | 22 +++ scripts/cache/kill-switch/main.py | 45 ++++++ scripts/cache/kill-switch/requirements.txt | 2 + scripts/cache/setup-gcs.sh | 158 +++++++++++++++++++++ scripts/cache/upload.sh | 43 ++++++ 10 files changed, 399 insertions(+), 1 deletion(-) create mode 100644 scripts/cache/README.md create mode 100755 scripts/cache/get.sh create mode 100644 scripts/cache/kill-switch/main.py create mode 100644 scripts/cache/kill-switch/requirements.txt create mode 100755 scripts/cache/setup-gcs.sh create mode 100755 scripts/cache/upload.sh diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index e84f90096..86613f42f 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,26 @@ jobs: run: | set -e lake exe checkInitImports + # Input-to-output mappings of this build, for diagnosing remote-cache misses. + - name: "Record build-output mappings" + run: | + set -e + lake build Complexity ComplexityTests -o lake-mappings.jsonl + - uses: actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9 # v7.0.2 + with: + name: lake-mappings + path: lake-mappings.jsonl + retention-days: 14 + # 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..bb6ee904d --- /dev/null +++ b/scripts/cache/setup-gcs.sh @@ -0,0 +1,158 @@ +#!/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" --versioning=false --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 + gc storage buckets add-iam-policy-binding "gs://$BUCKET" --member="serviceAccount:$KILLER" \ + --role="projects/$PROJECT/roles/lakeCacheKillSwitch" + 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" --set-env-vars="BUCKET=$BUCKET" --max-instances=1 +} + +step_alert() { + # Billing data lags by hours; this fires within minutes of an unusual download rate, notifies + # the maintainer (when ALERT_EMAIL is set) and triggers the kill switch through the topic. + local channels policy + gc pubsub topics add-iam-policy-binding "$TOPIC" --project="$PROJECT" --role=roles/pubsub.publisher \ + --member="serviceAccount:service-$(project_number)@gcp-sa-monitoring-notification.iam.gserviceaccount.com" + channels="$(gc beta monitoring channels create --project="$PROJECT" --type=pubsub \ + --display-name="Cache kill switch" --channel-labels="topic=projects/$PROJECT/topics/$TOPIC" \ + --format='value(name)')" + if [ -n "${ALERT_EMAIL:-}" ]; then + channels="$channels,$(gc beta monitoring channels create --project="$PROJECT" --type=email \ + --display-name="Cache maintainer" --channel-labels="email_address=$ALERT_EMAIL" \ + --format='value(name)')" + fi + policy="$(mktemp)" + cat > "$policy" <&2 + "step_$step" +done diff --git a/scripts/cache/upload.sh b/scripts/cache/upload.sh new file mode 100755 index 000000000..803fe3494 --- /dev/null +++ b/scripts/cache/upload.sh @@ -0,0 +1,43 @@ +#!/usr/bin/env bash +# Upload this checkout's build outputs to the remote cache. Run by `main` CI after a successful +# build; it needs write access to the bucket and is not meant for local use. +# +# Usage: scripts/cache/upload.sh +# +# Object layout (the one `lake cache put --repo=cslib-community/complexitylib` produces, which +# `lake cache get` reads; artifacts are content-addressed module archives): +# gs:///a0/cslib-community/complexitylib/.art +# gs:///r0/cslib-community/complexitylib/tc//.jsonl +# `lake cache put` re-uploads every artifact on each run; this script uploads only new ones +# (`--no-clobber`) and writes the revision mapping last, so a published mapping never refers to +# a missing artifact. The writer cannot overwrite objects, so published artifacts are immutable. +set -euo pipefail +cd "$(dirname "$0")/../.." + +bucket="${1:?Usage: scripts/cache/upload.sh }" +scope="cslib-community/complexitylib" +rev="$(git rev-parse HEAD)" +if [ -n "$(git status --porcelain --untracked-files=no)" ]; then + echo "Refusing to upload: the work tree differs from $rev." >&2 + exit 1 +fi +# `leanprover/lean4:v4.36.0` → `leanprover--lean4---v4.36.0`, as Lake names toolchain scopes. +toolchain="$(tr -d '[:space:]' < lean-toolchain | sed 's#/#--#; s#:#---#')" + +stage="$(mktemp -d "${TMPDIR:-/tmp}/complexitylib-cache.XXXXXX")" +trap 'rm -rf "$stage"' EXIT +lake build Complexity ComplexityTests -o "$stage/mappings.jsonl" +lake cache stage "$stage/mappings.jsonl" "$stage/out" +mkdir "$stage/art" +for f in "$stage"/out/*.ltar; do + base="$(basename "$f" .ltar)" + mv "$f" "$stage/art/$base.art" +done +count="$(find "$stage/art" -name '*.art' | wc -l | tr -d ' ')" +echo "Uploading up to $count artifacts for $rev (existing objects are skipped)" +find "$stage/art" -name '*.art' | gcloud storage cp --no-clobber --quiet \ + --content-type=application/vnd.reservoir.artifact -I "gs://$bucket/a0/$scope/" +gcloud storage cp --no-clobber --quiet \ + --content-type=application/vnd.reservoir.outputs+json-lines \ + "$stage/mappings.jsonl" "gs://$bucket/r0/$scope/tc/$toolchain/$rev.jsonl" +echo "Published gs://$bucket/r0/$scope/tc/$toolchain/$rev.jsonl" From 6797c5d03efe0011759553352580c09d012caa4d Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 23 Oct 2026 15:06:00 -0400 Subject: [PATCH 2/6] fix(cache): disable bucket versioning with --no-versioning Co-Authored-By: Claude Opus 5.5 --- scripts/cache/setup-gcs.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/cache/setup-gcs.sh b/scripts/cache/setup-gcs.sh index bb6ee904d..6e4c8aae0 100755 --- a/scripts/cache/setup-gcs.sh +++ b/scripts/cache/setup-gcs.sh @@ -48,7 +48,7 @@ step_bucket() { lifecycle="$(mktemp)" echo '{"rule":[{"action":{"type":"Delete"},"condition":{"age":180,"matchesPrefix":["r0/"]}}]}' \ > "$lifecycle" - gc storage buckets update "gs://$BUCKET" --versioning=false --lifecycle-file="$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" \ From 4a549152a0bea5991ded210910a37463855b08cd Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 23 Oct 2026 15:11:07 -0400 Subject: [PATCH 3/6] fix(cache): retry granting the new kill-switch role until it propagates Co-Authored-By: Claude Opus 5.5 --- scripts/cache/setup-gcs.sh | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/scripts/cache/setup-gcs.sh b/scripts/cache/setup-gcs.sh index 6e4c8aae0..6d3d056d0 100755 --- a/scripts/cache/setup-gcs.sh +++ b/scripts/cache/setup-gcs.sh @@ -98,8 +98,15 @@ step_killswitch() { 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 - gc storage buckets add-iam-policy-binding "gs://$BUCKET" --member="serviceAccount:$KILLER" \ - --role="projects/$PROJECT/roles/lakeCacheKillSwitch" + # 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" --set-env-vars="BUCKET=$BUCKET" --max-instances=1 From b0109592d1e5747452c73b16afadf26a0aa6cff7 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 23 Oct 2026 15:14:52 -0400 Subject: [PATCH 4/6] fix(cache): let the kill-switch trigger invoke the function; internal ingress only Co-Authored-By: Claude Opus 5.5 --- scripts/cache/setup-gcs.sh | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/scripts/cache/setup-gcs.sh b/scripts/cache/setup-gcs.sh index 6d3d056d0..8badcd148 100755 --- a/scripts/cache/setup-gcs.sh +++ b/scripts/cache/setup-gcs.sh @@ -109,7 +109,11 @@ step_killswitch() { 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" --set-env-vars="BUCKET=$BUCKET" --max-instances=1 + --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 } step_alert() { From 6f4b9c6735770c804e63307f2702bf62f1d24ce2 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 23 Oct 2026 15:18:54 -0400 Subject: [PATCH 5/6] fix(cache): create Monitoring's notification agent before granting it the topic Reuse existing notification channels so the alert step can be rerun. Co-Authored-By: Claude Opus 5.5 --- scripts/cache/setup-gcs.sh | 37 ++++++++++++++++++++++++++++--------- 1 file changed, 28 insertions(+), 9 deletions(-) diff --git a/scripts/cache/setup-gcs.sh b/scripts/cache/setup-gcs.sh index 8badcd148..21951c271 100755 --- a/scripts/cache/setup-gcs.sh +++ b/scripts/cache/setup-gcs.sh @@ -116,19 +116,38 @@ step_killswitch() { --region="$REGION" --member="serviceAccount:$KILLER" --role=roles/run.invoker >/dev/null } +# channel