Commit 2024-06-21 07:01 00d112fb

View on Github →

feat: rewrite file length check in Lean (#13620) This is the first in a series of PRs rewriting most checks from lint-style.py in Lean. This PR sets up the basic infrastructure and ports the check for files longer than 1500 lines. This includes parsing style-exceptions.txt. To enable a gradual conversion of the linters, this PR adds a new executable lint_style (which runs the rewritten linters), and has lint-style.sh call this one also.

Estimated changes

Modified .github/workflows/bors.yml

Modified .github/workflows/build.yml

Modified .github/workflows/build.yml.in

Modified .github/workflows/build_fork.yml

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/Linter/TextBased.lean

added structure ErrorContext

added def StyleError.errorCode

added def StyleError.errorMessage

added def StyleError.normalise

added inductive StyleError

added def checkFileLength

added def formatErrors

added def isImportsOnlyFile

added def lintAllFiles

added def lintFile

added def main

added def outputMessage

added def parse?_errorContext

added def parseStyleExceptions

Modified lakefile.lean

Modified scripts/lint-style.py

Modified scripts/lint-style.sh

Modified scripts/update-style-exceptions.sh