Update lake-manifest.json #96
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 Project -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 Project -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$') |