push_pr.yml

on:
  pull_request:
  push:
    branches-ignore:
      - master

jobs:
  style_lint:
    name: Lint style
    runs-on: ubuntu-latest
    steps:
      - name: Check for long lines
        if: always()
        run: |
          ! (find PFR -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')

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

  build_project:
    runs-on: ubuntu-latest
    name: Build project
    steps:
      - name: Checkout project
        uses: actions/checkout@v2
        with:
          fetch-depth: 0

      - name: Install elan
        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.0

      - name: Get cache
        run: ~/.elan/bin/lake exe cache get || true

      - name: Build project
        run: ~/.elan/bin/lake build PFR