feat: the trailingWhitespace linter

Batteries.lean

@@ -64,6 +64,7 @@ import Batteries.Lean.System.IO
 import Batteries.Lean.TagAttribute
 import Batteries.Lean.Util.EnvSearch
 import Batteries.Linter
+import Batteries.Linter.TrailingWhitespace
 import Batteries.Linter.UnnecessarySeqFocus
 import Batteries.Linter.UnreachableTactic
 import Batteries.Logic

Batteries/Linter.lean

@@ -1,2 +1,3 @@
+import Batteries.Linter.TrailingWhitespace
 import Batteries.Linter.UnreachableTactic
 import Batteries.Linter.UnnecessarySeqFocus

Batteries/Linter/TrailingWhitespace.lean

@@ -0,0 +1,48 @@
+import Lean.Elab.Command
+import Lean.Linter.Util
+
+/-!
+#  The "trailingWhitespace" linter
+
+The "trailingWhitespace" linter emits a warning whenever a line ends with a space or a file
+does not end with a line break.
+-/
+
+open Lean Elab
+
+namespace Batteries.Linter
+
+/--
+The "trailingWhitespace" linter emits a warning whenever a line ends with a space or a file
+does not end with a line break.
+-/
+register_option linter.trailingWhitespace : Bool := {
+  defValue := false
+  descr := "enable the trailingWhitespace linter"
+}
+
+namespace TrailingWhitespace
+
+@[inherit_doc Batteries.Linter.linter.trailingWhitespace]
+def trailingWhitespaceLinter : Linter where run := withSetOptionIn fun stx => do
+  unless Linter.getLinterValue linter.trailingWhitespace (← getOptions) do
+    return
+  if (← get).messages.hasErrors then
+    return
+  unless Parser.isTerminalCommand stx do return
+  let fm ← getFileMap
+  for lb in fm.positions do
+    let last : Substring := { str := fm.source, startPos := ⟨lb.1 - 2⟩, stopPos := ⟨lb.1 - 1⟩ }
+    if last.toString == " " then
+      Linter.logLint linter.trailingWhitespace (.ofRange ⟨⟨lb.1 - 2⟩, ⟨lb.1 - 1⟩⟩)
+        m!"Lines should not end with a space."
+  let (backBack, back) := (fm.positions.pop.back, fm.positions.back)
+  let rg : String.Range := ⟨back - ⟨1⟩, back⟩
+  if backBack != back then
+    Linter.logLint linter.trailingWhitespace (.ofRange rg) m!"Files should end with a line-break."
+
+initialize addLinter trailingWhitespaceLinter
+
+end TrailingWhitespace
+
+end Batteries.Linter

test/TrailingWhitespace.lean

@@ -0,0 +1,18 @@
+import Batteries.Linter.TrailingWhitespace
+
+set_option linter.trailingWhitespace false
+
+section 
+end
+/--
+warning: using 'exit' to interrupt Lean
+---
+warning: Lines should not end with a space.
+note: this linter can be disabled with `set_option linter.trailingWhitespace false`
+---
+warning: Files should end with a line-break.
+note: this linter can be disabled with `set_option linter.trailingWhitespace false`
+-/
+#guard_msgs in
+set_option linter.trailingWhitespace true in
+#exit