build.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-ignore:
      # ignore tmp branches used by bors
      - 'staging.tmp*'
      - 'trying.tmp*'
      - 'staging*.tmp'
      - 'nolints'
      # ignore staging branch used by bors, this is handled by bors.yml
      - 'staging'
  merge_group:

name: continuous integration

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

concurrency:
  # label each workflow run; only the latest with each label will run
  # workflows on master get more expressive labels
  group: ${{ github.workflow }}-${{ github.ref }}.
    ${{ ( 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

jobs:
  style_lint:
    if: github.repository == 'leanprover-community/mathlib4'
    name: Lint style
    runs-on: ubuntu-latest
    steps:
      - name: cleanup
        run: |
          find . -name . -o -prune -exec rm -rf -- {} +

      - uses: actions/checkout@v4

      # Run the case checker action
      - name: Check Case Sensitivity
        uses: credfeto/action-case-checker@v1.3.0

      - name: Look for ignored files
        uses: credfeto/action-no-ignored-files@v1.2.0

      - name: "Check for Lean files with the executable bit set"
        shell: bash
        run: |
          executable_files="$(find . -name '*.lean' -type f \( -perm -u=x -o -perm -g=x -o -perm -o=x \))"
          if [[ -n "$executable_files" ]]
          then
            echo "ERROR: The following Lean files have the executable bit set."
            echo "$executable_files"
            exit 1
          fi

      - name: install Python
        if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }}
        uses: actions/setup-python@v5
        with:
          python-version: 3.8

      - name: install elan
        run: |
          set -o pipefail
          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
          ./elan-init -y --default-toolchain none
          echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"

      - name: "run style linters"
        run: |
          lake exe lint-style

      - name: Install bibtool
        if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }}
        run: |
          sudo apt-get update
          sudo apt-get install -y bibtool

      - name: lint references.bib
        run: |
          ./scripts/lint-bib.sh

  build:
    if: github.repository == 'leanprover-community/mathlib4'
    name: Build
    runs-on: pr
    steps:
      - name: cleanup
        run: |
          find . -name . -o -prune -exec rm -rf -- {} +
          # 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@v2.1.0

      - name: install elan
        run: |
          set -o pipefail
          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
          ./elan-init -y --default-toolchain none
          echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"

      - uses: actions/checkout@v4

      - name: If using a lean-pr-release toolchain, uninstall
        run: |
          if [[ $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
            printf 'Uninstalling transient toolchain %s\n' "$(cat lean-toolchain)"
            elan toolchain uninstall "$(cat lean-toolchain)"
          fi

      - name: print lean and lake versions
        run: |
          lean --version
          lake --version

      - name: build cache
        run: |
          lake build cache

      - name: get cache
        id: get
        run: |
          rm -rf .lake/build/lib/Mathlib/
          # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
          lake exe cache get Mathlib.Init
          lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"

      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
        id: mk_all
        run: |

          if ! lake exe mk_all --check
          then
            echo "Not all lean files are in the import all files"
            echo "mk_all=false" >> "${GITHUB_OUTPUT}"
          else
            echo "mk_all=true" >> "${GITHUB_OUTPUT}"
          fi

      - name: build mathlib
        id: build
        uses: liskin/gh-problem-matcher-wrap@v3
        with:
          linters: gcc
          run: |
            bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"

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

      - name: upload cache
        # 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' }}
        run: |
          # TODO: this is not doing anything currently, and needs to be integrated with put-unpacked
          # lake exe cache commit || true
          # run this in CI if it gets an incorrect lake hash for existing cache files somehow
          # lake exe cache put!
          # do not try to upload files just downloaded
          lake exe cache put-unpacked
        env:
          MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
          MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}

      - name: check the cache
        run: |
          # Because the `lean-pr-testing-NNNN` branches use toolchains that are "updated in place"
          # the cache mechanism is unreliable, so we don't test it if we are on such a branch.
          if [[ ! $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
            lake exe cache clean!
            rm -rf .lake/build/lib/Mathlib
            lake exe cache get || (sleep 1; lake exe cache get)
            lake build --no-build
          fi

      - name: build archive
        id: archive
        run: |
          # 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.
          lake exe cache get Archive.lean
          bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build Archive"
          lake exe cache put Archive.lean
        env:
          MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
          MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}

      - name: build counterexamples
        id: counterexamples
        run: |
          lake exe cache get Counterexamples.lean
          bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build Counterexamples"
          lake exe cache put Counterexamples.lean
        env:
          MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
          MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}

      - name: Check {Mathlib, Tactic, Counterexamples, Archive}.lean
        run: |
          if [ ${{ steps.mk_all.outputs.mk_all }} == "false" ]
          then
            echo "Please run 'lake exe mk_all' to regenerate the import all files"
            exit 1
          fi

      - name: check for noisy stdout lines
        id: noisy
        run: |
          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."){ print $0 }')"
          if [ -n "${buildMsgs}" ]
          then
            printf $'%s\n' "${buildMsgs}"
            exit 1
          fi

      - 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@v4
        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
        run: |
          lake build Batteries Qq Aesop ProofWidgets Plausible

      - name: test mathlib
        id: test
        uses: liskin/gh-problem-matcher-wrap@v3
        with:
          linters: gcc
          run:
            lake --iofail test

      - name: check for unused imports
        id: shake
        uses: liskin/gh-problem-matcher-wrap@v3
        with:
          linters: gcc
          run: 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
        uses: liskin/gh-problem-matcher-wrap@v3
        with:
          linters: gcc
          run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib

      # 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 `lean4checker.yml`.
      # Output is posted to the zulip topic
      # https://leanprover.zulipchat.com/#narrow/stream/345428-mathlib-reviewers/topic/lean4checker

      - name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
        if: always()
        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 }}
        run: |
          scripts/lean-pr-testing-comments.sh lean
          scripts/lean-pr-testing-comments.sh batteries

      - name: build lean4checker, but don't run it
        if: ${{ (always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure') && contains(github.event.pull_request.changed_files, 'lean-toolchain') }}
        run: |
          git clone https://github.com/leanprover/lean4checker
          cd lean4checker
          # Read lean-toolchain file and checkout appropriate branch
          TOOLCHAIN=$(cat ../lean-toolchain)
          if [[ "$TOOLCHAIN" =~ ^leanprover/lean4:v ]]; then
            VERSION=${TOOLCHAIN#leanprover/lean4:}
            git checkout "$VERSION"
          else
            git checkout master
          fi
          # Build lean4checker using the same toolchain
          cp ../lean-toolchain .
          lake build

  final:
    name: Post-CI job
    if: github.repository == 'leanprover-community/mathlib4'
    needs: [style_lint, build]
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

      - id: PR
        uses: 8BitJonny/gh-get-current-pr@3.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: If `auto-merge-after-CI` is present, add a `bors merge` comment.
        uses: GrantBirki/comment@v2
        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