Skip to content

LeanAgent Proofs (#67) #138

LeanAgent Proofs (#67)

LeanAgent Proofs (#67) #138

Workflow file for this run

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 FormalBook -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 FormalBook -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$')