Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

refactor(lint-style): make sure to read the nolints file outside of t… #19384

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
+13 −6
Open

refactor(lint-style): make sure to read the nolints file outside of t… #19384

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 4 additions & 5 deletions Mathlib/Tactic/Linter/TextBased.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -262,14 +262,13 @@ def lintFile (path : FilePath) (exceptions : Array ErrorContext) :
Print formatted errors for all unexpected style violations to standard output;
correct automatically fixable style errors if configured so.
Return the number of files which had new style errors.
`moduleNames` are all the modules to lint,
`nolints` is a list of style exceptions to take into account.
`moduleNames` are the names of all the modules to lint,
`mode` specifies what kind of output this script should produce,
`fix` configures whether fixable errors should be corrected in-place. -/
def lintModules (moduleNames : Array Lean.Name) (style : ErrorFormat) (fix : Bool) : IO UInt32 := do
-- Read the `nolints` file, with manual exceptions for the linter.
let nolints ← IO.FS.lines ("scripts" / "nolints-style.txt")
def lintModules (nolints: Array String) (moduleNames : Array Lean.Name) (style : ErrorFormat)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
def lintModules (nolints: Array String) (moduleNames : Array Lean.Name) (style : ErrorFormat)
def lintModules (nolints : Array String) (moduleNames : Array Lean.Name) (style : ErrorFormat)

(fix : Bool) : IO UInt32 := do
let styleExceptions := parseStyleExceptions nolints

let mut numberErrorFiles : UInt32 := 0
let mut allUnexpectedErrors := #[]
for module in moduleNames do
Expand Down
10 changes: 9 additions & 1 deletion scripts/lint-style.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -109,7 +109,15 @@ def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do
allModuleNames := allModuleNames.append (← findImports s)
-- Note: since "Batteries" is added explicitly to "Mathlib.lean", we remove it here manually.
allModuleNames := allModuleNames.erase `Batteries
let mut numberErrors ← lintModules allModuleNames style fix

-- Read the `nolints` file, with manual exceptions for the linter.
-- NB. We pass these lints to `lintModules` explicitly to prevent cache invalidation bugs:
-- if the text-based linter read the file itself, replaying a cached build of that
-- file could re-use an outdated version of the nolints file.
-- (For syntax linters, such a bug actually occurred in mathlib.)
-- This script is re-run each time, hence is immune to such issues.
let nolints ← IO.FS.lines ("scripts" / "nolints-style.txt")
let mut numberErrors ← lintModules nolints allModuleNames style fix
if ← checkInitImports then numberErrors := numberErrors + 1
if !(← allScriptsDocumented) then numberErrors := numberErrors + 1
-- If run with the `--fix` argument, return a zero exit code.
Expand Down
Loading