From 234e24bcc398e64a75656c7a6f3f74ce1b71a05f Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 16 Aug 2024 06:17:35 +0200 Subject: [PATCH 1/4] feat: the trailingWhitespace linter --- Batteries/Linter.lean | 1 + Batteries/Linter/TrailingWhitespace.lean | 50 ++++++++++++++++++++++++ 2 files changed, 51 insertions(+) create mode 100644 Batteries/Linter/TrailingWhitespace.lean 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..a0a861cefb --- /dev/null +++ b/Batteries/Linter/TrailingWhitespace.lean @@ -0,0 +1,50 @@ +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 Mathlib.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 := true + descr := "enable the trailingWhitespace linter" +} + +namespace TrailingWhitespace + +@[inherit_doc Mathlib.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 + let srg := stx.getRange?.getD default + let fm ← getFileMap + for lb in fm.positions do + if srg.contains lb then + 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." + unless Parser.isTerminalCommand stx do return + 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 Mathlib.Linter From ec18d1b1093547778ba93aa68dac01b8ac9e9349 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 16 Aug 2024 06:25:06 +0200 Subject: [PATCH 2/4] lint --- Batteries.lean | 1 + Batteries/Linter/TrailingWhitespace.lean | 8 ++++---- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/Batteries.lean b/Batteries.lean index 8e1e6f1828..a08d17319b 100644 --- a/Batteries.lean +++ b/Batteries.lean @@ -68,6 +68,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/TrailingWhitespace.lean b/Batteries/Linter/TrailingWhitespace.lean index a0a861cefb..688a45c136 100644 --- a/Batteries/Linter/TrailingWhitespace.lean +++ b/Batteries/Linter/TrailingWhitespace.lean @@ -10,7 +10,7 @@ does not end with a line break. open Lean Elab -namespace Mathlib.Linter +namespace Batteries.Linter /-- The "trailingWhitespace" linter emits a warning whenever a line ends with a space or a file @@ -23,8 +23,8 @@ register_option linter.trailingWhitespace : Bool := { namespace TrailingWhitespace -@[inherit_doc Mathlib.Linter.linter.trailingWhitespace] -def trailingWhitespaceLinter : Linter where run := withSetOptionIn fun stx ↦ do +@[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 @@ -47,4 +47,4 @@ initialize addLinter trailingWhitespaceLinter end TrailingWhitespace -end Mathlib.Linter +end Batteries.Linter From d2931f9623f90fe934fdacbae650914c8cc81ad1 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 16 Aug 2024 06:50:27 +0200 Subject: [PATCH 3/4] add test file --- Batteries/Linter/TrailingWhitespace.lean | 4 +--- test/TrailingWhitespace.lean | 18 ++++++++++++++++++ 2 files changed, 19 insertions(+), 3 deletions(-) create mode 100644 test/TrailingWhitespace.lean diff --git a/Batteries/Linter/TrailingWhitespace.lean b/Batteries/Linter/TrailingWhitespace.lean index 688a45c136..f346ed78e7 100644 --- a/Batteries/Linter/TrailingWhitespace.lean +++ b/Batteries/Linter/TrailingWhitespace.lean @@ -29,15 +29,13 @@ def trailingWhitespaceLinter : Linter where run := withSetOptionIn fun stx => do return if (← get).messages.hasErrors then return - let srg := stx.getRange?.getD default + unless Parser.isTerminalCommand stx do return let fm ← getFileMap for lb in fm.positions do - if srg.contains lb then 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." - unless Parser.isTerminalCommand stx do return let (backBack, back) := (fm.positions.pop.back, fm.positions.back) let rg : String.Range := ⟨back - ⟨1⟩, back⟩ if backBack != back then 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 From 452d37b79bdbad821591b3552b22cd2784b65854 Mon Sep 17 00:00:00 2001 From: damiano Date: Wed, 2 Oct 2024 18:45:05 +0200 Subject: [PATCH 4/4] Update Batteries/Linter/TrailingWhitespace.lean --- Batteries/Linter/TrailingWhitespace.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Batteries/Linter/TrailingWhitespace.lean b/Batteries/Linter/TrailingWhitespace.lean index f346ed78e7..3312694a5b 100644 --- a/Batteries/Linter/TrailingWhitespace.lean +++ b/Batteries/Linter/TrailingWhitespace.lean @@ -17,7 +17,7 @@ The "trailingWhitespace" linter emits a warning whenever a line ends with a spac does not end with a line break. -/ register_option linter.trailingWhitespace : Bool := { - defValue := true + defValue := false descr := "enable the trailingWhitespace linter" }