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:
      - uses: actions/checkout@v4

      - id: lean-action
        name: build, test, and lint batteries
        uses: leanprover/lean-action@v1
        with:
          build-args: '--wfail'

      - 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 Batteries -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 "./BatteriesTest/import_lean.lean" -type f -print0 | xargs -0 grep -E -n '^import Lean$')