release_cache.yml

name: publish release cache

# Publishes the Mathlib cache for every release tag.
#
# Master CI leaves two kinds of release commit without a cache:
#   - Patch releases (`v4.X.Y` with Y ≥ 1) and patched release candidates
#     (e.g. `v4.32.0-rc1-patch1`) live on `bump_to_*` branches outside
#     `master`. Their branch CI writes the fork-trust container, and a
#     canonical checkout at the tag reads only `master`.
#   - Bors lands a batch of commits at once, and CI builds only the last one.
#     A tag on an earlier commit of the batch has no build.
# This workflow builds the tagged commit and publishes the result to the
# `master` container. When master CI already cached the commit, the build is
# a full cache hit: it stages no files and skips both upload jobs.
#
# Trust model:
#   - Creating a `v4.*` tag is restricted to release managers by a tag
#     ruleset, so a tag push is a deliberate release-manager action — and the
#     tagged tree is what runs here, including this workflow file. Tags on
#     lineages older than this file do not trigger it.
#   - The upload job mints its OIDC token under the `cache-upload-master`
#     environment (inside build_template.yml); the environment's deployment
#     policy admits only `master`, `staging`, and `v4.*` tag refs.
#
# Retry: re-run a failed run with "Re-run failed jobs" or `gh run rerun`. The
# re-run builds the same tag and tree, and needs no tag re-push. The
# `workflow_dispatch` trigger covers what re-run cannot: a tag push that never
# produced a run, or a re-run window that has expired. Dispatch it AT the tag
# ref (`gh workflow run release_cache.yml --ref v4.X.Y`); the run then executes
# the tag's own tree exactly as a tag push would.

on:
  push:
    tags:
      - 'v4.*'
  # Manual fallback; see the retry note above. The `tags` filter does not
  # apply to dispatches — the build job's ref guards enforce it instead, so a
  # dispatch on a branch ref skips cleanly.
  workflow_dispatch:

# `v4.*` tags are immutable (the tag ruleset blocks updates), so this group
# only ever collides on re-runs of the same tag; keep those queued rather
# than cancelled.
concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}

# Read-only by default; the build job elevates for itself only.
permissions:
  contents: read

jobs:
  build:
    name: ci
    # The ref guards double as the dispatch-path filter; on the push path the
    # `tags` trigger filter has already enforced them.
    if: ${{ github.repository == 'leanprover-community/mathlib4' && github.ref_type == 'tag' && startsWith(github.ref_name, 'v4.') }}
    # What build_template.yml needs, granted to this job only — the same set
    # build.yml grants it on push events. In particular, the OIDC token for
    # the cache upload can be minted here and nowhere else in this workflow.
    permissions:
      contents: read
      id-token: write
      actions: read  # Allow get-tools to download the prebuilt tools artifact from master's publish_tools runs
      pull-requests: write  # Only allow PR comments/labels
    uses: ./.github/workflows/build_template.yml
    with:
      concurrency_group: ${{ github.workflow }}-${{ github.ref }}
      pr_branch_ref: ${{ github.sha }}
      # Release tags publish to the `master` container; see the trust note above
      # and cache-trust-dispatch, which routes `v4.*` tag refs to that container.
      cache_environment: cache-upload-master
      # The cache-snapshot warming artifact exists to seed master and PR
      # builds, which a release tag's snapshot cannot do.
      publish_cache: false
      # Skip the Post-CI job: it grooms PR labels, and a tag run has no PR.
      run_post_ci: false
      runs_on: pr
    secrets: inherit