Skip to content

remove reflexivity handling from outcomes_to_image.py (#227) #752

remove reflexivity handling from outcomes_to_image.py (#227)

remove reflexivity handling from outcomes_to_image.py (#227) #752

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 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$')