feat: rewrite the linter for the string ' ;' in Lean

Author: grunweg

Mathlib/Tactic/Linter/TextBased.lean

@@ -58,6 +58,8 @@ inductive StyleError where
   | windowsLineEnding
   /-- A line contains trailing whitespace. -/
   | trailingWhitespace
+  /-- A line contains the string " ;" -/
+  | semicolon
 deriving BEq
 
 /-- How to format style errors -/
@@ -79,6 +81,7 @@ def StyleError.errorMessage (err : StyleError) : String := match err with
   | 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;
@@ -87,6 +90,7 @@ 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. -/
@@ -164,6 +168,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_SEM" => some (StyleError.semicolon)
         | "ERR_TWS" => some (StyleError.trailingWhitespace)
         | "ERR_WIN" => some (StyleError.windowsLineEnding)
         | _ => none
@@ -219,6 +224,22 @@ def trailingWhitespaceLinter : TextbasedLinter := fun lines ↦ Id.run do
   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 (· == ';')
+    if pos != line.endPos && line.get (line.prev pos) == ' ' then
+      let indent := line.length - line.trimLeft.length
+      let replaced := (line.trimLeft.replace " ;" "; ").replace "  " " "
+      errors := errors.push (StyleError.semicolon, idx + 1)
+      -- Concatenate "indent" spaces... better ways to do so welcome!
+      let space := "".intercalate (List.replicate indent " ")
+      fixedLines := fixedLines.set! idx s!"{space}{replaced}"
+   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 :=
@@ -230,7 +251,7 @@ end
 
 /-- All text-based linters registered in this file. -/
 def allLinters : Array TextbasedLinter := #[
-    adaptationNoteLinter, trailingWhitespaceLinter
+    adaptationNoteLinter, semicolonLinter, trailingWhitespaceLinter
   ]
 
 

scripts/lint-style.py

@@ -38,7 +38,6 @@
 
 ERR_IBY = 11 # isolated by
 ERR_IWH = 22 # isolated where
-ERR_SEM = 13 # the substring " ;"
 ERR_CLN = 16 # line starts with a colon
 ERR_IND = 17 # second line not correctly indented
 ERR_ARR = 18 # space after "←"
@@ -197,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))
@@ -236,8 +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_CLN:
             output_message(path, line_nr, "ERR_CLN", "Put : and := before line breaks, not after")
         if errno == ERR_IND:

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