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

…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.)

Mathlib/Tactic/Linter/TextBased.lean

@@ -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)
+    (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.