From 31afbee87398ec9d4d672f236672c8380c169949 Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgami@math.hu-berlin.de>
Date: Fri, 30 Aug 2024 23:26:31 +0200
Subject: [PATCH 01/13] feat: rewrite the windows line endings linter

---
 Mathlib/Tactic/Linter/TextBased.lean | 18 +++++++++++++++++-
 1 file changed, 17 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Tactic/Linter/TextBased.lean b/Mathlib/Tactic/Linter/TextBased.lean
index a6accb1135fd0..9cbc32f07d13d 100644
--- a/Mathlib/Tactic/Linter/TextBased.lean
+++ b/Mathlib/Tactic/Linter/TextBased.lean
@@ -69,6 +69,8 @@ inductive StyleError where
   The `longFile` linter implements the line-length check as a syntax linter.
   This text-based check is present to ensure the limit on files that do not import the linter. -/
   | fileTooLong (numberLines : ℕ) (newSizeLimit : ℕ) (previousLimit : Option ℕ) : StyleError
+  /-- A line ends with windows line endings (\r\n) instead of unix ones (\n). -/
+  | windowsLineEnding
 deriving BEq
 
 /-- How to format style errors -/
@@ -107,6 +109,8 @@ def StyleError.errorMessage (err : StyleError) (style : ErrorFormat) : String :=
     | ErrorFormat.exceptionsFile =>
         s!"{sizeLimit} file contains {currentSize} lines, try to split it up"
     | 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"
 
 /-- 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;
@@ -117,6 +121,7 @@ def StyleError.errorCode (err : StyleError) : String := match err with
   | StyleError.adaptationNote => "ERR_ADN"
   | StyleError.broadImport _ => "ERR_IMP"
   | StyleError.fileTooLong _ _ _ => "ERR_NUM_LIN"
+  | StyleError.windowsLineEnding => "ERR_WIN"
 
 /-- Context for a style error: the actual error, the line number in the file we're reading
 and the path to the file. -/
@@ -211,6 +216,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_WIN" => some (StyleError.windowsLineEnding)
         | "ERR_IMP" =>
           -- XXX tweak exceptions messages to ease parsing?
           if (errorMessage.get! 0).containsSubstr "tactic" then
@@ -341,6 +347,16 @@ def broadImportsLinter : TextbasedLinter := fun lines ↦ Id.run do
   return errors
 
 
+/-- Lint a collection of input strings if one of them contains windows line endings. -/
+def windowsLineEndingLinter : TextbasedLinter := fun lines ↦ Id.run do
+  let mut errors := Array.mkEmpty 0
+  let mut lineNumber := 0
+  for line in lines do
+    let rep := line.crlfToLf
+    if rep != line then
+      errors := errors.push (StyleError.windowsLineEnding, lineNumber)
+  return errors
+
 /-- 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 :=
@@ -373,7 +389,7 @@ end
 
 /-- All text-based linters registered in this file. -/
 def allLinters : Array TextbasedLinter := #[
-    copyrightHeaderLinter, adaptationNoteLinter, broadImportsLinter
+    copyrightHeaderLinter, adaptationNoteLinter, broadImportsLinter, windowsLineEndingLinter
   ]
 
 /-- Controls what kind of output this programme produces. -/

From 59ea5e90fca248e27aae457cdef0ec9b773bdeb4 Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgami@math.hu-berlin.de>
Date: Fri, 30 Aug 2024 23:29:27 +0200
Subject: [PATCH 02/13] chore: make text-based linters return the fixed lines,
 if any

---
 Mathlib/Tactic/Linter/TextBased.lean | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Tactic/Linter/TextBased.lean b/Mathlib/Tactic/Linter/TextBased.lean
index 9cbc32f07d13d..9487bbc82dbd9 100644
--- a/Mathlib/Tactic/Linter/TextBased.lean
+++ b/Mathlib/Tactic/Linter/TextBased.lean
@@ -255,8 +255,9 @@ def formatErrors (errors : Array ErrorContext) (style : ErrorFormat) : IO Unit :
     IO.println (outputMessage e style)
 
 /-- Core logic of a text based linter: given a collection of lines,
-return an array of all style errors with line numbers. -/
-abbrev TextbasedLinter := Array String → Array (StyleError × ℕ)
+return an array of all style errors with line numbers and, optionally, an array of lines
+changed to fix the linter automatically. (This is not always possible, but sometimes it is.) -/
+abbrev TextbasedLinter := Array String → Array (StyleError × ℕ) × (Option (Array String))
 
 /-! Definitions of the actual text-based linters. -/
 section
@@ -305,7 +306,7 @@ def copyrightHeaderLinter : TextbasedLinter := fun lines ↦ Id.run do
       -- If it does, we check the authors line is formatted correctly.
       if !isCorrectAuthorsLine line then
         output := output.push (StyleError.authors, 4)
-  return output
+  return (output, none)
 
 /-- Lint on any occurrences of the string "Adaptation note:" or variants thereof. -/
 def adaptationNoteLinter : TextbasedLinter := fun lines ↦ Id.run do
@@ -316,7 +317,7 @@ def adaptationNoteLinter : TextbasedLinter := fun lines ↦ Id.run do
     if line.containsSubstr "daptation note" then
       errors := errors.push (StyleError.adaptationNote, lineNumber)
     lineNumber := lineNumber + 1
-  return errors
+  return (errors, none)
 
 /-- Lint a collection of input strings if one of them contains an unnecessarily broad import. -/
 def broadImportsLinter : TextbasedLinter := fun lines ↦ Id.run do
@@ -344,7 +345,7 @@ def broadImportsLinter : TextbasedLinter := fun lines ↦ Id.run do
             else if name == "Lake" || name.startsWith "Lake." then
               errors := errors.push (StyleError.broadImport BroadImports.Lake, lineNumber)
       lineNumber := lineNumber + 1
-  return errors
+  return (errors, none)
 
 
 /-- Lint a collection of input strings if one of them contains windows line endings. -/
@@ -355,7 +356,7 @@ def windowsLineEndingLinter : TextbasedLinter := fun lines ↦ Id.run do
     let rep := line.crlfToLf
     if rep != line then
       errors := errors.push (StyleError.windowsLineEnding, lineNumber)
-  return errors
+  return (errors, none) -- TODO: add auto-fix!
 
 /-- 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. -/
@@ -416,8 +417,9 @@ def lintFile (path : FilePath) (sizeLimit : Option ℕ) (exceptions : Array Erro
   let mut errors := #[]
   if let some (StyleError.fileTooLong n limit ex) := checkFileLength lines sizeLimit then
     errors := #[ErrorContext.mk (StyleError.fileTooLong n limit ex) 1 path]
+  -- TODO: use auto-fixes if available
   let allOutput := (Array.map (fun lint ↦
-    (Array.map (fun (e, n) ↦ ErrorContext.mk e n path)) (lint lines))) allLinters
+    (Array.map (fun (e, n) ↦ ErrorContext.mk e n path)) (lint lines).1)) allLinters
   -- This list is not sorted: for github, this is fine.
   errors := errors.append
     (allOutput.flatten.filter (fun e ↦ (e.find?_comparable exceptions).isNone))

From f4c14369a685b2ccdd2cb5fd63e8ea4d28532210 Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgami@math.hu-berlin.de>
Date: Fri, 30 Aug 2024 23:33:36 +0200
Subject: [PATCH 03/13] feat: auto-fix line ending warnings

---
 Mathlib/Tactic/Linter/TextBased.lean | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Tactic/Linter/TextBased.lean b/Mathlib/Tactic/Linter/TextBased.lean
index 9487bbc82dbd9..bddc44c4242bd 100644
--- a/Mathlib/Tactic/Linter/TextBased.lean
+++ b/Mathlib/Tactic/Linter/TextBased.lean
@@ -351,12 +351,17 @@ def broadImportsLinter : TextbasedLinter := fun lines ↦ Id.run do
 /-- Lint a collection of input strings if one of them contains windows line endings. -/
 def windowsLineEndingLinter : 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
-    let rep := line.crlfToLf
-    if rep != line then
+    let replaced := line.crlfToLf
+    if replaced != line then
       errors := errors.push (StyleError.windowsLineEnding, lineNumber)
-  return (errors, none) -- TODO: add auto-fix!
+      fixedLines := fixedLines.set! 0 replaced
+    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. -/

From 6436ad3123a53ededc003e14dc953608369f8611 Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgami@math.hu-berlin.de>
Date: Fri, 30 Aug 2024 23:36:34 +0200
Subject: [PATCH 04/13] feat: when the --fix is given, change the linted module
 according to auto-fixes

---
 Mathlib/Tactic/Linter/TextBased.lean | 35 ++++++++++++++++++++--------
 scripts/lint-style.lean              |  4 ++++
 2 files changed, 29 insertions(+), 10 deletions(-)

diff --git a/Mathlib/Tactic/Linter/TextBased.lean b/Mathlib/Tactic/Linter/TextBased.lean
index bddc44c4242bd..34e153fa6d47c 100644
--- a/Mathlib/Tactic/Linter/TextBased.lean
+++ b/Mathlib/Tactic/Linter/TextBased.lean
@@ -410,25 +410,35 @@ inductive OutputSetting : Type
   | update
   deriving BEq
 
-/-- Read a file and apply all text-based linters. Return a list of all unexpected errors.
+/-- Read a file and apply all text-based linters.
+Return a list of all unexpected errors, and optionally automatically fixed lines.
 `sizeLimit` is any pre-existing limit on this file's size.
 `exceptions` are any other style exceptions. -/
 def lintFile (path : FilePath) (sizeLimit : Option ℕ) (exceptions : Array ErrorContext) :
-    IO (Array ErrorContext) := do
+    IO (Array ErrorContext × Option (Array String)) := do
   let lines ← IO.FS.lines path
   -- We don't need to run any checks on imports-only files.
   if isImportsOnlyFile lines then
-    return #[]
+    return (#[], none)
   let mut errors := #[]
   if let some (StyleError.fileTooLong n limit ex) := checkFileLength lines sizeLimit then
     errors := #[ErrorContext.mk (StyleError.fileTooLong n limit ex) 1 path]
-  -- TODO: use auto-fixes if available
-  let allOutput := (Array.map (fun lint ↦
-    (Array.map (fun (e, n) ↦ ErrorContext.mk e n path)) (lint lines).1)) allLinters
+  -- All errors raised in this file.
+  let mut allOutput := #[]
+  -- A working copy of the lines in this file, modified by applying the auto-fixes.
+  let mut changed := lines
+  let mut change_made := false
+  for lint in allLinters do
+    let (err, changes) := lint changed
+    allOutput := allOutput.append (Array.map (fun (e, n) ↦ #[(ErrorContext.mk e n path)]) err)
+    if let some c := changes then
+      changed := c
+      change_made := true
   -- This list is not sorted: for github, this is fine.
   errors := errors.append
     (allOutput.flatten.filter (fun e ↦ (e.find?_comparable exceptions).isNone))
-  return errors
+  return (errors, if change_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;
@@ -457,12 +467,17 @@ def lintModules (moduleNames : Array String) (mode : OutputSetting) (fix : Bool)
       match errctx.error with
       | StyleError.fileTooLong _ limit _ => some limit
       | _ => none)
-    let errors :=
+    let mut errors := #[]
     if let OutputSetting.print _ := mode then
-      ← lintFile path (sizeLimits.get? 0) styleExceptions
+      let (errors', changed) := ← lintFile path (sizeLimits.get? 0) styleExceptions
+      if let some c := changed then
+        if fix then
+          let _ := ← IO.FS.writeFile path ("\n".intercalate c.toList)
+      errors := errors'
     else
       -- In "update" mode, we ignore the exceptions file (and only take `nolints` into account).
-      ← lintFile path none (parseStyleExceptions nolints)
+      let (errors', _) := ← lintFile path none (parseStyleExceptions nolints)
+      errors := errors'
     if errors.size > 0 then
       allUnexpectedErrors := allUnexpectedErrors.append errors
       numberErrorFiles := numberErrorFiles + 1
diff --git a/scripts/lint-style.lean b/scripts/lint-style.lean
index 2db69b6d8db67..6769ded689b15 100644
--- a/scripts/lint-style.lean
+++ b/scripts/lint-style.lean
@@ -22,6 +22,10 @@ def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do
     | (true, _) => OutputSetting.update
     | (false, true) => OutputSetting.print ErrorFormat.github
     | (false, false) => OutputSetting.print ErrorFormat.humanReadable
+  let fix := args.hasFlag "fix"
+  if args.hasFlag "update" && fix then
+    IO.println "The --update and --fix options must be provided separately: please run --fix first."
+    return 1
   -- Read all module names to lint.
   let mut allModules := #[]
   for s in ["Archive.lean", "Counterexamples.lean", "Mathlib.lean"] do

From 2900855954bc60f647ebe2d6473c3644b853820e Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgami@math.hu-berlin.de>
Date: Sat, 31 Aug 2024 00:29:05 +0200
Subject: [PATCH 05/13] chore: remove corresponding Python style linter

---
 scripts/lint-style.py | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/scripts/lint-style.py b/scripts/lint-style.py
index 18bafab6042dd..9e938c21f23fc 100755
--- a/scripts/lint-style.py
+++ b/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_WIN = 14 # Windows line endings "\r\n"
 ERR_TWS = 15 # trailing whitespace
 ERR_CLN = 16 # line starts with a colon
 ERR_IND = 17 # second line not correctly indented
@@ -133,9 +132,6 @@ def line_endings_check(lines, path):
     errors = []
     newlines = []
     for line_nr, line in lines:
-        if "\r\n" in line:
-            errors += [(ERR_WIN, line_nr, path)]
-            line = line.replace("\r\n", "\n")
         if line.endswith(" \n"):
             errors += [(ERR_TWS, line_nr, path)]
             line = line.rstrip() + "\n"
@@ -324,8 +320,6 @@ def format_errors(errors):
             output_message(path, line_nr, "ERR_DOT", "Line is an isolated focusing dot or uses . instead of ·")
         if errno == ERR_SEM:
             output_message(path, line_nr, "ERR_SEM", "Line contains a space before a semicolon")
-        if errno == ERR_WIN:
-            output_message(path, line_nr, "ERR_WIN", "Windows line endings (\\r\\n) detected")
         if errno == ERR_TWS:
             output_message(path, line_nr, "ERR_TWS", "Trailing whitespace detected on line")
         if errno == ERR_CLN:

From 89886208ffc21888191296a6497da5127769dfe0 Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgami@math.hu-berlin.de>
Date: Sun, 1 Sep 2024 20:42:53 +0200
Subject: [PATCH 06/13] fix: actually detect line length thingies

---
 Mathlib/Tactic/Linter/TextBased.lean | 44 +++++++++++++---------------
 1 file changed, 20 insertions(+), 24 deletions(-)

diff --git a/Mathlib/Tactic/Linter/TextBased.lean b/Mathlib/Tactic/Linter/TextBased.lean
index 34e153fa6d47c..67f432dae58dd 100644
--- a/Mathlib/Tactic/Linter/TextBased.lean
+++ b/Mathlib/Tactic/Linter/TextBased.lean
@@ -348,21 +348,6 @@ def broadImportsLinter : TextbasedLinter := fun lines ↦ Id.run do
   return (errors, none)
 
 
-/-- Lint a collection of input strings if one of them contains windows line endings. -/
-def windowsLineEndingLinter : 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
-    let replaced := line.crlfToLf
-    if replaced != line then
-      errors := errors.push (StyleError.windowsLineEnding, lineNumber)
-      fixedLines := fixedLines.set! 0 replaced
-    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 +380,7 @@ end
 
 /-- All text-based linters registered in this file. -/
 def allLinters : Array TextbasedLinter := #[
-    copyrightHeaderLinter, adaptationNoteLinter, broadImportsLinter, windowsLineEndingLinter
+    copyrightHeaderLinter, adaptationNoteLinter, broadImportsLinter
   ]
 
 /-- Controls what kind of output this programme produces. -/
@@ -416,18 +401,29 @@ Return a list of all unexpected errors, and optionally automatically fixed lines
 `exceptions` are any other style exceptions. -/
 def lintFile (path : FilePath) (sizeLimit : Option ℕ) (exceptions : Array ErrorContext) :
     IO (Array ErrorContext × Option (Array String)) := do
-  let lines ← IO.FS.lines path
-  -- We don't need to run any checks on imports-only files.
-  if isImportsOnlyFile lines then
-    return (#[], none)
   let mut errors := #[]
+  -- Whether any changes were made by auto-fixes.
+  let mut changes_made := false
+  -- Check for windows line endings first: as `FS.lines` treats Unix and Windows lines the same,
+  -- we need to analyse the actual file contents.
+  let contents ← IO.FS.readFile path
+  let replaced := contents.crlfToLf
+  if replaced != then
+    changes_made := true
+    errors := errors.push (ErrorContext.mk StyleError.windowsLineEnding 1 path)
+  let lines := replaced.splitOn '\n'
+
+  -- We don't need to run any further checks on imports-only files.
+  if isImportsOnlyFile lines then
+    return (errors, if changes_made then some lines else none)
+
   if let some (StyleError.fileTooLong n limit ex) := checkFileLength lines sizeLimit then
-    errors := #[ErrorContext.mk (StyleError.fileTooLong n limit ex) 1 path]
-  -- All errors raised in this file.
+    errors := errors.push (ErrorContext.mk (StyleError.fileTooLong n limit ex) 1 path)
+  -- All further style errors raised in this file.
   let mut allOutput := #[]
   -- A working copy of the lines in this file, modified by applying the auto-fixes.
   let mut changed := lines
-  let mut change_made := false
+
   for lint in allLinters do
     let (err, changes) := lint changed
     allOutput := allOutput.append (Array.map (fun (e, n) ↦ #[(ErrorContext.mk e n path)]) err)
@@ -437,7 +433,7 @@ def lintFile (path : FilePath) (sizeLimit : Option ℕ) (exceptions : Array Erro
   -- This list is not sorted: for github, this is fine.
   errors := errors.append
     (allOutput.flatten.filter (fun e ↦ (e.find?_comparable exceptions).isNone))
-  return (errors, if change_made then some changed else none)
+  return (errors, if change_mades then some changed else none)
 
 
 /-- Lint a collection of modules for style violations.

From 4fa03af4f5e18f4ed4d41e2a0277cb19ea75f64d Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgami@math.hu-berlin.de>
Date: Mon, 2 Sep 2024 16:56:16 +0200
Subject: [PATCH 07/13] Fix merge

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

diff --git a/Mathlib/Tactic/Linter/TextBased.lean b/Mathlib/Tactic/Linter/TextBased.lean
index 1e89ffbd3441a..dba93a992be0b 100644
--- a/Mathlib/Tactic/Linter/TextBased.lean
+++ b/Mathlib/Tactic/Linter/TextBased.lean
@@ -350,17 +350,15 @@ def lintFile (path : FilePath) (exceptions : Array ErrorContext) :
   -- we need to analyse the actual file contents.
   let contents ← IO.FS.readFile path
   let replaced := contents.crlfToLf
-  if replaced != then
+  if replaced != contents then
     changes_made := true
     errors := errors.push (ErrorContext.mk StyleError.windowsLineEnding 1 path)
-  let lines := replaced.splitOn '\n'
+  let lines := (replaced.splitOn "\n").toArray
 
   -- We don't need to run any further checks on imports-only files.
   if isImportsOnlyFile lines then
     return (errors, if changes_made then some lines else none)
 
-  if let some (StyleError.fileTooLong n limit ex) := checkFileLength lines sizeLimit then
-    errors := errors.push (ErrorContext.mk (StyleError.fileTooLong n limit ex) 1 path)
   -- All further style errors raised in this file.
   let mut allOutput := #[]
   -- A working copy of the lines in this file, modified by applying the auto-fixes.
@@ -371,11 +369,11 @@ def lintFile (path : FilePath) (exceptions : Array ErrorContext) :
     allOutput := allOutput.append (Array.map (fun (e, n) ↦ #[(ErrorContext.mk e n path)]) err)
     if let some c := changes then
       changed := c
-      change_made := true
+      changes_made := true
   -- This list is not sorted: for github, this is fine.
   errors := errors.append
     (allOutput.flatten.filter (fun e ↦ (e.find?_comparable exceptions).isNone))
-  return (errors, if change_mades then some changed else none)
+  return (errors, if changes_made then some changed else none)
 
 
 /-- Lint a collection of modules for style violations.
diff --git a/scripts/lint-style.py b/scripts/lint-style.py
index 5448262c52cbc..4c87286e8acb1 100755
--- a/scripts/lint-style.py
+++ b/scripts/lint-style.py
@@ -60,7 +60,7 @@
         path = ROOT_DIR / filename
         map = {
             "ERR_MOD": ERR_MOD, "ERR_IBY": ERR_IBY, "ERR_IWH": ERR_IWH,
-            "ERR_DOT": ERR_DOT, "ERR_SEM": ERR_SEM, "ERR_WIN": ERR_WIN,
+            "ERR_DOT": ERR_DOT, "ERR_SEM": ERR_SEM,
             "ERR_TWS": ERR_TWS, "ERR_CLN": ERR_CLN, "ERR_IND": ERR_IND,
             "ERR_ARR": ERR_ARR, "ERR_NSP": ERR_NSP,
         }

From 5196b7dbaf141a3e29638117acbff8ddec99133e Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgami@math.hu-berlin.de>
Date: Wed, 4 Sep 2024 10:35:02 +0200
Subject: [PATCH 08/13] Review comments.

---
 Mathlib/Tactic/Linter/TextBased.lean | 6 ++++--
 scripts/lint-style.lean              | 2 +-
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Tactic/Linter/TextBased.lean b/Mathlib/Tactic/Linter/TextBased.lean
index dba93a992be0b..e8e6dab6d07b1 100644
--- a/Mathlib/Tactic/Linter/TextBased.lean
+++ b/Mathlib/Tactic/Linter/TextBased.lean
@@ -219,8 +219,10 @@ def formatErrors (errors : Array ErrorContext) (style : ErrorFormat) : IO Unit :
     IO.println (outputMessage e style)
 
 /-- Core logic of a text based linter: given a collection of lines,
-return an array of all style errors with line numbers and, optionally, an array of lines
-changed to fix the linter automatically. (This is not always possible, but sometimes it is.) -/
+return an array of all style errors with line numbers and, optionally,
+the collection of lines changed to fix the linter errors automatically.
+(Such automatic fixes are only possible for some kinds of `StyleError`s.)
+-/
 abbrev TextbasedLinter := Array String → Array (StyleError × ℕ) × (Option (Array String))
 
 /-! Definitions of the actual text-based linters. -/
diff --git a/scripts/lint-style.lean b/scripts/lint-style.lean
index 6769ded689b15..16b2f02f5e0ad 100644
--- a/scripts/lint-style.lean
+++ b/scripts/lint-style.lean
@@ -32,7 +32,7 @@ def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do
     allModules := allModules.append ((← IO.FS.lines s).map (·.stripPrefix "import "))
   -- note: since we manually add "Batteries" to "Mathlib.lean", we remove it here manually
   allModules := allModules.erase "Batteries"
-  let numberErrorFiles ← lintModules allModules mode (args.hasFlag "fix")
+  let numberErrorFiles ← lintModules allModules mode fix
   -- If run with the `--update` or `--fix` argument, return a zero exit code.
   -- Otherwise, make sure to return an exit code of at most 125,
   -- so this return value can be used further in shell scripts.

From 4524784ab1e010f078b3f4a157bd496c7679fd9c Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgami@math.hu-berlin.de>
Date: Sat, 31 Aug 2024 00:35:08 +0200
Subject: [PATCH 09/13] 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 rewritten as a syntax linter, as a fair number
of mathlib contributors have their text editor configured to remove trailing
whitespace when saving: with such configurations, 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 | 22 +++++++++++++++++++++-
 scripts/lint-style.py                | 15 +--------------
 2 files changed, 22 insertions(+), 15 deletions(-)

diff --git a/Mathlib/Tactic/Linter/TextBased.lean b/Mathlib/Tactic/Linter/TextBased.lean
index 79ab15905126f..6ca95a11cbcb3 100644
--- a/Mathlib/Tactic/Linter/TextBased.lean
+++ b/Mathlib/Tactic/Linter/TextBased.lean
@@ -64,6 +64,8 @@ inductive StyleError where
   | broadImport (module : BroadImports)
   /-- 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 -/
@@ -94,6 +96,7 @@ def StyleError.errorMessage (err : StyleError) : String := match err with
       benchmark it. If this is fine, feel free to allow this linter."
   | 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;
@@ -104,6 +107,7 @@ def StyleError.errorCode (err : StyleError) : String := match err with
   | StyleError.adaptationNote => "ERR_ADN"
   | StyleError.broadImport _ => "ERR_IMP"
   | 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. -/
@@ -189,6 +193,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?
@@ -314,6 +319,21 @@ def broadImportsLinter : TextbasedLinter := fun lines ↦ Id.run do
   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
+  -- 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 :=
@@ -325,7 +345,7 @@ end
 
 /-- All text-based linters registered in this file. -/
 def allLinters : Array TextbasedLinter := #[
-    copyrightHeaderLinter, adaptationNoteLinter, broadImportsLinter
+    copyrightHeaderLinter, adaptationNoteLinter, broadImportsLinter, trailingWhitespaceLinter
   ]
 
 
diff --git a/scripts/lint-style.py b/scripts/lint-style.py
index face057f0f464..6f43a2765a8c0 100755
--- a/scripts/lint-style.py
+++ b/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
@@ -284,8 +274,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:
@@ -303,8 +291,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]:

From 34b6ef3c573d9a41bf7ad07848ba581dc35ce972 Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgami@math.hu-berlin.de>
Date: Sun, 1 Sep 2024 20:58:32 +0200
Subject: [PATCH 10/13] fix line numbers; better iteration over the array

---
 Mathlib/Tactic/Linter/TextBased.lean | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Tactic/Linter/TextBased.lean b/Mathlib/Tactic/Linter/TextBased.lean
index 6ca95a11cbcb3..4d931d1e28f10 100644
--- a/Mathlib/Tactic/Linter/TextBased.lean
+++ b/Mathlib/Tactic/Linter/TextBased.lean
@@ -323,15 +323,12 @@ 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
-  -- 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
+  for h : idx in [:lines.size] do
+    let line := lines[idx]
     if line.back == ' ' then
-      errors := errors.push (StyleError.trailingWhitespace, lineNumber)
-      fixedLines := fixedLines.set! 0 (line.dropRightWhile (· == ' '))
-    lineNumber := lineNumber + 1
-  return (errors, fixedLines)
+      errors := errors.push (StyleError.trailingWhitespace, idx + 1)
+      fixedLines := fixedLines.set! idx (line.dropRightWhile (· == ' '))
+  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.

From 81bfec2e075d228ac6dfbe56c5e2807945b46f87 Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgami@math.hu-berlin.de>
Date: Thu, 5 Sep 2024 16:10:55 +0200
Subject: [PATCH 11/13] Tweaks.

---
 Mathlib/Tactic/Linter/TextBased.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/Mathlib/Tactic/Linter/TextBased.lean b/Mathlib/Tactic/Linter/TextBased.lean
index 4d931d1e28f10..e8cf1b8c0e013 100644
--- a/Mathlib/Tactic/Linter/TextBased.lean
+++ b/Mathlib/Tactic/Linter/TextBased.lean
@@ -318,7 +318,6 @@ def broadImportsLinter : TextbasedLinter := fun lines ↦ Id.run do
       lineNumber := lineNumber + 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
@@ -327,7 +326,7 @@ def trailingWhitespaceLinter : TextbasedLinter := fun lines ↦ Id.run do
     let line := lines[idx]
     if line.back == ' ' then
       errors := errors.push (StyleError.trailingWhitespace, idx + 1)
-      fixedLines := fixedLines.set! idx (line.dropRightWhile (· == ' '))
+      fixedLines := fixedLines.set! idx line.trimRight
   return (errors, if errors.size > 0 then some fixedLines else none)
 
 
@@ -384,7 +383,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.

From 88631511a5a3a8256c9e9db8f316e30250d59943 Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgami@math.hu-berlin.de>
Date: Sat, 7 Sep 2024 10:39:15 +0200
Subject: [PATCH 12/13] Small golf: use Array.zipWithIndex

---
 Mathlib/Tactic/Linter/TextBased.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Tactic/Linter/TextBased.lean b/Mathlib/Tactic/Linter/TextBased.lean
index 90f8e87d8eb45..074e493d4ffaa 100644
--- a/Mathlib/Tactic/Linter/TextBased.lean
+++ b/Mathlib/Tactic/Linter/TextBased.lean
@@ -322,8 +322,7 @@ 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 h : idx in [:lines.size] do
-    let line := lines[idx]
+  for (line, idx) in lines.zipWithIndex do
     if line.back == ' ' then
       errors := errors.push (StyleError.trailingWhitespace, idx + 1)
       fixedLines := fixedLines.set! idx line.trimRight

From cae8fabf420493fddf73236fc19d90f03d9da856 Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgang@math.uni-bonn.de>
Date: Thu, 21 Nov 2024 16:46:17 +0100
Subject: [PATCH 13/13] chore: also use zipWithIndex in the
 adaptationNoteLinter

---
 Mathlib/Tactic/Linter/TextBased.lean | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Tactic/Linter/TextBased.lean b/Mathlib/Tactic/Linter/TextBased.lean
index 2899c4c72779e..aa2c455269b43 100644
--- a/Mathlib/Tactic/Linter/TextBased.lean
+++ b/Mathlib/Tactic/Linter/TextBased.lean
@@ -56,7 +56,7 @@ inductive StyleError where
   | adaptationNote
   /-- A line ends with windows line endings (\r\n) instead of unix ones (\n). -/
   | windowsLineEnding
-  /-- A line contains trailing whitespace -/
+  /-- A line contains trailing whitespace. -/
   | trailingWhitespace
 deriving BEq
 
@@ -201,12 +201,10 @@ 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)