nolints.yml

name: update nolints

on:
  workflow_dispatch: ~
  schedule:
    - cron: "0 0 * * *"

jobs:
  build:
    name: Build, lint and update nolints
    runs-on: ubuntu-latest
    env:
      # number of commits to check for olean cache
      GIT_HISTORY_DEPTH: 20
    steps:
      - uses: actions/checkout@v2
        with:
          fetch-depth: ${{ env.GIT_HISTORY_DEPTH }}
          # We need to use a personal access token here. See the comment in upgrade_lean.yml.
          token: ${{ secrets.PA_TOKEN }}

      - 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 "name=short_lean_version::$(~/.elan/bin/lean --run scripts/lean_version.lean)" >> $GITHUB_ENV

      - name: install Python
        uses: actions/setup-python@v1
        with:
          python-version: 3.8

      - name: install mathlibtools
        run: python -m pip install --upgrade pip mathlibtools

      - name: leanpkg configure
        run: leanpkg configure

      - name: get mathlib cache
        run: leanproject get-mathlib-cache || true

      - name: try to find olean cache
        continue-on-error: true
        run: ./scripts/fetch_olean_cache.sh

      - name: leanpkg build
        id: build
        run: |
          leanpkg configure
          lean --json --make src | python scripts/detect_errors.py

      - name: lint
        run: |
          ./scripts/mk_all.sh
          lean --run ./scripts/lint_project.lean || true
          if [[ ! -e nolints.txt ]]; then
            echo "Error during linting - could not generate nolints.txt"
            exit 1
          fi
          mv nolints.txt scripts/nolints.txt
          # ./scripts/update-style-exceptions.sh
          git diff

      - name: configure git user
        run: |
          git config user.email "leanprover.community@gmail.com"
          git config user.name "leanprover-community-bot"
          git config pull.rebase true

      - name: update nolints.txt
        run: ./scripts/update_nolints.sh