build.yml

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

name: ci

jobs:
  build:
    name: Build
    runs-on: ubuntu-latest
    steps:
      - 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@v2

      - name: build std
        id: build
        run: lake build -Kwerror

      - name: test std
        if: steps.build.outcome == 'success'
        run: make test

      - name: lint std
        if: steps.build.outcome == 'success'
        run: make lint

      - name: Check that all files are imported
        run: lake env lean scripts/check_imports.lean

      - name: Check for forbidden character ↦
        if: always()
        run: |
          if grep -r -n --include=\*.lean -e '↦' . ; then
            echo "Error: Found forbidden character ↦"
            exit 1
          fi

      - name: Check for 'namespace Mathlib'
        if: always()
        run: |
          if grep -r -n --include=\*.lean -e 'namespace Mathlib' . ; then
            echo "Error: Found 'namespace Mathlib'"
            exit 1
          fi

      - name: Check for long lines
        if: always()
        run: |
          ! (find Std -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')

      - name: Check for trailing whitespace
        if: always()
        run: |
          scripts/lintWhitespace.sh

      - name: Don't 'import Lean', use precise imports
        if: always()
        run: |
          ! (find . -name "*.lean" ! -path "./test/import_lean.lean" -type f -print0 | xargs -0 grep -E -n '^import Lean$')