push.yml

on:
  push:
    branches:
      - master

# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
permissions:
  contents: read
  pages: write
  id-token: write

jobs:
  style_lint:
    name: Lint style
    runs-on: ubuntu-latest
    steps:
      - name: Check for long lines
        if: always()
        run: |
          ! (find LeanCondensed -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 LeanCondensed -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 none

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

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

      # - name: Cache mathlib docs
      #   uses: actions/cache@v3
      #   with:
      #     path: |
      #       .lake/build/doc/Init
      #       .lake/build/doc/Lake
      #       .lake/build/doc/Lean
      #       .lake/build/doc/Std
      #       .lake/build/doc/Mathlib
      #       .lake/build/doc/declarations
      #       !.lake/build/doc/declarations/declaration-data-LeanCondensed*
      #     key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
      #     restore-keys: |
      #       MathlibDoc-