Skip to content

Minor: fix some build linter issues (#326) #921

Minor: fix some build linter issues (#326)

Minor: fix some build linter issues (#326) #921

Workflow file for this run

name: Lint Style
on:
push:
branches:
- main
paths:
- '**/*.lean'
- 'lean-toolchain'
- 'lakefile.toml'
- 'lake-manifest.json'
pull_request:
branches:
- main
paths:
- '**/*.lean'
- 'lean-toolchain'
- 'lakefile.toml'
- 'lake-manifest.json'
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 equational_theories -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 equational_theories -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$')