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 }}
      lint-outcome: ${{ steps.lint.outcome }}
      mk_all-outcome: ${{ steps.mk_all.outcome }}
      noisy-outcome: ${{ steps.noisy.outcome }}
      # shake-outcome: ${{ steps.shake.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: 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: cleanup
        shell: bash    # This *just* deletes old files, so is safe to run outside landrun.
        run: |
          if ! find . -mindepth 1 -exec rm -rf -- {} +; then
            echo "ERROR: Initial cleanup failed, waiting 5 seconds and retrying..."
            sleep 5
            find . -mindepth 1 -exec rm -rf -- {} +
          fi
          # Delete all but the 5 most recent toolchains.
          # Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file.
          # Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`.
          if cd ~/.elan/toolchains && find . -maxdepth 1 -type d ! -name . -print0 | xargs -0 ls -1td | grep -v 'nightly$' | grep -v 'stable$' | tail -n +6 | xargs -I {} sh -c 'echo {} && rm -rf "{}" && rm "../update-hashes/{}"'; then
              : # Do nothing on success
          else
              : # Do nothing on failure, but suppress errors
          fi

      # The Hoskinson runners may not have jq installed, so do that now.
      - name: 'Setup jq'
        uses: dcarbone/install-jq-action@b7ef57d46ece78760b4019dbc4080a1ba2a40b45 # v3.2.0

      - name: Checkout local actions
        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
        with:
          ref: ${{ github.workflow_sha }}
          fetch-depth: 1
          sparse-checkout: .github/actions
          path: workflow-actions

      # We need to 'duplicate' this step below because GitHub Actions does not let a `uses:` step
      # conditionally omit a single `with:` key, and passing `ref: ''` would override
      # the composite action's default to the empty string instead of falling back to it
      # Note only one of the two below will actually run in any given run
      - name: Get mathlib-ci
        if: ${{ inputs.mathlib_ci_ref == '' }}
        uses: ./workflow-actions/.github/actions/get-mathlib-ci

      - name: Get mathlib-ci
        if: ${{ inputs.mathlib_ci_ref != '' }}
        uses: ./workflow-actions/.github/actions/get-mathlib-ci
        with:
          ref: ${{ inputs.mathlib_ci_ref }}

      # Compute the trust-classified container target and read fallback
      # for this job. Sets MATHLIB_CACHE_FROM / MATHLIB_CACHE_PRIMARY in
      # env so every subsequent `cache get` in this job inherits them
      # without per-call flag plumbing. Loaded from master via the sparse
      # `workflow-actions/` checkout above, not from the PR branch — this
      # keeps the trust policy out of fork-controllable file paths.
      - 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 }}

      # Checkout the PR branch into a subdirectory
      - name: Checkout PR branch
        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
        with:
          ref: ${{ inputs.pr_branch_ref }}
          fetch-depth: 2 # we may fetch cache from the commit before this one (or earlier)
          path: pr-branch
          # This is an untrusted (potentially fork) checkout whose code we build.
          # Don't leave the GITHUB_TOKEN in pr-branch/.git/config, where that code could read it.
          persist-credentials: false

      # 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."

      # Create empty directories so landrun doesn't complain
      - name: Create empty directories
        shell: bash # We need to run this outside landrun, as it is a prerequisite for landrun!
        run: |
          mkdir -p pr-branch/.lake/
          mkdir -p .cache/mathlib/
          mkdir -p _work

      # NOTE: if you copy this, consider using `leanprover/lean-action` instead.
      # We install manually, to avoid running lean outside landrun.
      - name: install elan
        shell: bash
        run: |
          set -o pipefail
          curl -o elan-init.sh -sSfL https://elan.lean-lang.org/elan-init.sh
          chmod +x elan-init.sh
          ./elan-init.sh -y --default-toolchain none
          echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"

      - name: set toolchain directory
        shell: bash
        run: |
          cd pr-branch
          # Get the lake binary path from elan and extract toolchain directory
          LAKE_PATH=$(elan which lake)
          echo "Lake path: $LAKE_PATH"

          # Extract the toolchain directory by removing /bin/lake from the end
          TOOLCHAIN_DIR=$(dirname "$LAKE_PATH")
          TOOLCHAIN_DIR=$(dirname "$TOOLCHAIN_DIR")
          echo "Toolchain directory: $TOOLCHAIN_DIR"

          # Set it as an environment variable for subsequent steps
          echo "TOOLCHAIN_DIR=$TOOLCHAIN_DIR" >> "$GITHUB_ENV"

      - name: set LEAN_SRC_PATH
        shell: bash
        run: |
          cd pr-branch

          # Start with the base paths
          LEAN_SRC_PATH=".:$TOOLCHAIN_DIR/src/lean/lake"

          # Extract package names from lake-manifest.json and validate them
          # Only allow A-Z, a-z, 0-9, _, and - characters
          # Build the LEAN_SRC_PATH by appending each validated package
          PACKAGE_NAMES=$(jq -r '.packages[].name' lake-manifest.json)
          for pkg in $PACKAGE_NAMES; do
            if [[ "$pkg" =~ ^[A-Za-z0-9_-]+$ ]]; then
              LEAN_SRC_PATH="$LEAN_SRC_PATH:.lake/packages/$pkg"
            else
              echo "Warning: Skipping invalid package name: $pkg"
            fi
          done

          echo "LEAN_SRC_PATH=$LEAN_SRC_PATH"

          # Set it as an environment variable for subsequent steps
          echo "LEAN_SRC_PATH=$LEAN_SRC_PATH" >> "$GITHUB_ENV"

      # Populate `tools-branch/` with the trusted CI tooling (the `cache` binary and
      # the `lake-build-*` helper scripts invoked by path below).
      #
      #   - Fast path: download the prebuilt `tools-bin` artifact published from
      #     `master` by `publish_tools.yml` — only on canonical mathlib4, and only
      #     when the branch under test doesn't change the cache tool. `get-tools`
      #     makes that comparison itself against `source_dir` (the already-checked-
      #     out `pr-branch`), so the tool-source path list lives in the action, not
      #     duplicated here.
      #   - Source build: from `tools_source_ref`, pointed at the branch *under
      #     test* (`pr_branch_ref`) — bors `staging`/`trying`, in-repo dev branches,
      #     and the nightly-testing repo (which has no `master` branch) — so the
      #     built tool matches the tree. Fork PRs keep `master` and skip the
      #     comparison (empty `source_dir`): they run master's `build_template` via
      #     `pull_request_target`, never this one, and their untrusted tool must
      #     never be built/run with cache credentials (bors exercises tool changes
      #     in-repo instead).
      - name: Get CI tools
        uses: ./workflow-actions/.github/actions/get-tools
        with:
          use_artifact: ${{ inputs.tools_branch_ref == '' && github.repository == 'leanprover-community/mathlib4' }}
          tools_source_ref: ${{ inputs.tools_branch_ref != '' && inputs.tools_branch_ref || (github.event.pull_request.head.repo.fork && 'master' || inputs.pr_branch_ref) }}
          source_dir: ${{ github.event.pull_request.head.repo.fork != true && 'pr-branch' || '' }}
          github_token: ${{ github.token }}

      - name: download dependencies
        # We need network access to download dependencies
        # We run this inside landrun, but restrict disk access.
        # Landrun argument notes:
        # - we give --rox access to `~/.elan` and `~/actions-runner/_work` (GitHub CI needs this)
        # - we give --unrestricted-network as we need this to download dependencies
        # - git needs read only access to `/etc`.
        shell: landrun --unrestricted-network --rox /etc --rox /usr --rw /dev --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rw pr-branch/.lake/ --env PATH --env HOME --env GITHUB_OUTPUT --env CI -- bash -euxo pipefail {0}
        run: |
          cd pr-branch
          lake env

      - 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@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
        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@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
        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

      - 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/

      # 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

      - name: begin gh-problem-match-wrap for test step
        uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
        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
        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
        uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
        with:
          action: remove
          linters: lean

      - name: begin gh-problem-match-wrap for shake and lint steps
        uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
        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() && steps.build.outcome == 'success' || steps.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
        uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
        with:
          action: remove
          linters: gcc

      - 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 Mathlib Archive Counterexamples |
            ##  we filter out the output lines that begin with `✔ [xx/yy]`, where xx, yy
            ##  are either numbers or ?, and the "Build completed successfully." message.
            ##  We keep the rest, which are actual outputs of the files
            awk '!($0 ~ "^\\s*✔ \\[[?0-9]*/[?0-9]*\\]" || $0 ~ "^Build completed successfully( \\([0-9]+ jobs\\))?\\.?$"){ print $0 }')"
          if [ -n "${buildMsgs}" ]
          then
            printf $'%s\n' "${buildMsgs}"
            exit 1
          fi

      # 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_OUTCOME: ${{ steps.build.outcome }}
          NOISY_OUTCOME: ${{ steps.noisy.outcome }}
          ARCHIVE_OUTCOME: ${{ steps.archive.outcome }}
          COUNTEREXAMPLES_OUTCOME: ${{ steps.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@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
        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@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
        with:
          ref: ${{ inputs.pr_branch_ref }}
          # Untrusted (potentially fork) checkout: don't persist the GITHUB_TOKEN into its .git/config.
          persist-credentials: false

      # 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@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
        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@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
        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
          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.post_steps.result == 'success' }}
    needs: [style_lint, build, 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