build_template.yml

# Reusable workflow invoked by build.yml, bors.yml, build_fork.yml, and ci_dev.yml.

on:
  workflow_call:
    inputs:
      concurrency_group:
        type: string
        required: true
      tools_branch_ref:
        type: string
        required: false
        default: ''
      pr_branch_ref:
        type: string
        required: true
      run_post_ci:
        type: boolean
        required: false
        default: true
      runs_on:
        type: string
        required: true
      mathlib_ci_ref:
        type: string
        required: false
        default: ''
      cache_application_id:
        type: string
        required: true
      cache_environment:
        # GitHub environment for the `upload_cache` job. Its only role is to fix the
        # OIDC `sub` claim to `...:environment:<name>`, which the Azure cache app's
        # federated credential is scoped to; it must match the writer `cache_application_id`.
        type: string
        required: true
      publish_cache:
        # On a successful build, publish this run's `.ltar` set as `cache-snapshot`.
        # Set by callers ONLY for the master-`push` build — the single producer.
        type: boolean
        required: false
        default: false

env:
  # Disable Lake's automatic fetching of cloud builds.
  # Lake's cache is currently incompatible with Mathlib's `lake exe cache`.
  # This is because Mathlib's Cache assumes all build artifacts present in the build directory
  # are valid by-products of the Mathlib build. Build artifacts fetched from Lake's cache do
  # not necessarily satisfy this property.
  LAKE_NO_CACHE: true

jobs:
  build:
    name: Build
    runs-on: ${{ inputs.runs_on }}
    outputs:
      build-outcome: ${{ steps.build.outcome }}
      archive-outcome: ${{ steps.archive.outcome }}
      counterexamples-outcome: ${{ steps.counterexamples.outcome }}
      cache-staging-has-files: ${{ steps.cache_staging_check.outputs.has_files }}
      mk_all-outcome: ${{ steps.mk_all.outcome }}
      noisy-outcome: ${{ steps.noisy.outcome }}
      # shake-outcome: ${{ steps.shake.outcome }}
      # `test`/`lint` outcomes are exposed by the `test_lint` job (and consumed by
      # its nightly-testing comment step).
    defaults: # On Hoskinson runners, landrun is already installed.
      run: # note that .pr-branch/.lake must be created in a step below before we use this
        shell: landrun --rox /usr --ro /etc/timezone --rw /dev --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rox /home/lean/.cache/mathlib/ --rw pr-branch/.lake/ --env PATH --env HOME --env GITHUB_OUTPUT --env CI -- bash -euxo pipefail {0}
    steps:
      - name: job info
        env:
          WORKFLOW: ${{ github.workflow }}
          PR_NUMBER: ${{ github.event.pull_request.number }}
          REF: ${{ github.ref }}
          EVENT_NAME: ${{ github.event_name }}
          RUN_ID: ${{ github.run_id }}
          CONCURRENCY_GROUP: ${{ inputs.concurrency_group }}
        shell: bash # there is no script body, so this is safe to "run" outside landrun.
        run: |
          # We just populate the env vars for this step to make them viewable in the logs

      - name: Checkout local actions
        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
        with:
          ref: ${{ github.workflow_sha }}
          fetch-depth: 1
          sparse-checkout: .github/actions
          path: workflow-actions

      # Shared self-hosted setup (toolchain prune, jq, cache-trust dispatch,
      # PR-branch checkout, elan + toolchain/LEAN_SRC_PATH env, CI tools, dependency
      # download); see the action for per-step rationale. It is loaded from the
      # `Checkout local actions` checkout above, which therefore runs first.
      - name: Set up build environment
        uses: ./workflow-actions/.github/actions/setup-build-env
        with:
          pr_branch_ref: ${{ inputs.pr_branch_ref }}
          tools_branch_ref: ${{ inputs.tools_branch_ref }}

      # TEMPORARY (cache storage-layout migration, PR #40035): remove once
      # active branches have merged the new cache tool.
      # CI writes the new container layout via the master-built cache binary,
      # but a PR branch that predates the migration ships the old cache tool locally,
      # so `lake exe cache get` on the contributor's machine reads the old layout and misses
      # its own branch's freshly-built artifacts.
      # Hard-fail here (same style as the `lake lint` predates-config gate below in 'lint mathlib')
      #  and tell the author to merge master, which swaps in the new binary.
      # The marker is `Cache/Infra.lean`, a module that only exists post-migration (it replaced `Cache/Init.lean`).
      #
      # TODO: Remove this check eventually. Note that there is no 'correctness' issue if we don't check this:
      #       it's just that locally, the user will not get the artifacts this run has produced (also meaning the upload is 'waste').
      - name: check cache tool is post-migration
        # Canonical repo only. This nudge targets human fork-PR / dev-branch
        # contributors who run `lake exe cache get` locally. The nightly-testing
        # repo's branches (nightly-testing, bump/*, lean-pr-testing-*) are
        # machine-managed and don't merge master the same way, so "merge master
        # and push" is the wrong remedy there; never fail their CI on it.
        if: github.repository == 'leanprover-community/mathlib4'
        shell: bash
        run: |
          if [ ! -f pr-branch/Cache/Infra.lean ]; then
            echo "::error title=Outdated cache tool::Your branch predates the cache storage-layout migration; merge master so 'lake exe cache get' can read your branch's artifacts."
            echo ""
            echo "=============================================================================="
            echo "ERROR: Your branch predates the cache storage-layout migration (PR #40035)."
            echo "Its 'lake exe cache' tool uses outdated infrastructure, so it will miss the"
            echo "artifacts CI builds for your branch and rebuild them locally instead."
            echo "Please merge 'master' into your PR branch and push again."
            echo ""
            echo "You can do this with:"
            echo "  git fetch upstream"
            echo "  git merge upstream/master"
            echo "  git push"
            echo "=============================================================================="
            echo ""
            exit 1
          fi

      - name: Prepare DownstreamTest directory
        shell: bash
        run: |
          echo "Copying lean-toolchain to DownstreamTest..."
          cd pr-branch
          # Ensure DownstreamTest/.lake/ directory exists, since landrun will need it later
          mkdir -p DownstreamTest/.lake/
          cd DownstreamTest
          cp ../lean-toolchain .
          echo "lean-toolchain copied successfully to DownstreamTest."

      - name: validate lake-manifest.json inputRevs
        # Only enforce this on the main mathlib4 repository, not on nightly-testing
        if: github.repository == 'leanprover-community/mathlib4' && github.ref_name != 'nightly-testing'
        shell: bash
        run: |
          cd pr-branch

          # Check that all inputRevs in lake-manifest.json match the required pattern
          echo "Validating lake-manifest.json inputRevs..."

          # Extract all inputRevs from the manifest
          invalid_revs=$(jq -r '.packages[].inputRev // empty' lake-manifest.json | \
            grep -v -E '^(main|master|v[0-9]+\.[0-9]+\.[0-9]+(-[a-zA-Z0-9.-]+)?(\+[a-zA-Z0-9.-]+)?)$' || true)

          if [ -n "$invalid_revs" ]; then
            echo "❌ Error: Found invalid inputRevs in lake-manifest.json:"
            echo "$invalid_revs"
            echo ""
            echo "All inputRevs must be one of:"
            echo "  - 'main'"
            echo "  - 'master'"
            echo "  - 'vX.Y.Z' (semantic version, e.g., v1.2.3, v1.2.3-pre, or v1.2.3+build)"
            exit 1
          else
            echo "✅ All inputRevs in lake-manifest.json are valid"
          fi

      # Get this commit's oleans into the local cache — see the action for the steps.
      - name: Get cache
        uses: ./workflow-actions/.github/actions/get-cache
        with:
          working_directory: pr-branch
          cache_bin: ../tools-branch/.lake/build/bin/cache

      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
        id: mk_all
        continue-on-error: true # Allow workflow to continue, outcome checked later
        # This runs `mk_all --check` from the `pr-branch` inside landrun
        run: |
          cd pr-branch
          echo "Running mk_all --check (from pr-branch)..."
          lake exe mk_all --check

      - name: begin gh-problem-match-wrap for build step
        uses: leanprover-community/gh-problem-matcher-wrap@65a654fcdf7b64ff7633bc7a558f7b46d59a27bf # 2026-06-25
        with:
          action: add # In order to be able to run a multiline script, we need to add/remove the problem matcher before and after.
          linters: lean
      - name: build mathlib
        id: build
        run: |
          cd pr-branch
          echo "::group::{test curl}"
          # Test curl - should fail when landrun network isolation is working
          if curl --silent --head --fail https://www.example.com/ >/dev/null 2>&1; then
            echo "ERROR: curl to example.com succeeded, but it should fail when landrun is working correctly!"
            exit 1
          else
            echo "curl to example.com failed as expected - landrun network isolation is working"
          fi
          echo "::endgroup::"

          ../tools-branch/scripts/lake-build-with-retry.sh Mathlib
          # results of build at pr-branch/.lake/build_summary_Mathlib.json
      - name: end gh-problem-match-wrap for build step
        uses: leanprover-community/gh-problem-matcher-wrap@65a654fcdf7b64ff7633bc7a558f7b46d59a27bf # 2026-06-25
        with:
          action: remove
          linters: lean

      - name: print the sizes of the oleans
        run: |
          cd pr-branch
          du .lake/build/lib/lean/Mathlib || echo "This code should be unreachable"

      # Note: we should not be including `Archive` and `Counterexamples` in the cache.
      # We do this for now for the sake of not rebuilding them in every CI run
      # even when they are not touched.
      # Since `Archive` and `Counterexamples` files have very simple dependencies,
      # it should be possible to determine whether they need to be built without actually
      # storing and transferring oleans over the network.
      # Hopefully a future re-implementation of `cache` will obviate the present need for this hack.

      - name: fetch archive and counterexamples cache
        shell: bash
        run: |
          cd pr-branch
          ../tools-branch/.lake/build/bin/cache get Archive.lean
          ../tools-branch/.lake/build/bin/cache get Counterexamples.lean

      - name: build archive
        id: archive
        continue-on-error: true
        run: |
          cd pr-branch
          ../tools-branch/scripts/lake-build-with-retry.sh Archive
          # results of build at pr-branch/.lake/build_summary_Archive.json

      - name: build counterexamples
        id: counterexamples
        continue-on-error: true
        run: |
          cd pr-branch
          ../tools-branch/scripts/lake-build-with-retry.sh Counterexamples
          # results of build at pr-branch/.lake/build_summary_Counterexamples.json

      # Runs in the build job because it only needs the freshly-built Mathlib/
      # Archive/Counterexamples oleans, which are present here; keeping it in
      # `build` also spares `test_lint` from fetching Archive/Counterexamples.
      - name: check for noisy stdout lines
        id: noisy
        run: |
          cd pr-branch
          buildMsgs="$(
            ##  we exploit `lake`s replay feature: since the cache is present, running
            ##  `lake build` will reproduce all the outputs without having to recompute
            lake build -q --iofail Mathlib Archive Counterexamples
          )"
          if [ -n "${buildMsgs}" ]
          then
            printf $'%s\n' "${buildMsgs}"
            exit 1
          fi

      - name: prepare staging directory
        if: ${{ always() && (steps.build.outcome == 'success' || steps.build.outcome == 'failure' || steps.build.outcome == 'cancelled') }}
        shell: bash
        run: |
          # Clean the staging directory first, though it should be empty at this point, to be safe
          rm -rf cache-staging
          mkdir -p cache-staging

      - name: stage Mathlib cache files
        if: ${{ always() && (steps.build.outcome == 'success' || steps.build.outcome == 'failure' || steps.build.outcome == 'cancelled') }}
        shell: landrun --rox /usr --ro /etc/timezone --rw /dev --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rox /home/lean/.cache/mathlib/ --rw /home/lean/.cache/mathlib/ --rw pr-branch/.lake/ --rw cache-staging/ --env PATH --env HOME --env GITHUB_OUTPUT --env CI -- bash -euxo pipefail {0}
        run: |
          cd pr-branch
          lake env ../tools-branch/.lake/build/bin/cache --staging-dir="../cache-staging" stage

      - name: stage Archive cache files
        if: ${{ steps.archive.outcome == 'success' }}
        shell: landrun --rox /usr --ro /etc/timezone --rw /dev --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rox /home/lean/.cache/mathlib/ --rw /home/lean/.cache/mathlib/ --rw pr-branch/.lake/ --rw cache-staging/ --env PATH --env HOME --env GITHUB_OUTPUT --env CI -- bash -euxo pipefail {0}
        run: |
          cd pr-branch
          lake env ../tools-branch/.lake/build/bin/cache --staging-dir="../cache-staging" stage Archive.lean

      - name: stage Counterexamples cache files
        if: ${{ steps.counterexamples.outcome == 'success' }}
        shell: landrun --rox /usr --ro /etc/timezone --rw /dev --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rox /home/lean/.cache/mathlib/ --rw /home/lean/.cache/mathlib/ --rw pr-branch/.lake/ --rw cache-staging/ --env PATH --env HOME --env GITHUB_OUTPUT --env CI -- bash -euxo pipefail {0}
        run: |
          cd pr-branch
          lake env ../tools-branch/.lake/build/bin/cache --staging-dir="../cache-staging" stage Counterexamples.lean

      - name: check cache staging contents
        id: cache_staging_check
        if: ${{ always() && (steps.build.outcome == 'success' || steps.build.outcome == 'failure' || steps.build.outcome == 'cancelled') }}
        shell: bash
        run: |
          if find cache-staging -type f -name '*.ltar' -print -quit | grep -q .; then
            echo "has_files=true" >> "$GITHUB_OUTPUT"
          else
            echo "has_files=false" >> "$GITHUB_OUTPUT"
          fi

      - name: upload cache staging artifact
        if: ${{ always() && steps.cache_staging_check.outputs.has_files == 'true' }}
        uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
        with:
          name: cache-staging
          path: cache-staging/
          # The `.ltar` files are already zstd-compressed; recompressing wastes CPU.
          compression-level: 0

      # Prune to this commit's `.ltar` set so the published snapshot is exactly master's
      # current cache (the local dir also holds the previous snapshot it warmed from).
      - name: prune local cache to this commit's set
        if: ${{ inputs.publish_cache && steps.build.outcome == 'success' }}
        continue-on-error: true # best-effort; never fail the build
        shell: bash # runs the trusted tools-branch `cache` binary, so no landrun needed
        run: |
          cd pr-branch
          ../tools-branch/.lake/build/bin/cache clean

      # Publish this run's pruned `.ltar` set as `cache-snapshot` for other runs to warm
      # from. Already on disk (no Azure egress) and already zstd-compressed (skip
      # recompression); retention covers how far back a PR's merge-base can be matched.
      - name: upload cache snapshot warming artifact
        if: ${{ inputs.publish_cache && steps.build.outcome == 'success' }}
        continue-on-error: true # best-effort; never fail the build
        uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
        with:
          name: cache-snapshot
          path: /home/lean/.cache/mathlib/*.ltar
          compression-level: 0
          retention-days: 14
          if-no-files-found: warn

      - name: Check if building Archive or Counterexamples failed
        if: steps.archive.outcome == 'failure' || steps.counterexamples.outcome == 'failure'
        run: |
          if [ "${{ steps.archive.outcome }}" == "failure" ]; then
            echo "❌ The \"build archive\" step above failed; please check its logs."
          fi
          if [ "${{ steps.counterexamples.outcome }}" == "failure" ]; then
            echo "❌ The \"build counterexamples\" step above failed; please check its logs."
          fi
          exit 1

      - name: Check {Mathlib, Tactic, Counterexamples, Archive}.lean
        if: ${{ always() && steps.mk_all.outcome != 'skipped' }}
        run: |
          if [[ "${{ steps.mk_all.outcome }}" != "success" ]]; then
            echo "Please run 'lake exe mk_all' to regenerate the import all files"
            exit 1
          else
            echo "'mk_all --check' passed successfully."
          fi

  test_lint:
    name: Test and lint
    needs: [build]
    # Runs `test` and `lint` on the same self-hosted pool as `build`, but as a
    # separate job so it runs in parallel with the GitHub-hosted post-build chain
    # (upload_cache -> post_steps) rather than ahead of it. `build` and `test_lint`
    # run sequentially on the pool, so peak per-run concurrency is unchanged; the
    # only cost is a second setup prefix on a fresh runner.
    #
    # It does not depend on `upload_cache`: it reconstitutes this run's oleans
    # without the paid Azure round-trip, by downloading the `cache-staging` artifact
    # `build` produces (this commit's freshly-built delta) and warming the rest from
    # the master `cache-snapshot` via the `get-cache` action. The `verify the Mathlib
    # cache is complete` step below fails loudly if that reconstitution is incomplete,
    # rather than silently rebuilding under landrun (which has no network).
    #
    # Gating: runs when `build` succeeded or failed (not cancelled/skipped). Running
    # on build FAILURE too means `lint` still reports results on a failed build,
    # best-effort over whatever oleans were built. The per-step conditions below
    # match: `test` only on a clean build, `lint` on success-or-failure.
    if: ${{ always() && (needs.build.result == 'success' || needs.build.result == 'failure') }}
    runs-on: ${{ inputs.runs_on }}
    outputs:
      lint-outcome: ${{ steps.lint.outcome }}
      test-outcome: ${{ steps.test.outcome }}
    defaults: # On Hoskinson runners, landrun is already installed.
      run: # note that pr-branch/.lake must be created in a step below before we use this
        shell: landrun --rox /usr --ro /etc/timezone --rw /dev --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rox /home/lean/.cache/mathlib/ --rw pr-branch/.lake/ --env PATH --env HOME --env GITHUB_OUTPUT --env CI -- bash -euxo pipefail {0}
    steps:
      - name: Checkout local actions
        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
        with:
          ref: ${{ github.workflow_sha }}
          fetch-depth: 1
          sparse-checkout: .github/actions
          path: workflow-actions

      # Shared self-hosted setup (see the action).
      - name: Set up build environment
        uses: ./workflow-actions/.github/actions/setup-build-env
        with:
          pr_branch_ref: ${{ inputs.pr_branch_ref }}
          tools_branch_ref: ${{ inputs.tools_branch_ref }}

      # mathlib-ci provides the scripts for the lean-pr-testing comment at the end of
      # this job, which runs only on the nightly-testing repo — so check it out only
      # there. Written twice because a `uses:` step cannot conditionally omit the
      # single `ref` key (`ref: ''` would override the action's pinned default).
      - name: Get mathlib-ci
        if: ${{ github.repository == 'leanprover-community/mathlib4-nightly-testing' && inputs.mathlib_ci_ref == '' }}
        uses: ./workflow-actions/.github/actions/get-mathlib-ci

      - name: Get mathlib-ci
        if: ${{ github.repository == 'leanprover-community/mathlib4-nightly-testing' && inputs.mathlib_ci_ref != '' }}
        uses: ./workflow-actions/.github/actions/get-mathlib-ci
        with:
          ref: ${{ inputs.mathlib_ci_ref }}

      # Pre-populate the local cache with this commit's freshly-built delta: the
      # `cache-staging` artifact `build` produces holds its newly-built `.ltar` —
      # the oleans not already in the master snapshot. `get-cache` below then warms
      # the unchanged bulk from the master `cache-snapshot` and unpacks everything,
      # so the bulk of the cache is not re-downloaded from paid Azure storage.
      # Gated on `cache-staging-has-files`: a full cache hit stages nothing (no
      # artifact is uploaded), and `get-cache` alone then covers the commit.
      - name: download cache staging artifact
        if: ${{ needs.build.outputs.cache-staging-has-files == 'true' }}
        uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
        with:
          name: cache-staging
          path: /home/lean/.cache/mathlib

      # Warm the unchanged bulk from the master `cache-snapshot` and fetch/unpack
      # this commit's oleans. The staged `.ltar` placed above are already local, so
      # `get-cache`'s `cache get` decompresses them rather than re-downloading; only
      # anything still missing is pulled from Azure.
      - name: Get cache
        uses: ./workflow-actions/.github/actions/get-cache
        with:
          working_directory: pr-branch
          cache_bin: ../tools-branch/.lake/build/bin/cache

      - name: verify the Mathlib cache is complete
        # Enforced only when the build succeeded (then the cache must be complete):
        # fail fast rather than silently trying to rebuild under landrun (which has
        # no network). On a failed build the cache is expected to be partial, so this
        # is skipped and `lint` runs best-effort below.
        if: ${{ needs.build.outputs.build-outcome == 'success' }}
        # TODO: remove if there are no issues
        continue-on-error: true
        run: |
          cd pr-branch
          lake build --no-build --rehash -v Mathlib

      # `test` runs only on a clean build: `build` itself, the `mk_all` check, and
      # the archive/counterexamples builds all succeeded. The condition reads those
      # from the build job's outputs, and the problem-matcher wrap is gated to match.
      - name: begin gh-problem-match-wrap for test step
        if: ${{ needs.build.outputs.build-outcome == 'success' && needs.build.outputs.mk_all-outcome == 'success' && needs.build.outputs.archive-outcome == 'success' && needs.build.outputs.counterexamples-outcome == 'success' }}
        uses: leanprover-community/gh-problem-matcher-wrap@65a654fcdf7b64ff7633bc7a558f7b46d59a27bf # 2026-06-25
        with:
          action: add # In order to be able to run a multiline script, we need to add/remove the problem matcher before and after.
          linters: lean
      - name: test mathlib
        if: ${{ needs.build.outputs.build-outcome == 'success' && needs.build.outputs.mk_all-outcome == 'success' && needs.build.outputs.archive-outcome == 'success' && needs.build.outputs.counterexamples-outcome == 'success' }}
        id: test
        run: |
          cd pr-branch
          ../tools-branch/scripts/lake-build-wrapper.py .lake/build_summary_MathlibTest.json lake --iofail test
      - name: end gh-problem-match-wrap for test step
        if: ${{ needs.build.outputs.build-outcome == 'success' && needs.build.outputs.mk_all-outcome == 'success' && needs.build.outputs.archive-outcome == 'success' && needs.build.outputs.counterexamples-outcome == 'success' }}
        uses: leanprover-community/gh-problem-matcher-wrap@65a654fcdf7b64ff7633bc7a558f7b46d59a27bf # 2026-06-25
        with:
          action: remove
          linters: lean

      # `lint` runs on a build that succeeded or failed (not cancelled). On a failed
      # build it lints best-effort over whatever oleans the cache has, so partial
      # lint feedback is still reported. The problem-matcher wrap is gated to match.
      - name: begin gh-problem-match-wrap for shake and lint steps
        if: ${{ always() && (needs.build.outputs.build-outcome == 'success' || needs.build.outputs.build-outcome == 'failure') }}
        uses: leanprover-community/gh-problem-matcher-wrap@65a654fcdf7b64ff7633bc7a558f7b46d59a27bf # 2026-06-25
        with:
          action: add # In order to be able to run a multiline script, we need to add/remove the problem matcher before and after.
          linters: gcc

      # With the arrival of the module system, the old `shake` is no longer functional.
      # This will be replaced soon.
      # - name: check for unused imports
      #   id: shake
      #   run: |
      #     cd pr-branch
      #     env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
      - name: lint mathlib
        if: ${{ always() && (needs.build.outputs.build-outcome == 'success' || needs.build.outputs.build-outcome == 'failure') }}
        id: lint
        timeout-minutes: 40
        run: |
          cd pr-branch
          set -o pipefail
          # If lint fails because the PR predates lake-lint configuration or the
          # old --trace argument-parsing behavior, ask the author to merge master.
          # We use .lake/ for the output file because landrun restricts /tmp access
          for attempt in 1 2; do
            if timeout 10m env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake lint -- --trace 2>&1 | tee ".lake/lint_output_attempt_${attempt}.txt"; then
              break
            fi
            status=${PIPESTATUS[0]}
            if grep -qE "cannot parse arguments|no lint driver configured" ".lake/lint_output_attempt_${attempt}.txt"; then
              echo ""
              echo "=============================================================================="
              echo "ERROR: Your branch predates the current 'lake lint' configuration."
              echo "Please merge 'master' into your PR branch and push again."
              echo ""
              echo "You can do this with:"
              echo "  git fetch upstream"
              echo "  git merge upstream/master"
              echo "  git push"
              echo "=============================================================================="
              echo ""
              exit 1
            fi
            if [ "$status" -eq 124 ]; then
              echo "runLinter timed out (attempt $attempt)."
              if [ "$attempt" -lt 2 ]; then
                echo "Retrying runLinter after timeout..."
                continue
              fi
            fi
            exit $status
          done

      - name: end gh-problem-match-wrap for shake and lint steps
        if: ${{ always() && (needs.build.outputs.build-outcome == 'success' || needs.build.outputs.build-outcome == 'failure') }}
        uses: leanprover-community/gh-problem-matcher-wrap@65a654fcdf7b64ff7633bc7a558f7b46d59a27bf # 2026-06-25
        with:
          action: remove
          linters: gcc

      # Generate a fresh token just before posting comments.
      # GitHub App tokens expire after 1 hour, and the build can take longer than that.
      - name: Generate lean-pr-testing app token
        if: ${{ always() && github.repository == 'leanprover-community/mathlib4-nightly-testing' && (startsWith(github.ref_name, 'lean-pr-testing-') || startsWith(github.ref_name, 'batteries-pr-testing-')) }}
        id: lean-pr-testing-token
        uses: actions/create-github-app-token@bcd2ba49218906704ab6c1aa796996da409d3eb1 # v3.2.0
        with:
          # `batteries-pr-testing-*` branches need a token scoped to `leanprover-community/batteries`
          # for the labelling API; `lean-pr-testing-*` branches need one scoped to `leanprover/lean4`.
          app-id: ${{ startsWith(github.ref_name, 'batteries-pr-testing-') && secrets.MATHLIB_NIGHTLY_TESTING_APP_ID || secrets.MATHLIB_LEAN_PR_TESTING_APP_ID }}
          private-key: ${{ startsWith(github.ref_name, 'batteries-pr-testing-') && secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY || secrets.MATHLIB_LEAN_PR_TESTING_PRIVATE_KEY }}
          owner: ${{ startsWith(github.ref_name, 'batteries-pr-testing-') && 'leanprover-community' || 'leanprover' }}
          repositories: ${{ startsWith(github.ref_name, 'batteries-pr-testing-') && 'batteries' || 'lean4' }}
      # The create-github-app-token README states that this token is masked and will not be logged accidentally.
      - name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
        if: ${{ always() && github.repository == 'leanprover-community/mathlib4-nightly-testing' && (startsWith(github.ref_name, 'lean-pr-testing-') || startsWith(github.ref_name, 'batteries-pr-testing-')) }}
        shell: bash
        env:
          TOKEN: ${{ steps.lean-pr-testing-token.outputs.token }}
          GITHUB_CONTEXT: ${{ toJson(github) }}
          WORKFLOW_URL: https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}
          # build/archive/counterexamples/noisy outcomes come from the `build` job's
          # outputs; test/lint are produced by this job's own steps.
          BUILD_OUTCOME: ${{ needs.build.outputs.build-outcome }}
          NOISY_OUTCOME: ${{ needs.build.outputs.noisy-outcome }}
          ARCHIVE_OUTCOME: ${{ needs.build.outputs.archive-outcome }}
          COUNTEREXAMPLES_OUTCOME: ${{ needs.build.outputs.counterexamples-outcome }}
          LINT_OUTCOME: ${{ steps.lint.outcome }}
          TEST_OUTCOME: ${{ steps.test.outcome }}
          NIGHTLY_TESTING_REPO: leanprover-community/mathlib4-nightly-testing
        run: |
          "${CI_SCRIPTS_DIR}/maintainer/lean-pr-testing-comments.sh" lean
          "${CI_SCRIPTS_DIR}/maintainer/lean-pr-testing-comments.sh" batteries

  upload_cache:
    name: Upload to cache
    needs: [build]
    runs-on: ubuntu-latest # These steps run on a GitHub runner; no landrun sandboxing is needed.
    # Pins the OIDC `sub` claim to `...:environment:<cache_environment>`, which the Azure cache
    # app's federated credential is scoped to. A token minted by any job without this environment
    # (e.g. the untrusted build/post_steps/style_lint jobs) cannot satisfy that trust.
    environment:
      name: ${{ inputs.cache_environment }}
      # Skip creating a GitHub deployment record/UI; we use the environment only to
      # pin the OIDC `sub` claim and gate access to its federated credential.
      deployment: false
    permissions:
      contents: read
      id-token: write
    # We only upload the cache if the build started (whether succeeding, failing, or cancelled)
    # but not if any earlier step failed or was cancelled.
    # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Some.20files.20not.20found.20in.20the.20cache/near/407183836
    if: ${{ always() && needs.build.outputs.cache-staging-has-files == 'true' }}
    steps:
      # Build the write-side cache tool (and load the trust-dispatch action below)
      # from the branch under test, so a PR's `--container`-aware tool is what
      # writes the cache. This job only runs in trusted in-repo contexts (bors,
      # dev branches, the nightly-testing repo) — fork PRs run master's
      # `build_template` via `pull_request_target`, never this one — so
      # `pr_branch_ref` is always a trusted ref here. Fork PRs keep `master`.
      - name: Checkout tools branch
        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
        with:
          ref: ${{ inputs.tools_branch_ref != '' && inputs.tools_branch_ref || (github.event.pull_request.head.repo.fork && 'master' || inputs.pr_branch_ref) }}
          fetch-depth: 1

      # Same trust dispatch as in the `build` and `post_steps` jobs. Loaded from
      # the tools-branch checkout above (the branch under test, a trusted in-repo
      # ref in the contexts where this job runs), which is what the OIDC token's
      # container scoping is keyed to.
      - name: Compute cache trust dispatch
        uses: ./.github/actions/cache-trust-dispatch
        with:
          repo: ${{ github.event.pull_request.head.repo.full_name || github.repository }}
          branch: ${{ github.head_ref || github.ref_name }}
          head-sha: ${{ github.event.pull_request.head.sha || github.sha }}

      - name: Configure Lean
        uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0
        with:
          auto-config: false # Don't run `lake build`, `lake test`, or `lake lint` automatically.
          use-github-cache: false
          use-mathlib-cache: false # This can be re-enabled once we are confident in the cache again.
          reinstall-transient-toolchain: true

      - name: build cache executable
        run: |
          lake build cache
          CACHE_BIN="$(pwd)/.lake/build/bin/cache"
          if [ ! -x "$CACHE_BIN" ]; then
            echo "cache binary not found: $CACHE_BIN"
            exit 1
          fi
          echo "CACHE_BIN=$CACHE_BIN" >> "$GITHUB_ENV"

      - name: Download cache staging artifact
        uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c # v8.0.1
        with:
          name: cache-staging
          path: cache-staging

      - name: Azure CLI OIDC login and mint storage bearer token
        uses: leanprover-community/mathlib-ci/.github/actions/azure-create-cache-token@17db5ff55a65df98d55cbddcc67938f70d10dab2
        with:
          azure-client-id: ${{ inputs.cache_application_id }}
          azure-tenant-id: ${{ secrets.LPC_AZ_TENANT_ID }}

      - name: Upload staged cache to Azure
        shell: bash
        env:
          REPO: ${{ github.event.pull_request.head.repo.full_name || github.repository }}
        run: |
          # $MATHLIB_CACHE_PRIMARY is set by the `Compute cache trust dispatch`
          # step above, from the shared composite action that owns the (repo,
          # branch) → container mapping for both this job and the read-side
          # jobs (build, post_steps). Each job writes only into its own trust-level
          # container.
          echo "Uploading cache to Azure (container: $MATHLIB_CACHE_PRIMARY)..."
          lake env "$CACHE_BIN" put-staged --container="$MATHLIB_CACHE_PRIMARY" --staging-dir="cache-staging" --repo="$REPO"

  post_steps:
    name: Post-Build Step
    needs: [build, upload_cache]
    if: ${{ always() && needs.build.result == 'success' && (needs.upload_cache.result == 'success' || needs.upload_cache.result == 'skipped') }}
    runs-on: ubuntu-latest # Note these steps run on disposable GitHub runners, so no landrun sandboxing is needed.
    # This job checks out and executes (potentially fork) PR code unsandboxed,
    # so it must not inherit any write-capable token.
    permissions:
      contents: read
    steps:

      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
        with:
          ref: ${{ inputs.pr_branch_ref }}
          # Untrusted (potentially fork) checkout: don't persist the GITHUB_TOKEN into its .git/config.
          persist-credentials: false
          # This job runs with only `contents: read` and no persisted credentials,
          # so checking out fork PR code under pull_request_target is safe.
          allow-unsafe-pr-checkout: true

      # Sparse-checkout master's `.github/actions/` so the trust dispatch
      # below loads from a trust-rooted source, not from PR-branch-controlled
      # content. Mirrors the `Checkout local actions` step in the `build` job.
      - name: Checkout local actions
        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
        with:
          ref: ${{ github.workflow_sha }}
          fetch-depth: 1
          sparse-checkout: .github/actions
          path: workflow-actions

      # Sets MATHLIB_CACHE_FROM in env so the `cache get` calls below pick
      # up the trust-class-appropriate read fallback automatically. Replaces
      # the previous test-only `--cache-from=master,forks` hardcode that
      # lived in this file — that policy is now in the shared composite
      # action so build, upload_cache, and post_steps all consult the same
      # source of truth.
      - name: Compute cache trust dispatch
        uses: ./workflow-actions/.github/actions/cache-trust-dispatch
        with:
          repo: ${{ github.event.pull_request.head.repo.full_name || github.repository }}
          branch: ${{ github.head_ref || github.ref_name }}
          head-sha: ${{ github.event.pull_request.head.sha || github.sha }}

      - name: Configure Lean
        uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0
        with:
          auto-config: false # Don't run `lake build`, `lake test`, or `lake lint` automatically.
          use-github-cache: false
          use-mathlib-cache: false # This can be re-enabled once we are confident in the cache again.
          reinstall-transient-toolchain: true

      - name: get cache for Mathlib
        run: |
          # Run once without --repo, so we can diagnose what `lake exe cache get` wants to do by itself.
          lake exe cache get
          # Run again with --repo, so ensure we actually get the oleans.
          lake exe cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} get

      - name: get cache for Archive and Counterexamples
        run: |
          # Run once without --repo, so we can diagnose what `lake exe cache get` wants to do by itself.
          lake exe cache get Archive Counterexamples
          # Run again with --repo, so ensure we actually get the oleans.
          lake exe cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} get Archive Counterexamples

      - name: verify that everything was available in the cache
        run: |
          echo "::group::{verify Mathlib cache}"
          lake build --no-build --rehash -v Mathlib
          echo "::endgroup::"
          echo "::group::{verify Archive cache}"
          lake build --no-build --rehash -v Archive
          echo "::endgroup::"
          echo "::group::{verify Counterexamples cache}"
          lake build --no-build --rehash -v Counterexamples
          echo "::endgroup::"

      - name: check declarations in db files
        run: |
          python3 scripts/yaml_check.py docs/100.yaml docs/1000.yaml docs/overview.yaml docs/undergrad.yaml
          lake exe check-yaml

      - name: generate our import graph
        run: |
          lake exe graph

      - name: Checkout local actions
        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
        with:
          ref: ${{ github.workflow_sha }}
          fetch-depth: 1
          sparse-checkout: .github/actions
          path: workflow-actions

      - name: Get mathlib-ci
        uses: ./workflow-actions/.github/actions/get-mathlib-ci

      - name: dump declarations and transitive-import counts
        run: |
          lake env lean --run "${CI_SCRIPTS_DIR}/pr_summary/dumpReasonableDecls.lean" \
            --out decls.txt --imports-out imports.json Mathlib
          ## Record the PR number so the post-build `decls-diff` workflow can find
          ## the comment to patch without the (laggy) commit-SHA search API. Empty
          ## for non-PR builds (push to master / bors); the consumer then falls
          ## back to the commit's associated PRs.
          printf '%s' "${{ github.event.pull_request.number }}" > pr_number.txt

      - name: ensure dump outputs are regular files
        run: |
          for f in decls.txt imports.json import_graph.dot pr_number.txt; do
            if [ -L "$f" ] || [ ! -f "$f" ]; then
              echo "Refusing to upload: $f is not a regular file." >&2
              ls -la -- "$f" >&2 || true
              exit 1
            fi
          done

      - name: upload the import graph
        uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
        with:
          name: import-graph
          path: |
            import_graph.dot
            decls.txt
            imports.json
            pr_number.txt
          ## Master pushes: 90 days, so later PRs forked from these commits
          ## can consume the dumps from the artifact. Other branches: 7 days.
          retention-days: ${{ github.ref == 'refs/heads/master' && '90' || '7' }}

      - name: clean up the import graph file
        run: rm -f import_graph.dot decls.txt imports.json pr_number.txt

      - name: check all scripts build successfully
        run: |
          lake env lean scripts/create_deprecated_modules.lean
          lake env lean scripts/autolabel.lean
          # Executing this also runs the export and writes a (gitignored) `crossrefs.json`,
          # which doubles as a smoke test of the `export_crossrefs.yml` workflow.
          lake env lean scripts/export_crossrefs.lean
          lake exe check_title_labels --labels "t-algebra" "feat: dummy PR for testing"

      - name: build everything
        # make sure everything is available for test/import_all.lean
        # and that miscellaneous executables still work
        run: |
          lake build Batteries Qq Aesop ProofWidgets Plausible

      - name: build AesopTest (nightly-testing only)
        # Only run on the mathlib4-nightly-testing repository
        if: github.repository == 'leanprover-community/mathlib4-nightly-testing'
        run: |
          lake build AesopTest

      # We no longer run `lean4checker` in regular CI, as it is quite expensive for little benefit.
      # Instead we run it in a cron job on master: see `daily.yml`.

  style_lint:
    name: Lint style
    runs-on: ubuntu-latest
    # This job lints (potentially fork) PR code, so it must not inherit any write-capable token.
    # In `check` mode lint-style-action only reads and validates code locally (no API calls).
    permissions:
      contents: read
    steps:
      - uses: leanprover-community/lint-style-action@a7e7428fa44f9635d6eb8e01919d16fd498d387a # 2025-08-18
        with:
          mode: check
          lint-bib-file: true
          ref: ${{ inputs.pr_branch_ref }}

  final:
    name: Post-CI job
    # ensure that this runs iff direct dependencies succeeded even if transitive dependencies  were skipped
    if: ${{ always() && inputs.run_post_ci && needs.style_lint.result == 'success' && needs.build.result == 'success' && needs.test_lint.result == 'success' && needs.post_steps.result == 'success' }}
    needs: [style_lint, build, test_lint, post_steps]
    runs-on: ubuntu-latest
    steps:
      - id: PR
        uses: 8BitJonny/gh-get-current-pr@4056877062a1f3b624d5d4c2bedefa9cf51435c9 # 4.0.0
        # TODO: this may not work properly if the same commit is pushed to multiple branches:
        # https://github.com/8BitJonny/gh-get-current-pr/issues/8
        with:
          github-token: ${{ secrets.GITHUB_TOKEN }}
          # Only return if PR is still open
          filterOutClosed: true

      - id: remove_labels
        name: Remove "awaiting-CI"
        # we use curl rather than octokit/request-action so that the job won't fail
        # (and send an annoying email) if the labels don't exist
        run: |
          curl --request DELETE \
            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ steps.PR.outputs.number }}/labels/awaiting-CI \
            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'

      - if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
        name: Generate auto merge app token
        id: auto-merge-app-token
        uses: leanprover-community/mathlib-ci/.github/actions/azure-create-github-app-token@3bb576208589a435eeaeac9b144a1b7c3e948760
        with:
          app-id: ${{ secrets.MATHLIB_AUTO_MERGE_APP_ID }}
          key-vault-name: ${{ vars.MATHLIB_AZ_KEY_VAULT_NAME }}
          key-name: mathlib-auto-merge-app-pk
          azure-client-id: ${{ vars.GH_APP_AZURE_CLIENT_ID_CI_AUTO_MERGE }}
          azure-tenant-id: ${{ secrets.LPC_AZ_TENANT_ID }}

      - if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
        name: Get PR label timeline data
        # 'auto-merge-after-CI' must be within the last 100 labels added (could be increased to 250 if needed)
        # query from https://stackoverflow.com/a/67939355
        # unfortunately we cannot query only for 'auto-merge-after-CI' events
        # so we have to process this with jq in the next step
        id: get-timeline
        uses: octokit/graphql-action@ddde8ebb2493e79f390e6449c725c21663a67505 # v3.0.2
        with:
          query: |
            query($owner: String!, $name: String!, $number: Int!) {
              repository(owner: $owner, name: $name) {
                pullRequest(number: $number) {
                  timelineItems(itemTypes: LABELED_EVENT, last: 100) {
                    nodes {
                      ... on LabeledEvent {
                        createdAt
                        actor { login __typename }
                        label { name }
                      }
                    }
                  }
                }
              }
            }
          owner: leanprover-community
          name: mathlib4
          number: ${{ steps.PR.outputs.number }}
        env:
          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

      - if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
        name: Extract label actor username
        id: get-label-actor
        run: |
          # Parse the GraphQL response and filter for the specific label
          echo '${{ steps.get-timeline.outputs.data }}'
          ACTOR=$(echo '${{ steps.get-timeline.outputs.data }}' | jq -c '
            .repository.pullRequest.timelineItems.nodes
            | map(select(.label.name == "auto-merge-after-CI"))
            | sort_by(.createdAt)
            | last
            | .actor // empty
          ')
          USERNAME=$(echo "$ACTOR" | jq -r '.login // empty')
          # 'Bot' for GitHub App actors (whose GraphQL logins lack the '[bot]' suffix),
          # 'User' for regular accounts
          ACTOR_TYPE=$(echo "$ACTOR" | jq -r '.__typename // empty')

          # Validate username format (GitHub usernames are alphanumeric + hyphens, max 39 chars)
          printf 'USERNAME: %s\nACTOR_TYPE: %s\n' "$USERNAME" "$ACTOR_TYPE"
          if [[ -z "$USERNAME" ]]; then
            echo "Error: No actor found for the specified label"
            exit 1
          elif ! [[ "$USERNAME" =~ ^[a-zA-Z0-9-]{1,39}$ ]]; then
            echo "Error: Invalid username format: $USERNAME"
            exit 1
          fi

          echo "username=$USERNAME" >> "$GITHUB_OUTPUT"
          echo "actor_type=$ACTOR_TYPE" >> "$GITHUB_OUTPUT"
          echo "Found label actor: $USERNAME ($ACTOR_TYPE)"

      # bot usernames will cause this step to error with "Could not resolve to a User...",
      # so we skip it for all non-user actors; allowed bots are validated in the next step
      - if: >-
          contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI') &&
          steps.get-label-actor.outputs.actor_type == 'User'
        name: check team membership
        uses: tspascoal/get-user-teams-membership@b2546c5affc730fd8e3d8483ae9ad3621938c2f9 # v4.0.2
        id: actorTeams
        with:
          organization: leanprover-community # optional. Default value ${{ github.repository_owner }}
                  # Organization to get membership from.
          username: ${{ steps.get-label-actor.outputs.username }}
          GITHUB_TOKEN: ${{ secrets.MATHLIB_REVIEWERS_TEAM_KEY }} # (Requires scope: `read:org`)

      - if: >-
          contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI') &&
          (
            (
              steps.get-label-actor.outputs.actor_type == 'Bot' &&
              (
                steps.get-label-actor.outputs.username == 'mathlib-nolints' ||
                steps.get-label-actor.outputs.username == 'mathlib-update-dependencies' ||
                steps.get-label-actor.outputs.username == 'mathlib-splicebot'
              )
            ) ||
            contains(steps.actorTeams.outputs.teams, 'mathlib-maintainers') ||
            contains(steps.actorTeams.outputs.teams, 'lean-release-managers') ||
            contains(steps.actorTeams.outputs.teams, 'bot-users')
          )
        name: If `auto-merge-after-CI` is present, add a `bors merge` comment.
        uses: GrantBirki/comment@3439715f0cf3b8fc29bf47be0e3226679c06c41a # v3.0.0
        with:
          # This token is masked by the token minting action and will not be logged accidentally.
          token: ${{ steps.auto-merge-app-token.outputs.token }}
          issue-number: ${{ steps.PR.outputs.number }}
          body: |
            As this PR is labelled `auto-merge-after-CI`, we are now sending it to bors:

            bors merge