bors.yml

# DO NOT EDIT THIS FILE!!!

# This file is automatically generated by mk_build_yml.sh
# Edit .github/build.in.yml instead and run
# .github/workflows/mk_build_yml.sh to update.

# Forks of mathlib and other projects should be able to use build_fork.yml directly
# The jobs in this file run on self-hosted workers and will not be run from external forks

on:
  push:
    branches:
      - staging

name: continuous integration (staging)

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
  # Direct Lake to store its artifact cache in `.lake`.
  # Prevents Lake from using a directory it may not have permissions to under landrun.
  LAKE_CACHE_DIR: .lake/cache

concurrency:
  # label each workflow run; only the latest with each label will run
  # workflows on master get more expressive labels
  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}-${{ (github.event_name == 'push' && contains(fromJSON('["refs/heads/master", "refs/heads/staging"]'), github.ref) && github.run_id) || '' }}
  # cancel any running workflow with the same label
  cancel-in-progress: true

# Limit permissions for GITHUB_TOKEN for the entire workflow
permissions:
  contents: read
  pull-requests: write  # Only allow PR comments/labels
  # All other permissions are implicitly 'none'

jobs:
  build:
    if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'
    name: Build
    runs-on: bors
    outputs:
      build-outcome: ${{ steps.build.outcome }}
      archive-outcome: ${{ steps.archive.outcome }}
      counterexamples-outcome: ${{ steps.counterexamples.outcome }}
      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: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}-${{ (github.event_name == 'push' && contains(fromJSON('["refs/heads/master", "refs/heads/staging"]'), github.ref) && github.run_id) || '' }}
        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 the master branch into a subdirectory
      - name: Checkout master branch
        uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
        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` instead.
          ref: ${{ github.repository == 'leanprover-community/mathlib4-nightly-testing' && 'nightly-testing' || 'master' }}
          path: master-branch

      # Checkout the PR branch into a subdirectory
      - name: Checkout PR branch
        uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
        with:
          ref: "${{ github.sha }}"
          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 master-branch tools
        shell: bash # We're only building the `master` branch version of the tools, so don't need to run inside landrun.
        run: |
          cd master-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: cleanup .cache/mathlib
        # This needs write access to .cache/mathlib, so can't be run inside landrun.
        # However it is only using the `master` version of `cache`, so is safe to run outside landrun.
        shell: bash
        run: |
          # Define the cache directory path
          CACHE_DIR="$HOME/.cache/mathlib"

          # Check if directory exists
          if [ ! -d "$CACHE_DIR" ]; then
            echo "::warning::Cache directory does not exist: $CACHE_DIR"
            exit 0
          fi

          # Calculate directory size in bytes
          DIR_SIZE=$(du -sb "$CACHE_DIR" | cut -f1)
          printf 'Cache size (in bytes): %s\n' "$DIR_SIZE"

          # Check if size exceeds 10GB
          if [ "$DIR_SIZE" -gt "10737418240" ]; then
            echo "Cache size exceeds threshold, running lake exe cache clean"
            # We use the master-branch version of `cache`.
            cd master-branch
            lake exe cache clean
          fi

      - 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: verify ProofWidgets lean-toolchain matches on versioned releases
        # Only enforce this on the main mathlib4 repository, not on nightly-testing
        if: github.repository == 'leanprover-community/mathlib4'
        shell: bash
        run: |
          cd pr-branch

          # Read the lean-toolchain file
          TOOLCHAIN=$(cat lean-toolchain | tr -d '[:space:]')
          echo "Lean toolchain: $TOOLCHAIN"

          # Check if toolchain matches the versioned release pattern: leanprover/lean4:vX.Y.Z (with optional suffix like -rc1)
          if [[ "$TOOLCHAIN" =~ ^leanprover/lean4:v[0-9]+\.[0-9]+\.[0-9]+(-[a-zA-Z0-9.-]+)?$ ]]; then
            echo "✓ Detected versioned Lean release: $TOOLCHAIN"
            echo "Verifying ProofWidgets lean-toolchain matches..."

            # Check if ProofWidgets lean-toolchain exists
            if [ ! -f .lake/packages/proofwidgets/lean-toolchain ]; then
              echo "❌ Error: .lake/packages/proofwidgets/lean-toolchain does not exist"
              echo "This file should be created by 'lake env' during dependency download."
              exit 1
            fi

            # Read ProofWidgets lean-toolchain
            PROOFWIDGETS_TOOLCHAIN=$(cat .lake/packages/proofwidgets/lean-toolchain | tr -d '[:space:]')
            echo "ProofWidgets toolchain: $PROOFWIDGETS_TOOLCHAIN"

            # Compare the two
            if [ "$TOOLCHAIN" != "$PROOFWIDGETS_TOOLCHAIN" ]; then
              echo "❌ Error: Lean toolchain mismatch!"
              echo "  Main lean-toolchain: $TOOLCHAIN"
              echo "  ProofWidgets lean-toolchain: $PROOFWIDGETS_TOOLCHAIN"
              echo ""
              echo "When using a versioned Lean release (leanprover/lean4:vX.Y.Z),"
              echo "the ProofWidgets dependency must use the same toolchain."
              echo "Please update the ProofWidgets dependency to use $TOOLCHAIN"
              exit 1
            else
              echo "✅ ProofWidgets lean-toolchain matches: $TOOLCHAIN"
            fi
          else
            echo "ℹ Lean toolchain is not a versioned release (pattern: leanprover/lean4:vX.Y.Z)"
            echo "Skipping ProofWidgets toolchain verification."
          fi

      - name: get cache (1/3 - setup and initial fetch)
        id: get_cache_part1_setup
        shell: bash # only runs `cache get` from `master-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..."
          ../master-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 `cache get` from `master-branch`, so doesn't need to be inside landrun
        run: |
          cd pr-branch
          if [[ "${{ steps.get_cache_part2_test.outcome }}" == "success" ]]; then
            echo "Fetching all remaining cache..."

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

            # Run again with --repo, to ensure we actually get the oleans.
            ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} get
          else
            echo "WARNING: 'lake build --no-build -v Mathlib.Init' failed."
            echo "No cache for 'Mathlib.Init' available or it could not be prepared."
          fi

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

          ../master-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"

      - name: upload artifact containing contents of pr-branch
        # temporary measure for debugging no-build failures
        uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6.0.0
        with:
          name: mathlib4_artifact
          include-hidden-files: true
          # we exclude .git since there may be secrets in there
          path: |
            pr-branch/
            !pr-branch/.git/

      # The cache secrets are available here, so we must not run any untrusted code.
      - name: Upload cache to Azure
        # 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() && steps.get.outcome == 'success' }}
        shell: bash
        run: |
          cd pr-branch

          # Trim trailing whitespace from secrets to prevent issues with accidentally added spaces
          export MATHLIB_CACHE_SAS="${MATHLIB_CACHE_SAS_RAW%"${MATHLIB_CACHE_SAS_RAW##*[![:space:]]}"}"

          # Use the trusted cache tool from master-branch
          # TODO: this is not doing anything currently, and needs to be integrated with put-unpacked
          # ../master-branch/.lake/build/bin/cache commit || true
          # run this in CI if it gets an incorrect lake hash for existing cache files somehow
          # ../master-branch/.lake/build/bin/cache put!
          # do not try to upload files just downloaded

          echo "Uploading cache to Azure..."
          MATHLIB_CACHE_USE_CLOUDFLARE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked
        env:
          MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }}

      # 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
          ../master-branch/.lake/build/bin/cache get Archive.lean
          ../master-branch/.lake/build/bin/cache get Counterexamples.lean

      - name: build archive
        id: archive
        continue-on-error: true
        run: |
          cd pr-branch
          ../master-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
          ../master-branch/scripts/lake-build-with-retry.sh Counterexamples
          # results of build at pr-branch/.lake/build_summary_Counterexamples.json

      - 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

      # The cache secrets are available here, so we must not run any untrusted code.
      - name: Upload Archive and Counterexamples cache to Azure
        shell: bash
        run: |
          cd pr-branch

          # Trim trailing whitespace from secrets to prevent issues with accidentally added spaces
          export MATHLIB_CACHE_SAS="${MATHLIB_CACHE_SAS_RAW%"${MATHLIB_CACHE_SAS_RAW##*[![:space:]]}"}"

          echo "Uploading Archive and Counterexamples cache to Azure..."
          MATHLIB_CACHE_USE_CLOUDFLARE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked Archive.lean
          MATHLIB_CACHE_USE_CLOUDFLARE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked Counterexamples.lean
        env:
          MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }}

      - 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
          ../master-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: 30
        run: |
          cd pr-branch
          # 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
          if ! env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee .lake/lint_output.txt; then
            if grep -q "cannot parse arguments" .lake/lint_output.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 ""
            fi
            exit 1
          fi

      - 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

      - name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
        if: always()
        shell: bash
        env:
          TOKEN: ${{ secrets.LEAN_PR_TESTING }}
          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: |
          master-branch/scripts/lean-pr-testing-comments.sh lean
          master-branch/scripts/lean-pr-testing-comments.sh batteries

  post_steps:
    name: Post-Build Step
    if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'
    needs: [build]
    runs-on: ubuntu-latest # Note these steps run on disposable GitHub runners, so no landrun sandboxing is needed.
    steps:

      - uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
        with:
          ref: "${{ github.sha }}"

      - name: Configure Lean
        uses: leanprover/lean-action@434f25c2f80ded67bba02502ad3a86f25db50709 # v1.3.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@b7c566a772e6b6bfb58ed0dc250532a479d7789f # v6.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 pole unused

      - 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
    if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'
    runs-on: ubuntu-latest
    steps:
      - uses: leanprover-community/lint-style-action@a7e7428fa44f9635d6eb8e01919d16fd498d387a # 2025-08-18
        with:
          mode: check
          lint-bib-file: true
          ref: ${{ github.sha }}

  final:
    name: Post-CI job
    if: github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing'
    needs: [style_lint, build, post_steps]
    runs-on: ubuntu-latest
    steps:
      - id: PR_from_push
        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

      # TODO: delete this step and rename `PR_from_push` to `PR` if the above step seems to work properly
      # Combine the output from the previous action with the metadata supplied by GitHub itself.
      # Note that if we fall back to github.event.pull_request data, the list of labels is generated when this workflow is triggered
      # and not updated afterwards!
      - id: PR
        shell: bash
        run: |
          echo "number=${{ steps.PR_from_push.outputs.number || github.event.pull_request.number }}" | tee -a "$GITHUB_OUTPUT"
          echo "pr_labels=${{ steps.PR_from_push.outputs.pr_labels || join(github.event.pull_request.labels.*.name, ',') }}" | tee -a "$GITHUB_OUTPUT"

      - 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: 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: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
        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') && (contains(steps.actorTeams.outputs.teams, 'mathlib-maintainers') || 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:
          token: ${{ secrets.AUTO_MERGE_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