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'

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.11.0
        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@v3

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

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

  build:
    if: github.repository == 'leanprover-community/mathlib4'
    name: Build
    runs-on: pr
    steps:
      - name: cleanup
        run: |
          find . -name . -o -prune -exec rm -rf -- {} +

      - name: install elan
        run: |
          set -o pipefail
          curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/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: get cache
        run: |
          lake exe cache clean
          lake exe cache get

      - name: build mathlib
        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 "stdout:" stdout.log

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

      - name: upload cache
        if: always()
        run: |
          lake exe cache commit || true
          lake exe cache put || true
        env:
          MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}

      - name: build archive
        run: lake build Archive

      - name: build counterexamples
        run: lake build Counterexamples

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

      - name: test mathlib
        run: make -j 8 test

      - name: lint mathlib
        uses: liskin/gh-problem-matcher-wrap@v2
        with:
          linters: gcc
          run: env LEAN_ABORT_ON_PANIC=1 make lint

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