From d11b81ce41772bde20959d4da89c91dc6dfce30f Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgami@math.hu-berlin.de>
Date: Sun, 1 Sep 2024 21:03:16 +0200
Subject: [PATCH] wip: rewrite semicolon linter also. TODO perf-test, see if I
 need to speed up...

---
 Mathlib/Tactic/Linter/TextBased.lean | 18 +++++++++++++++++-
 scripts/lint-style.py                |  6 ------
 2 files changed, 17 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Tactic/Linter/TextBased.lean b/Mathlib/Tactic/Linter/TextBased.lean
index f3769f82824de0..a6e5474b1e139d 100644
--- a/Mathlib/Tactic/Linter/TextBased.lean
+++ b/Mathlib/Tactic/Linter/TextBased.lean
@@ -323,13 +323,29 @@ def broadImportsLinter : TextbasedLinter := fun lines ↦ Id.run do
 def trailingWhitespaceLinter : TextbasedLinter := fun lines ↦ Id.run do
   let mut errors := Array.mkEmpty 0
   let mut fixedLines := lines
-  for i in [0::lines.size -1] do
+  for i in [0::lines.size - 1] do
     let line := lines[i]
     if line.back == ' ' then
       errors := errors.push (StyleError.trailingWhitespace, i + 1)
       fixedLines := fixedLines.set! 0 (line.dropRightWhile (· == ' '))
   return (errors, fixedLines)
+-- xxx: can I avoid set!, as I know the index is inbounds? is there a better way?
+-- ask on zulip for the most idiomatic construct
 
+-- TODO: apply the same change to all other linters, once this has been tested...
+
+def semicolonLinter : TextbaseLinter := fun lines ↦ Id.run do
+  let mut errors := Array.mkEmpty 0
+  let mut fixedLines := lines
+  for i in [0::lines.size - 1] do
+    let line := lines[i]
+    if line.contains ';' then
+      let replaced := (line.replace " ;" "; ").replace "  " " "
+      if replaced != line then
+        errors := errors.push (StyleError.semicolon, i + 1) -- TODO: add error variant etc!
+        -- "Line contains a space before a semicolon"
+        fixedLines := fixedLines.set! 0 replaced
+  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. -/
diff --git a/scripts/lint-style.py b/scripts/lint-style.py
index 6f43a2765a8c0a..bd47d4fff21d89 100755
--- a/scripts/lint-style.py
+++ b/scripts/lint-style.py
@@ -38,7 +38,6 @@
 ERR_MOD = 2 # module docstring
 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 "←"
@@ -231,9 +230,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))
@@ -272,8 +268,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: