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

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 }}
      get-cache-outcome: ${{ steps.get.outcome }}
      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

      # Checkout a trusted branch to build the tooling from
      - name: Checkout tools branch
        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
        with:
          # Recall that on the `leanprover-community/mathlib4-nightly-testing` repository,
          # we don't maintain a `master` branch at all.
          # For PRs and pushes to this repository, we will use `nightly-testing-green` instead,
          # so that even when `nightly-testing` is broken, we can still build tools from a known good state.
          ref: ${{ inputs.tools_branch_ref != '' && inputs.tools_branch_ref || (github.repository == 'leanprover-community/mathlib4-nightly-testing' && 'nightly-testing-green' || 'master') }}
          path: tools-branch

      - name: Checkout local actions
        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
        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 }}

      # Checkout the PR branch into a subdirectory
      - name: Checkout PR branch
        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
        with:
          ref: ${{ inputs.pr_branch_ref }}
          fetch-depth: 2 # we may fetch cache from the commit before this one (or earlier)
          path: pr-branch

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

      - name: build tools-branch tools
        shell: bash # We're only building a trusted branch with the tools, so no need to run inside landrun.
        run: |
          cd tools-branch
          lake build cache check-yaml graph
          ls .lake/build/bin/cache
          ls .lake/build/bin/check-yaml
          ls .lake/packages/importGraph/.lake/build/bin/graph

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

      - name: get cache (1/3 - setup and initial fetch)
        id: get_cache_part1_setup
        shell: bash # only runs `cache get` from `tools-branch`, so doesn't need to be inside landrun
        run: |
          cd pr-branch
          echo "Removing old Mathlib build directories prior to cache fetch..."
          rm -rf .lake/build/lib/lean/Mathlib

          # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
          echo "Attempting to fetch olean for Mathlib/Init.lean from cache..."
          ../tools-branch/.lake/build/bin/cache get Mathlib/Init.lean

      - name: get cache (2/3 - test Mathlib.Init cache)
        id: get_cache_part2_test
        continue-on-error: true # Allow workflow to proceed to Part 3 to check outcome
        # This step uses the job's default shell, which is landrun-wrapped bash
        run: |
          cd pr-branch

          echo "Attempting: lake build --no-build -v Mathlib.Init (this runs under landrun)"
          lake build --no-build -v Mathlib.Init

      - name: get cache (3/3 - finalize cache operation)
        id: get
        shell: bash # only runs git and `cache get` from `tools-branch`, so doesn't need to be inside landrun
        env:
          BEFORE_SHA: ${{ github.event.before || '' }}
          BASE_SHA: ${{ github.event.pull_request.base.sha || '' }}
          CACHE_REPO: ${{ github.event.pull_request.head.repo.full_name || github.repository }}
        run: |
          cd pr-branch
          if [[ "${{ steps.get_cache_part2_test.outcome }}" != "success" ]]; then
            echo "WARNING: 'lake build --no-build -v Mathlib.Init' failed."
            echo "No cache for 'Mathlib.Init' available or it could not be prepared."
            exit 0
          fi

          ORIG_SHA="$(git rev-parse HEAD)"
          PREV_SHA=""
          PREV_SHA_SOURCE=""

          # When a ref is newly created, github.event.before can be all-zero.
          if [[ "$BEFORE_SHA" =~ ^0{40}$ ]]; then
            BEFORE_SHA=""
          fi

          if [[ -n "$BEFORE_SHA" ]]; then
            PREV_SHA="$BEFORE_SHA"
            PREV_SHA_SOURCE="github.event.before"
          elif [[ -n "$BASE_SHA" ]]; then
            PREV_SHA="$BASE_SHA"
            PREV_SHA_SOURCE="pull_request.base.sha"
          else
            PREV_SHA="$(git rev-parse --verify --quiet HEAD^ || true)"
            if [[ -n "$PREV_SHA" ]]; then
              PREV_SHA_SOURCE="HEAD^"
            fi
          fi

          if [[ -n "$PREV_SHA" ]]; then
            # cf. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Mathlib.20has.20moved.20to.20the.20new.20module.20system/near/563452000
            echo "Warming up cache using previous commit: $PREV_SHA (source: $PREV_SHA_SOURCE)"
            if git cat-file -e "$PREV_SHA^{commit}" 2>/dev/null || git fetch --no-tags --depth=1 origin "$PREV_SHA"; then
              git checkout "$PREV_SHA"
              ../tools-branch/.lake/build/bin/cache get
              # Run again with --repo, to ensure we actually get the oleans.
              ../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" get

              echo "Switching back to branch head"
              git checkout "$ORIG_SHA"
            else
              echo "Could not fetch $PREV_SHA; skipping parent warmup cache fetch."
            fi
          else
            echo "No previous commit candidate found; skipping parent warmup cache fetch."
          fi

          echo "Fetching all remaining cache..."

          ../tools-branch/.lake/build/bin/cache get

          # Run again with --repo, to ensure we actually get the oleans.
          ../tools-branch/.lake/build/bin/cache --repo="$CACHE_REPO" get

      - 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@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7.0.0
        with:
          name: cache-staging
          path: cache-staging/

      - 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
          # Try running with --trace; if it fails due to argument parsing, the PR needs 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 exe runLinter --trace Mathlib 2>&1 | tee ".lake/lint_output_attempt_${attempt}.txt"; then
              break
            fi
            status=${PIPESTATUS[0]}
            if grep -q "cannot parse arguments" ".lake/lint_output_attempt_${attempt}.txt"; then
              echo ""
              echo "=============================================================================="
              echo "ERROR: Your branch uses an older version of runLinter that doesn't support"
              echo "the --trace flag. Please merge 'master' into your PR branch to get the"
              echo "updated linter, then 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@f8d387b68d61c58ab83c6c016672934102569859 # v3.0.0
        with:
          app-id: ${{ secrets.MATHLIB_LEAN_PR_TESTING_APP_ID }}
          private-key: ${{ secrets.MATHLIB_LEAN_PR_TESTING_PRIVATE_KEY }}
          owner: leanprover
          repositories: 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.
    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:
      - name: Checkout tools branch
        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
        with:
          ref: ${{ inputs.tools_branch_ref != '' && inputs.tools_branch_ref || (github.repository == 'leanprover-community/mathlib4-nightly-testing' && 'nightly-testing-green' || 'master') }}
          fetch-depth: 1

      - name: Configure Lean
        uses: leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4.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
        id: mint_cache_bearer
        continue-on-error: true
        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: Fallback to SAS token if bearer mint fails (for ease of migration)
        if: ${{ steps.mint_cache_bearer.outcome != 'success' }}
        shell: bash
        env:
          MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }}
        run: |
          if [ -z "$MATHLIB_CACHE_SAS_RAW" ]; then
            echo "Azure bearer mint failed and secrets.MATHLIB_CACHE_SAS is not set"
            exit 1
          fi

          MATHLIB_CACHE_SAS="${MATHLIB_CACHE_SAS_RAW%"${MATHLIB_CACHE_SAS_RAW##*[![:space:]]}"}"
          if [ -z "$MATHLIB_CACHE_SAS" ]; then
            echo "Azure bearer mint failed and secrets.MATHLIB_CACHE_SAS is empty after trimming"
            exit 1
          fi

          echo "::add-mask::$MATHLIB_CACHE_SAS"
          echo "MATHLIB_CACHE_AZURE_BEARER_TOKEN=" >> "$GITHUB_ENV"
          echo "MATHLIB_CACHE_SAS=$MATHLIB_CACHE_SAS" >> "$GITHUB_ENV"
          echo "Using SAS fallback because bearer mint step failed."

      - name: Upload staged cache to Azure
        shell: bash
        run: |
          echo "Uploading cache to Azure..."
          MATHLIB_CACHE_USE_CLOUDFLARE=0 lake env "$CACHE_BIN" put-staged --staging-dir="cache-staging" --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }}

  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.
    steps:

      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
        with:
          ref: ${{ inputs.pr_branch_ref }}

      - name: Configure Lean
        uses: leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4.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: upload the import graph
        uses: actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f # v7.0.0
        with:
          name: import-graph
          path: import_graph.dot
          ## the default is 90, but we build often, so unless there's a reason
          ## to care about old copies in the future, just say 7 days for now
          retention-days: 7

      - name: clean up the import graph file
        run: rm import_graph.dot

      - 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
    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 }
                        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 }}'
          USERNAME=$(echo '${{ steps.get-timeline.outputs.data }}' | jq -r '
            .repository.pullRequest.timelineItems.nodes
            | map(select(.label.name == "auto-merge-after-CI"))
            | sort_by(.createdAt)
            | last
            | .actor.login // empty
          ')

          # Validate username format (GitHub usernames are alphanumeric + hyphens, max 39 chars)
          printf 'USERNAME: %s\n' "$USERNAME"
          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 "Found label actor: $USERNAME"

      - if: >- # bot usernames will cause this step to error with "Could not resolve to a User..."
          contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI') &&
          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'
        name: check team membership
        uses: tspascoal/get-user-teams-membership@57e9f42acd78f4d0f496b3be4368fc5f62696662 # v3.0.0
        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.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@608e41b19bc973020ec0e189ebfdae935d7fe0cc # v2.1.1
        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