Skip to content

Commit a4bd14a

Browse files
marcelolynchclaude
marcelolynch
and
claude
committed
ci: publish the cache for off-master release tags
Patch releases and patched release candidates are committed on bump_to_* branches that are not ancestors of master, so the master push build never caches them, while a canonical checkout at the tag reads the master-first container chain. A new v4.*-tag-triggered workflow rebuilds the tagged commit (skipping tags whose commit is on master) and publishes its cache to the master container under the master writer identity, gated by the cache-upload-master environment whose deployment policy admits v4.* tags. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
1 parent eb6a272 commit a4bd14a

5 files changed

Lines changed: 159 additions & 33 deletions

File tree

‎.github/actions/cache-trust-dispatch/action.yml‎

Lines changed: 58 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
# Single source of truth mapping (repo, branch) → (upload container,
1+
# Single source of truth mapping (repo, ref) → (upload container,
22
# read fallback chain) for Mathlib's multi-container cache.
33
#
44
# Called by build, upload_cache, and post_steps in build_template.yml so
@@ -14,7 +14,10 @@ inputs:
1414
description: GitHub repo full name (`owner/name`).
1515
required: true
1616
branch:
17-
description: Branch name (`github.head_ref || github.ref_name`).
17+
description: |
18+
Branch name (`github.head_ref || github.ref_name`); on tag-triggered
19+
runs this is the tag name, distinguished via `github.ref_type` inside
20+
the dispatch step.
1821
required: true
1922
head-sha:
2023
description: |
@@ -55,6 +58,10 @@ runs:
5558
REPO="${{ inputs.repo }}"
5659
BRANCH="${{ inputs.branch }}"
5760
HEAD_SHA="${{ inputs.head-sha }}"
61+
# Whether `branch` names a branch or a tag. Read from the run context
62+
# rather than an input: unlike `repo`/`branch`, the value does not
63+
# depend on which event shape (PR vs push) the caller handles.
64+
REF_TYPE="${{ github.ref_type }}"
5865
PRIMARY=""
5966
READ_CHAIN=""
6067
REPO_SCOPE=""
@@ -80,30 +87,55 @@ runs:
8087
else
8188
case "$REPO" in
8289
"leanprover-community/mathlib4")
83-
case "$BRANCH" in
84-
"master"|"staging")
85-
# Master / staging are the only writers that feed `master`
86-
# (`staging` is bors's merge candidate, which fast-forwards to
87-
# `master`). Read `master` only, not the default [master,
88-
# legacy]: files the read chain serves are skipped at stage
89-
# time, so keeping `legacy` would leave legacy-only files out of
90-
# `master` for good. Reading `master` alone turns them into
91-
# misses that get rebuilt and uploaded, so `master` fills itself
92-
# into a standalone cache. (Only PRIMARY=master does this; other
93-
# runs write to `forks` and keep the wider chain.)
94-
PRIMARY="master"
95-
READ_CHAIN="master"
96-
;;
97-
*)
98-
# `bors trying`, `ci-dev/*`, maintainer dev branches on the
99-
# canonical repo: trust level is fork-equivalent (the OIDC
100-
# token's RBAC scopes them to `forks`). Reads must widen
101-
# past the default [master, legacy] so the post-build
102-
# verification finds the just-uploaded fork-trust artifacts.
103-
PRIMARY="forks"
104-
READ_CHAIN="master,forks,legacy"
105-
;;
106-
esac
90+
if [ "$REF_TYPE" = "tag" ]; then
91+
case "$BRANCH" in
92+
v4.*)
93+
# `v4.*` release tags: release_cache.yml rebuilds off-master
94+
# release commits (patch releases, patched release
95+
# candidates) and publishes them into `master`, the container
96+
# canonical checkouts read. Tag creation is restricted to
97+
# release managers by a tag ruleset, and the
98+
# `cache-upload-master` environment admits `v4.*` tag refs,
99+
# so these builds carry master trust. Reads are `master`-only
100+
# for the same fill-in reason as the master/staging arm
101+
# below.
102+
PRIMARY="master"
103+
READ_CHAIN="master"
104+
;;
105+
*)
106+
# Other tags have no trust class of their own:
107+
# fork-equivalent, like the dev-branch arm below.
108+
PRIMARY="forks"
109+
READ_CHAIN="master,forks,legacy"
110+
;;
111+
esac
112+
else
113+
case "$BRANCH" in
114+
"master"|"staging")
115+
# Master, staging, and `v4.*` release tags (above) are the
116+
# only writers that feed `master` (`staging` is bors's merge
117+
# candidate, which fast-forwards to `master`). Read `master`
118+
# only, not the default [master, legacy]: files the read
119+
# chain serves are skipped at stage time, so keeping `legacy`
120+
# would leave legacy-only files out of `master` for good.
121+
# Reading `master` alone turns them into misses that get
122+
# rebuilt and uploaded, so `master` fills itself into a
123+
# standalone cache. (Only PRIMARY=master does this; other
124+
# runs write to `forks` and keep the wider chain.)
125+
PRIMARY="master"
126+
READ_CHAIN="master"
127+
;;
128+
*)
129+
# `bors trying`, `ci-dev/*`, maintainer dev branches on the
130+
# canonical repo: trust level is fork-equivalent (the OIDC
131+
# token's RBAC scopes them to `forks`). Reads must widen
132+
# past the default [master, legacy] so the post-build
133+
# verification finds the just-uploaded fork-trust artifacts.
134+
PRIMARY="forks"
135+
READ_CHAIN="master,forks,legacy"
136+
;;
137+
esac
138+
fi
107139
;;
108140
"leanprover-community/mathlib4-nightly-testing")
109141
case "$BRANCH" in

‎.github/workflows/build_template.yml‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
1-
# Reusable workflow invoked by build.yml, bors.yml, build_fork.yml, and ci_dev.yml.
1+
# Reusable workflow invoked by build.yml, bors.yml, build_fork.yml, ci_dev.yml,
2+
# and release_cache.yml.
23

34
on:
45
workflow_call:

‎.github/workflows/release_cache.yml‎

Lines changed: 90 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,90 @@
1+
name: publish release cache
2+
3+
# Publishes the Mathlib cache for release tags whose commits are not on
4+
# `master`.
5+
#
6+
# Patch releases (`v4.X.Y` with Y ≥ 1) and patched release candidates (e.g.
7+
# `v4.32.0-rc1-patch1`) are committed on `bump_to_*` branches that never merge
8+
# back into `master`, so the master push build never caches them; their branch
9+
# CI writes only the fork-trust container, which a canonical checkout at the
10+
# tag never reads. This workflow rebuilds the tagged commit and publishes the
11+
# result to the `master` container, where every consumer finds it. Tags that
12+
# point at commits on `master` (plain release candidates and `.0` releases)
13+
# are already cached by the master push build, so the gate job skips them.
14+
#
15+
# Trust model:
16+
# - Creating a `v4.*` tag is restricted to release managers by a tag
17+
# ruleset, so a tag push is a deliberate release-manager action — and the
18+
# tagged tree is what runs here, including this workflow file. Tags cut
19+
# from lineages predating this file simply never trigger it.
20+
# - The upload job mints its OIDC token under the `cache-upload-master`
21+
# environment (inside build_template.yml); the environment's deployment
22+
# policy admits only `master`, `staging`, and `v4.*` tag refs.
23+
24+
on:
25+
push:
26+
tags:
27+
- 'v4.*'
28+
29+
# `v4.*` tags are immutable (the tag ruleset blocks updates), so this group
30+
# only ever collides on re-runs of the same tag; keep those queued rather
31+
# than cancelled.
32+
concurrency:
33+
group: ${{ github.workflow }}-${{ github.ref }}
34+
35+
# Read-only by default; the build job elevates for itself only.
36+
permissions:
37+
contents: read
38+
39+
jobs:
40+
gate:
41+
name: skip tags already on master
42+
if: ${{ github.repository == 'leanprover-community/mathlib4' }}
43+
runs-on: ubuntu-latest
44+
outputs:
45+
off_master: ${{ steps.check.outputs.off_master }}
46+
steps:
47+
- uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
48+
with:
49+
# `merge-base` needs the commit graph, not trees: fetch the full
50+
# history of every ref, treeless.
51+
fetch-depth: 0
52+
filter: tree:0
53+
54+
- name: check whether the tagged commit is on master
55+
id: check
56+
run: |
57+
if git merge-base --is-ancestor "$GITHUB_SHA" origin/master; then
58+
echo "Tag $GITHUB_REF_NAME points at a commit on master; the master push build covers its cache."
59+
echo "off_master=false" >> "$GITHUB_OUTPUT"
60+
else
61+
echo "Tag $GITHUB_REF_NAME is not on master; rebuilding it to publish its cache."
62+
echo "off_master=true" >> "$GITHUB_OUTPUT"
63+
fi
64+
65+
build:
66+
name: ci
67+
needs: gate
68+
if: ${{ needs.gate.outputs.off_master == 'true' }}
69+
# What build_template.yml needs, granted to this job only — the same set
70+
# build.yml grants it on push events. In particular, the OIDC token for
71+
# the cache upload can be minted here and nowhere else in this workflow.
72+
permissions:
73+
contents: read
74+
id-token: write
75+
actions: read # Allow get-tools to download the prebuilt tools artifact from master's publish_tools runs
76+
pull-requests: write # Only allow PR comments/labels
77+
uses: ./.github/workflows/build_template.yml
78+
with:
79+
concurrency_group: ${{ github.workflow }}-${{ github.ref }}
80+
pr_branch_ref: ${{ github.sha }}
81+
# Release tags publish to the `master` container under the master writer
82+
# identity; see the trust note above and cache-trust-dispatch, which
83+
# routes `v4.*` tag refs to that container.
84+
cache_application_id: ${{ vars.CACHE_MASTER_WRITER_AZURE_APP_ID }}
85+
cache_environment: cache-upload-master
86+
# The cache-snapshot warming artifact exists to seed master and PR
87+
# builds, which a release tag's snapshot cannot do.
88+
publish_cache: false
89+
runs_on: pr
90+
secrets: inherit

‎Cache/Infra.lean‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,9 @@ account. A CI job at a given trust level may write only to its corresponding
4848
container, and `cache get` always tries the most trusted container first.
4949
-/
5050
inductive Container where
51-
/-- Most-trusted container (`mathlib4-master`); only master CI writes here. -/
51+
/-- Most-trusted container (`mathlib4-master`); written only by master CI and
52+
by `v4.*` release-tag CI, which publishes release commits that are not on
53+
`master` (patch releases, patched release candidates). -/
5254
| master
5355
/-- Container for PR builds on forks of mathlib4. -/
5456
| forks
@@ -111,8 +113,9 @@ artifacts from several writers whose `repo` need not match the container's
111113
trust level, and a stable per-container layout is what keeps readers and
112114
writers in sync.
113115
114-
- `master` is flat: RBAC admits only master CI, whose writes all carry
115-
`repo == MATHLIBREPO`, so a single hash never collides.
116+
- `master` is flat: RBAC admits only master CI and `v4.*` release-tag CI,
117+
whose writes all carry `repo == MATHLIBREPO`, so a single hash never
118+
collides.
116119
- `legacy` keys the layout on the writer: `MATHLIBREPO` writes are flat (where
117120
older `mathlib4` readers look for them), fork writes are repo-namespaced.
118121
- `forks`, `nightly-testing`, and `pr-toolchain-tests` always namespace by

‎Cache/SECURITY.md‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ CI job and assigned a trust level:
2121

2222
| Container | Who may write | Trust |
2323
|-----------------------|--------------------------------------------------------|--------|
24-
| `master` | mathlib4 `master`/`staging` | high |
24+
| `master` | mathlib4 `master`/`staging`, `v4.*` release tags | high |
2525
| `forks` | mathlib4 PR builds, non-master branches, `bors try` | medium |
2626
| `nightly-testing` | nightly-testing's trusted branches | medium |
2727
| `pr-toolchain-tests` | nightly-testing's experimental toolchain branches | low |
@@ -148,5 +148,5 @@ The trust model does not attempt to defend against:
148148
| Trust property tests | [`Cache/Test.lean`](Test.lean) |
149149
| User-facing CLI surface, env vars | [`Cache/Main.lean`](Main.lean), [`Cache/README.md`](README.md) |
150150
| OIDC mint + per-job dispatch | [`.github/workflows/build_template.yml`](../.github/workflows/build_template.yml) (`upload_cache` job) |
151-
| (repo, branch) → trust class policy table | [`.github/actions/cache-trust-dispatch/action.yml`](../.github/actions/cache-trust-dispatch/action.yml) |
152-
| Caller `cache_application_id` ternaries | [`.github/workflows/build.yml`](../.github/workflows/build.yml), [`bors.yml`](../.github/workflows/bors.yml), [`build_fork.yml`](../.github/workflows/build_fork.yml), [`ci_dev.yml`](../.github/workflows/ci_dev.yml) |
151+
| (repo, ref) → trust class policy table | [`.github/actions/cache-trust-dispatch/action.yml`](../.github/actions/cache-trust-dispatch/action.yml) |
152+
| Caller `cache_application_id` wiring | [`.github/workflows/build.yml`](../.github/workflows/build.yml), [`bors.yml`](../.github/workflows/bors.yml), [`build_fork.yml`](../.github/workflows/build_fork.yml), [`ci_dev.yml`](../.github/workflows/ci_dev.yml), [`release_cache.yml`](../.github/workflows/release_cache.yml) |

0 commit comments

Comments
 (0)