build_fork.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 GitHub-hosted workers and will only be run from external forks

on:
  push:
    branches-ignore:
      # ignore tmp branches used by bors
      - 'staging.tmp*'
      - 'trying.tmp*'
      - 'staging*.tmp'
      - 'nolints'

name: continuous integration (mathlib forks)

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.11.0
        with:
          all_but_latest: true
          access_token: ${{ github.token }}

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

      - uses: actions/checkout@v3

      # 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@v4
        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 (fork)
    runs-on: ubuntu-latest
    steps:
      - name: cleanup
        run: |
          find . -name . -o -prune -exec rm -rf -- {} +

      - uses: actions/checkout@v3

      - 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 MathlibExtras.lean
        run: |
          git ls-files 'MathlibExtras/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > MathlibExtras.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 (fork)
    runs-on: ubuntu-latest
    steps:
      - name: cleanup
        run: |
          find . -name . -o -prune -exec rm -rf -- {} +

      - uses: actions/checkout@v3

      - 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 (fork)
    runs-on: ubuntu-latest
    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`.
          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/{}"' || true

      # 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@v3

      # 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
            echo "Uninstalling transient toolchain `cat lean-toolchain`"
            elan toolchain uninstall `cat lean-toolchain`
          fi

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

      - name: get cache
        run: |
          lake exe cache clean
          # We've been seeing many failures at this step recently because of network errors.
          # As a band-aid, we try twice.
          # The 'sleep 1' is small pause to let the network recover.
          lake exe cache get || (sleep 1; lake exe cache get)

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

      - name: check for noisy stdout lines
        run: |
          ! grep --after-context=1 "stdout:" stdout.log

      - name: build library_search cache
        run: lake build -KCI MathlibExtras

      - name: upload cache
        if: always()
        run: |
          # run this in CI if it gets an incorrect lake hash for existing cache files somehow
          # lake exe cache pack! || true
          lake exe cache commit || true
          # try twice in case of network errors
          lake exe cache put || (sleep 1; lake exe cache put) || true
        env:
          MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}

      - 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 get || (sleep 1; lake exe cache get)
            # We pipe the output of `lake build` to a file,
            # and if we find " Building Mathlib" in that file we kill `lake build`, and error.
            lake build > tmp & tail --pid=$! -n +1 -F tmp | (! (grep -m 1 " Building Mathlib" && kill $! ))
          fi

      - name: build archive
        run: |
          # Note: we should not be including `Archive` and `Countexamples` 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.
          # We retry twice in case of network errors.
          lake exe cache get Archive.lean || (sleep 1; lake exe cache get Archive.lean)
          lake build Archive
          lake exe cache put Archive.lean || (sleep 1; lake exe cache put Archive.lean)
        env:
          MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}

      - name: build counterexamples
        run: |
          lake exe cache get Counterexamples.lean || (sleep 1; lake exe cache get Counterexamples.lean)
          lake build Counterexamples
          lake exe cache put Counterexamples.lean || (sleep 1; lake exe cache put Counterexamples.lean)
        env:
          MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}

      - 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
        run: |
          # Tests use parts of ProofWidgets not imported by Mathlib.
          # Ensure everything has been built.
          lake build ProofWidgets
          make -j 8 test

      - name: lint mathlib
        id: lint
        uses: liskin/gh-problem-matcher-wrap@v2
        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 toolchain/v4.3.0
          # 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 }}
          LINT_OUTCOME: ${{ steps.lint.outcome }}
          TEST_OUTCOME: ${{ steps.test.outcome }}
          BUILD_OUTCOME: ${{ steps.build.outcome }}
          CHECK_OUTCOME: ${{ steps.lean4checker.outcome }}
        run: |
          scripts/lean-pr-testing-comments.sh

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

      - 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