Commit 2024-06-23 12:43 1ca54303

View on Github →

feat: rewrite the copyright header check in Lean (#13240) This is one in a series of PRs rewriting most checks from lint-style.py in Lean. This PR moves the check for copyright headers and authors: the check has been rewritten anew (and is hopefully simpler to understand now); this has made it stricter in various places. The necessary adjustments have been made in #13212 and #13247. This PR also adds a nolints file for text-based linters.

Estimated changes

Modified Mathlib/Tactic/Linter/TextBased.lean

added def allLinters

added def copyrightHeaderLinter

added def isCorrectAuthorsLine

deleted def isImportsOnlyFile

modified def lintFile

Modified scripts/lint-style.py

Created scripts/nolints-style.txt