feat: rewrite the trailing whitespace linter in Lean (#16334)

Co-authored-by: Michael Rothgang <[email protected]>

Mathlib/Tactic/Linter/TextBased.lean

@@ -56,6 +56,8 @@ inductive StyleError where
   | adaptationNote
   /-- A line ends with windows line endings (\r\n) instead of unix ones (\n). -/
   | windowsLineEnding
+  /-- A line contains trailing whitespace. -/
+  | trailingWhitespace
 deriving BEq
 
 /-- How to format style errors -/
@@ -76,13 +78,15 @@ def StyleError.errorMessage (err : StyleError) : String := match err with
     "Found the string \"Adaptation note:\", please use the #adaptation_note command instead"
   | windowsLineEnding => "This line ends with a windows line ending (\r\n): please use Unix line\
     endings (\n) instead"
+  | trailingWhitespace => "This line ends with some whitespace: please remove this"
 
 /-- The error code for a given style error. Keep this in sync with `parse?_errorContext` below! -/
 -- FUTURE: we're matching the old codes in `lint-style.py` for compatibility;
 -- in principle, we could also print something more readable.
 def StyleError.errorCode (err : StyleError) : String := match err with
   | StyleError.adaptationNote => "ERR_ADN"
   | StyleError.windowsLineEnding => "ERR_WIN"
+  | StyleError.trailingWhitespace => "ERR_TWS"
 
 /-- Context for a style error: the actual error, the line number in the file we're reading
 and the path to the file. -/
@@ -160,6 +164,7 @@ def parse?_errorContext (line : String) : Option ErrorContext := Id.run do
         -- Use default values for parameters which are ignored for comparing style exceptions.
         -- NB: keep this in sync with `compare` above!
         | "ERR_ADN" => some (StyleError.adaptationNote)
+        | "ERR_TWS" => some (StyleError.trailingWhitespace)
         | "ERR_WIN" => some (StyleError.windowsLineEnding)
         | _ => none
       match String.toNat? lineNumber with
@@ -196,14 +201,24 @@ section
 /-- Lint on any occurrences of the string "Adaptation note:" or variants thereof. -/
 def adaptationNoteLinter : TextbasedLinter := fun lines ↦ Id.run do
   let mut errors := Array.mkEmpty 0
-  let mut lineNumber := 1
-  for line in lines do
+  for (line, idx) in lines.zipWithIndex do
     -- We make this shorter to catch "Adaptation note", "adaptation note" and a missing colon.
     if line.containsSubstr "daptation note" then
-      errors := errors.push (StyleError.adaptationNote, lineNumber)
-    lineNumber := lineNumber + 1
+      errors := errors.push (StyleError.adaptationNote, idx + 1)
   return (errors, none)
 
+
+/-- Lint a collection of input strings if one of them contains trailing whitespace. -/
+def trailingWhitespaceLinter : TextbasedLinter := fun lines ↦ Id.run do
+  let mut errors := Array.mkEmpty 0
+  let mut fixedLines := lines
+  for (line, idx) in lines.zipWithIndex do
+    if line.back == ' ' then
+      errors := errors.push (StyleError.trailingWhitespace, idx + 1)
+      fixedLines := fixedLines.set! idx line.trimRight
+  return (errors, if errors.size > 0 then some fixedLines else none)
+
+
 /-- Whether a collection of lines consists *only* of imports, blank lines and single-line comments.
 In practice, this means it's an imports-only file and exempt from almost all linting. -/
 def isImportsOnlyFile (lines : Array String) : Bool :=
@@ -215,7 +230,7 @@ end
 
 /-- All text-based linters registered in this file. -/
 def allLinters : Array TextbasedLinter := #[
-    adaptationNoteLinter
+    adaptationNoteLinter, trailingWhitespaceLinter
   ]
 
 
@@ -257,7 +272,6 @@ def lintFile (path : FilePath) (exceptions : Array ErrorContext) :
     (allOutput.flatten.filter (fun e ↦ (e.find?_comparable exceptions).isNone))
   return (errors, if changes_made then some changed else none)
 
-
 /-- Lint a collection of modules for style violations.
 Print formatted errors for all unexpected style violations to standard output;
 correct automatically fixable style errors if configured so.

scripts/lint-style.py

@@ -39,7 +39,6 @@
 ERR_IBY = 11 # isolated by
 ERR_IWH = 22 # isolated where
 ERR_SEM = 13 # the substring " ;"
-ERR_TWS = 15 # trailing whitespace
 ERR_CLN = 16 # line starts with a colon
 ERR_IND = 17 # second line not correctly indented
 ERR_ARR = 18 # space after "←"
@@ -107,15 +106,6 @@ def annotate_strings(enumerate_lines):
                 continue
         yield line_nr, line, *rem, False
 
-def line_endings_check(lines, path):
-    errors = []
-    newlines = []
-    for line_nr, line in lines:
-        if line.endswith(" \n"):
-            errors += [(ERR_TWS, line_nr, path)]
-            line = line.rstrip() + "\n"
-        newlines.append((line_nr, line))
-    return errors, newlines
 
 def four_spaces_in_second_line(lines, path):
     # TODO: also fix the space for all lines before ":=", right now we only fix the line after
@@ -248,8 +238,6 @@ def format_errors(errors):
             output_message(path, line_nr, "ERR_IWH", "Line is an isolated where")
         if errno == ERR_SEM:
             output_message(path, line_nr, "ERR_SEM", "Line contains a space before a semicolon")
-        if errno == ERR_TWS:
-            output_message(path, line_nr, "ERR_TWS", "Trailing whitespace detected on line")
         if errno == ERR_CLN:
             output_message(path, line_nr, "ERR_CLN", "Put : and := before line breaks, not after")
         if errno == ERR_IND:
@@ -267,8 +255,7 @@ def lint(path, fix=False):
         lines = f.readlines()
         enum_lines = enumerate(lines, 1)
         newlines = enum_lines
-        for error_check in [line_endings_check,
-                            four_spaces_in_second_line,
+        for error_check in [four_spaces_in_second_line,
                             isolated_by_dot_semicolon_check,
                             left_arrow_check,
                             nonterminal_simp_check]: