lint.yml

name: Lint Style

on:
    push:
       branches: ["main"] # Trigger the workflow on pushes to the "main" branch (replace "main" with your default branch if different)
    pull_request:
       branches: ["main"] # Trigger the workflow on pull requests targeting the "main" branch (replace "main" with your default branch if different)
    workflow_dispatch:    # Allow manual triggering of the workflow from the GitHub Actions interface

# Set permissions for the workflow
permissions:
    contents: read  # Grant read access to repository contents
    pages: write    # Grant write access to GitHub Pages
    id-token: write # Grant write access to ID tokens

jobs:
  style_lint:
    runs-on: ubuntu-latest
    steps:
      - name: Check for long lines
        if: always() # Ensure the step runs regardless of the success or failure of previous steps
        run: |
          # Find Lean files with lines longer than 100 characters, excluding URLs
          ! (find expdb -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')

      - name: Don't 'import Mathlib', use precise imports
        if: always() # Ensure the step runs regardless of the success or failure of previous steps
        run: |
          # Find and disallow any file that imports the entire Mathlib, encouraging precise imports instead
          ! (find expdb -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$')