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

…he linter implementation

This way, we categorically prevent cache invalidation bugs caused by lake replaying unchanged inputs, and thus not reaction to changes in the linter exceptions. For *syntax linters*, such a bug actually occurred in mathlib. (With the current implementation of text-based linters, this issue won't occur; this is merely a defensive change.)

Suggested in #19275.



Co-authored-by: Jon Eugster <eugster.jon@gmail.com>

Author: grunweg

Mathlib/Tactic/Linter/TextBased.lean

@@ -276,14 +276,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)
+    (fix : Bool) : IO UInt32 := do
   let styleExceptions := parseStyleExceptions nolints
-
   let mut numberErrorFiles : UInt32 := 0
   let mut allUnexpectedErrors := #[]
   for module in moduleNames do

scripts/lint-style.lean

@@ -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.