feat: rewrite the linter for spaces before semicolons in Lean

Mathlib/Tactic/Linter/TextBased.lean

@@ -56,6 +56,10 @@ 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
+  /-- A line contains the string " ;" -/
+  | semicolon
 deriving BEq
 
 /-- How to format style errors -/
@@ -76,13 +80,17 @@ 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"
+  | semicolon => "This line contains a space before a semicolon"
 
 /-- 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"
+  | StyleError.semicolon => "ERR_SEM"
 
 /-- 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 +168,8 @@ 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_SEM" => some (StyleError.semicolon)
+        | "ERR_TWS" => some (StyleError.trailingWhitespace)
         | "ERR_WIN" => some (StyleError.windowsLineEnding)
         | _ => none
       match String.toNat? lineNumber with
@@ -196,14 +206,37 @@ 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)
+
+
+/-- Lint a collection of input strings for the substring " ;". -/
+def semicolonLinter : TextbasedLinter := fun lines ↦ Id.run do
+  let mut errors := Array.mkEmpty 0
+  let mut fixedLines := lines
+  for (line, idx) in lines.zipWithIndex do
+    let pos := line.find (· == ';')
+    -- Future: also lint for a semicolon *not* followed by a space or ⟩.
+    if pos != line.endPos && line.get (line.prev pos) == ' ' then
+      errors := errors.push (StyleError.semicolon, idx + 1)
+      fixedLines := fixedLines.set! idx (line.replace " ;" ";")
+   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 +248,7 @@ end
 
 /-- All text-based linters registered in this file. -/
 def allLinters : Array TextbasedLinter := #[
-    adaptationNoteLinter
+    adaptationNoteLinter, semicolonLinter, trailingWhitespaceLinter
   ]
 
 
@@ -257,7 +290,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

@@ -38,8 +38,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 +105,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
@@ -207,9 +196,6 @@ def isolated_by_dot_semicolon_check(lines, path):
                     line = f"{indent}{line.lstrip()[3:]}"
         elif line.lstrip() == "where":
             errors += [(ERR_IWH, line_nr, path)]
-        if " ;" in line:
-            errors += [(ERR_SEM, line_nr, path)]
-            line = line.replace(" ;", ";")
         if line.lstrip().startswith(":"):
             errors += [(ERR_CLN, line_nr, path)]
         newlines.append((line_nr, line))
@@ -246,10 +232,6 @@ def format_errors(errors):
             output_message(path, line_nr, "ERR_IBY", "Line is an isolated 'by'")
         if errno == ERR_IWH:
             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 +249,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]:

scripts/nolints-style.txt

@@ -15,3 +15,8 @@ Mathlib/Tactic/Linter/TextBased.lean : line 84 : ERR_ADN : Found the string "Ada
 Mathlib/Tactic/Linter/TextBased.lean : line 274 : ERR_ADN : Found the string "Adaptation note:", please use the #adaptation_note command instead
 Mathlib/Tactic/Linter/TextBased.lean : line 279 : ERR_ADN : Found the string "Adaptation note:", please use the #adaptation_note command instead
 Mathlib/Tactic/Linter/TextBased.lean : line 280 : ERR_ADN : Found the string "Adaptation note:", please use the #adaptation_note command instead
+
+-- The linter for the substring " ;" fires on its own implementation.
+Mathlib/Tactic/Linter/TextBased.lean : line 69 : ERR_SEM : This line contains a space before a semicolon
+Mathlib/Tactic/Linter/TextBased.lean : line 336 : ERR_SEM : This line contains a space before a semicolon
+Mathlib/Tactic/Linter/TextBased.lean : line 345 : ERR_SEM : This line contains a space before a semicolon