diff --git a/Batteries.lean b/Batteries.lean index f04a7a1f76..0a35e9f6f4 100644 --- a/Batteries.lean +++ b/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 diff --git a/Batteries/Linter.lean b/Batteries/Linter.lean index 8e72b689cb..cc42f679ca 100644 --- a/Batteries/Linter.lean +++ b/Batteries/Linter.lean @@ -1,2 +1,3 @@ +import Batteries.Linter.TrailingWhitespace import Batteries.Linter.UnreachableTactic import Batteries.Linter.UnnecessarySeqFocus diff --git a/Batteries/Linter/TrailingWhitespace.lean b/Batteries/Linter/TrailingWhitespace.lean new file mode 100644 index 0000000000..3312694a5b --- /dev/null +++ b/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 diff --git a/test/TrailingWhitespace.lean b/test/TrailingWhitespace.lean new file mode 100644 index 0000000000..660ff18140 --- /dev/null +++ b/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 \ No newline at end of file