feat: rewrite the trailing whitespace linter in Lean

There is an in-progress PR batteries to the same effect: when that PR
lands, this linter can be removed. Both implement basically the same logic.

This linter is consciously not rewritte as a syntax linter, as a fair number
of mathlib contributors have their editors configured to remove trailing
whitespace when saving: in effect, the linter would only fire intermittently
(such as, between keypresses), which is not helpful.
Running this as a text-based linter in CI, which is auto-fixable, is far
more helpful.

Mathlib/Tactic/Linter/TextBased.lean

@@ -71,6 +71,8 @@ inductive StyleError where
   | fileTooLong (numberLines : ℕ) (newSizeLimit : ℕ) (previousLimit : Option ℕ) : StyleError
   /-- 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 -/
@@ -111,6 +113,7 @@ def StyleError.errorMessage (err : StyleError) (style : ErrorFormat) : String :=
     | ErrorFormat.humanReadable => s!"file contains {currentSize} lines, try to split it up"
   | 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;
@@ -122,6 +125,7 @@ def StyleError.errorCode (err : StyleError) : String := match err with
   | StyleError.broadImport _ => "ERR_IMP"
   | StyleError.fileTooLong _ _ _ => "ERR_NUM_LIN"
   | 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. -/
@@ -216,6 +220,7 @@ def parse?_errorContext (line : String) : Option ErrorContext := Id.run do
         | "ERR_COP" => some (StyleError.copyright none)
         | "ERR_AUT" => some (StyleError.authors)
         | "ERR_ADN" => some (StyleError.adaptationNote)
+        | "ERR_TWS" => some (StyleError.trailingWhitespace)
         | "ERR_WIN" => some (StyleError.windowsLineEnding)
         | "ERR_IMP" =>
           -- XXX tweak exceptions messages to ease parsing?
@@ -363,6 +368,21 @@ def windowsLineEndingLinter : TextbasedLinter := fun lines ↦ Id.run do
     lineNumber := lineNumber + 1
   return (errors, fixedLines)
 
+
+/-- 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
+  -- invariant: this equals the current index of 'line' in 'lines',
+  -- hence starts at 0 and is incremented *at the end* of the loop
+  let mut lineNumber := 0
+  for line in lines do
+    if line.back == ' ' then
+      errors := errors.push (StyleError.trailingWhitespace, lineNumber)
+      fixedLines := fixedLines.set! 0 (line.dropRightWhile (· == ' '))
+    lineNumber := lineNumber + 1
+  return (errors, fixedLines)
+
 /-- 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 :=
@@ -395,7 +415,8 @@ end
 
 /-- All text-based linters registered in this file. -/
 def allLinters : Array TextbasedLinter := #[
-    copyrightHeaderLinter, adaptationNoteLinter, broadImportsLinter, windowsLineEndingLinter
+    copyrightHeaderLinter, adaptationNoteLinter, broadImportsLinter,
+    windowsLineEndingLinter, trailingWhitespaceLinter
   ]
 
 /-- Controls what kind of output this programme produces. -/

scripts/lint-style.py

@@ -42,7 +42,6 @@
 ERR_IWH = 22 # isolated where
 ERR_DOT = 12 # isolated or low focusing dot
 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 "←"
@@ -62,7 +61,7 @@
             exceptions += [(ERR_MOD, path, None)]
         elif errno == "ERR_IND":
             exceptions += [(ERR_IND, path, None)]
-        elif errno in ["ERR_COP", "ERR_LIN", "ERR_ADN", "ERR_NUM_LIN"]:
+        elif errno in ["ERR_COP", "ERR_LIN", "ERR_ADN", "ERR_WIN", "ERR_TWS", "ERR_NUM_LIN"]:
             pass # maintained by the Lean style linter now
         else:
             print(f"Error: unexpected errno in style-exceptions.txt: {errno}")