build.yml

# DO NOT EDIT THIS FILE!!!

# This file is automatically generated by mk_build_yml.sh
# Edit build.yml.in instead and run 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

jobs:
  # Cancels previous runs of jobs in this file
  cancel:
    if: github.repository == 'leanprover-community/mathlib4'
    name: 'Cancel Previous Runs (CI)'
    runs-on: ubuntu-latest
    # timeout-minutes: 3
    steps:
      - uses: styfle/cancel-workflow-action@0.12.1
        with:
          all_but_latest: true
          access_token: ${{ github.token }}

  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.1.0

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

      - name: lint
        run: |
          ./scripts/lint-style.sh

      - 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

  check_imported:
    if: github.repository == 'leanprover-community/mathlib4'
    name: Check all files imported
    runs-on: ubuntu-latest
    steps:
      - name: cleanup
        run: |
          find . -name . -o -prune -exec rm -rf -- {} +

      - uses: actions/checkout@v4

      - name: update Mathlib.lean
        run: |
          git ls-files 'Mathlib/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean

      - name: update Mathlib/Tactic.lean
        run: |
          git ls-files 'Mathlib/Tactic/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib/Tactic.lean

      - name: update Counterexamples.lean
        run: |
          git ls-files 'Counterexamples/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Counterexamples.lean

      - name: update Archive.lean
        run: |
          git ls-files 'Archive/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Archive.lean

      - name: check that all files are imported
        run: git diff --exit-code

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

      - uses: actions/checkout@v4

      - name: update workflows
        run: |
          cd .github/workflows/
          ./mk_build_yml.sh

      - name: check that workflows were consistent
        run: git diff --exit-code

  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@v1.0.1

      - name: install elan
        run: |
          set -o pipefail
          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/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

      # We update `Mathlib.lean` as a convenience here,
      # but verify that this didn't change anything in the `check_imported` job.
      - name: update Mathlib.lean
        run: |
          find Mathlib -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean

      - 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: prune ProofWidgets .lake
        run: |
          # The ProofWidgets release contains not just the `.js` (which we need in order to build)
          # but also `.oleans`, which may have been built with the wrong toolchain.
          # This removes them.
          # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
          rm -rf .lake/packages/proofwidgets/.lake/build/lib
          rm -rf .lake/packages/proofwidgets/.lake/build/ir

      - name: get cache
        run: |
          lake exe cache clean
          lake exe cache get

      - 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 | tee stdout.log"

      - name: upload cache
        # We only upload the cache if the build ran (either succeeding or failing),
        # but not if it was skipped.
        if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
        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: find `#`-commands
        id: hash_commands
        run: |
          chmod u+x scripts/lint_hash_commands.sh
          ./scripts/lint_hash_commands.sh

      - 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 | tee --append stdout.log"
          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 | tee --append stdout.log"
          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 for noisy stdout lines
        id: noisy
        run: |
          grep --after-context=1 "stdout" stdout.log && ret=0
          grep --after-context=1 "stderr" stdout.log && new=0
          if [ "${ret}" == "0" ] || [ "${new}"  == "0" ]; then exit 1; fi

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

      - name: verify `lake exe graph` works
        run: |
          lake exe graph
          rm import_graph.dot

      - name: test mathlib
        id: test
        uses: liskin/gh-problem-matcher-wrap@v3
        with:
          linters: gcc
          run: |
            bash -o pipefail -c "
            make -k -j 8 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

      - name: check environments using lean4checker
        id: lean4checker
        run: |
          git clone https://github.com/leanprover/lean4checker
          cd lean4checker
          git checkout v4.8.0-rc1
          # Now that the git hash is embedded in each olean,
          # we need to compile lean4checker on the same toolchain
          cp ../lean-toolchain .
          lake build
          ./test.sh
          cd ..
          lake env lean4checker/.lake/build/bin/lean4checker

      - name: Post comments for lean-pr-testing branch
        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 }}
          COUNTEREXAMPLE_OUTCOME: ${{ steps.counterexamples.outcome }}
          LINT_OUTCOME: ${{ steps.lint.outcome }}
          TEST_OUTCOME: ${{ steps.test.outcome }}
          CHECK_OUTCOME: ${{ steps.lean4checker.outcome }}
        run: |
          scripts/lean-pr-testing-comments.sh

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

      - id: PR
        uses: 8BitJonny/gh-get-current-pr@2.2.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.0.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