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'
      # do not build lean-x.y.z branch used by leanpkg
      - 'lean-3.*'
      # 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/mathlib'
    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/mathlib'
    name: Lint style
    runs-on: ubuntu-latest
    steps:
      - 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 style
        run: |
          ./scripts/lint-style.sh

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

  build:
    if: github.repository == 'leanprover-community/mathlib'
    name: Build mathlib
    runs-on: pr
    env:
      # number of commits to check for olean cache
      GIT_HISTORY_DEPTH: 20
    outputs:
      artifact_name: ${{ steps.setup_precompiled.outputs.artifact_name }}
    steps:
      - uses: actions/checkout@v3
        with:
          fetch-depth: ${{ env.GIT_HISTORY_DEPTH }}

      - name: install elan
        run: |
          set -o pipefail
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
          ~/.elan/bin/lean --version
          echo "$HOME/.elan/bin" >> $GITHUB_PATH
          echo "short_lean_version=$(~/.elan/bin/lean --run scripts/lean_version.lean)" >> $GITHUB_ENV

      - name: install Python
        if: ${{ ! 1 }}
        uses: actions/setup-python@v4
        with:
          python-version: 3.8

      - name: try to find olean cache
        run: ./scripts/fetch_olean_cache.sh

      - name: leanpkg build
        id: build
        run: |
          set -o pipefail
          leanpkg configure
          echo "started=true" >> $GITHUB_OUTPUT
          lean --json -T100000 --make src | python3 scripts/detect_errors.py
          lean --json -T400000 --make src | python3 scripts/detect_errors.py

      - name: push release to azure
        if: always() && github.repository == 'leanprover-community/mathlib' && steps.build.outputs.started == 'true'
        run: |
          archive_name="$(git rev-parse HEAD).tar.gz"
          find src/ -name "*.olean" -o -name ".noisy_files" | tar czf "$archive_name" -T -
          azcopy copy "$archive_name" "${{ secrets.AZURE_SAS_TOKEN }}" --block-size-mb 99 --overwrite false
          archive_name="$(git rev-parse HEAD).tar.xz"
          find src/ -name "*.olean" -o -name ".noisy_files" | tar cJf "$archive_name" -T -
          azcopy copy "$archive_name" "${{ secrets.AZURE_SAS_TOKEN }}" --block-size-mb 99 --overwrite false

      - name: setup precompiled zip file
        if: always() && steps.build.outputs.started == 'true'
        id: setup_precompiled
        run: |
          touch workspace.tar
          tar -cf workspace.tar --exclude=*.tar* .
          git_hash="$(git log -1 --pretty=format:%h)"
          echo "artifact_name=precompiled-mathlib-$short_lean_version-$git_hash" >> $GITHUB_OUTPUT

      - name: upload precompiled mathlib zip file
        if: always() && steps.build.outputs.started == 'true'
        uses: actions/upload-artifact@v2
        with:
          name: ${{ steps.setup_precompiled.outputs.artifact_name }}
          path: workspace.tar

      - name: cleanup after upload step
        # cf. https://github.com/actions/upload-artifact/issues/256
        if: always() && steps.build.outputs.started == 'true' && ${{ 1 }}
        run: rm /tmp/tmp-* || true

      - name: clean up working directory and elan
        if: always() && ${{ 1 }}
        run: rm -rf * $HOME/.elan

  lint:
    name: Lint mathlib
    runs-on: pr
    needs: build

    # skip on master branch
    if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'

    steps:
      - name: clean build directory
        if: ${{ 1 }}
        run: rm -rf ./* ./.??*

      - name: retrieve build
        uses: actions/download-artifact@v3
        with:
          name: ${{ needs.build.outputs.artifact_name }}

      - name: untar build
        run: tar -xf workspace.tar

      - name: install elan
        run: |
          set -o pipefail
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
          ~/.elan/bin/lean --version
          echo "$HOME/.elan/bin" >> $GITHUB_PATH

      - name: lint
        run: |
          ./scripts/mk_all.sh
          lean --run scripts/lint_mathlib.lean --github

      - name: clean up working directory and elan
        if: always() && ${{ 1 }}
        run: rm -rf * $HOME/.elan

  tests:
    name: Run tests
    runs-on: pr
    needs: build

    # skip on master branch
    if: github.repository != 'leanprover-community/mathlib' || github.ref != 'refs/heads/master'

    steps:
      - name: clean build directory
        if: ${{ 1 }}
        run: rm -rf ./* ./.??*

      - name: retrieve build
        uses: actions/download-artifact@v3
        with:
          name: ${{ needs.build.outputs.artifact_name }}

      - name: untar build
        run: tar -xf workspace.tar

      - name: install elan
        run: |
          set -o pipefail
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
          ~/.elan/bin/lean --version
          echo "$HOME/.elan/bin" >> $GITHUB_PATH

      - name: install Python
        if: ${{ ! 1 }}
        uses: actions/setup-python@v4
        with:
          python-version: 3.8

      - name: install Python dependencies
        if: ${{ ! 1 }}
        run: python3 -m pip install --upgrade pip pyyaml requests mathlibtools

      - name: tests
        run: |
          set -o pipefail
          lean --json -T100000 --make docs archive roadmap test counterexamples | python3 scripts/detect_errors.py

      - name: check archive and counterexample directories have unique identifiers
        run: |
          pip install mathlibtools
          (cd archive && python -m mathlibtools.leanproject mk-all && mv all.lean archive_all.lean)
          (cd counterexamples && python -m mathlibtools.leanproject mk-all && mv all.lean counterexamples_all.lean)
          python -m mathlibtools.leanproject mk-all
          echo "import all" >> all_all.lean
          echo "import counterexamples_all" >> all_all.lean
          echo "import archive_all" >> all_all.lean
          echo "path ./archive" >> leanpkg.path
          echo "path ./counterexamples" >> leanpkg.path
          lean --json -T100000 --make all_all.lean | python3 scripts/detect_errors.py

      - uses: actions/setup-java@v2
        if: ${{ ! 1 }}
        with:
          distribution: 'adopt'
          java-version: '16'

      - name: install trepplein
        run: |
          trepplein_version=1.1
          wget https://github.com/gebner/trepplein/releases/download/v$trepplein_version/trepplein-$trepplein_version.zip
          unzip trepplein-$trepplein_version.zip
          echo $PWD/trepplein-$trepplein_version/bin >>$GITHUB_PATH

      - name: export as low-level text file
        run: lean --recursive --export=mathlib.txt src/

      - name: trepplein
        run: trepplein mathlib.txt

      - name: check declarations in db files
        run: |
          python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
          bash scripts/mk_all.sh
          lean --run scripts/yaml_check.lean

      - name: clean up working directory and elan
        if: always() && ${{ 1 }}
        run: rm -rf * $HOME/.elan

  final:
    name: Post-CI job
    if: github.repository == 'leanprover-community/mathlib'
    needs: [style_lint, build, lint, tests]
    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 }}'