From 3ee9ab855e58a3d0bbe2477bce8367765ec8e93e Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 5 Aug 2022 18:10:05 +0200
Subject: [PATCH] fix: logging of linter warnings

---
 src/Lean/Linter/Builtin.lean                | 6 ++----
 src/Lean/Linter/MissingDocs.lean            | 2 +-
 src/Lean/Linter/UnusedVariables.lean        | 5 ++---
 src/Lean/Linter/Util.lean                   | 8 ++------
 tests/lean/warningAsError.lean              | 3 +++
 tests/lean/warningAsError.lean.expected.out | 1 +
 6 files changed, 11 insertions(+), 14 deletions(-)

diff --git a/src/Lean/Linter/Builtin.lean b/src/Lean/Linter/Builtin.lean
index 1c433c4a96..e1f10a05cf 100644
--- a/src/Lean/Linter/Builtin.lean
+++ b/src/Lean/Linter/Builtin.lean
@@ -25,10 +25,8 @@ def suspiciousUnexpanderPatterns : Linter := fun cmdStx => do
       | `(`($patHead:ident))         => pure patHead
       | _                            => continue
 
-    if let some range := patHead.raw.getRange? then
-      publishMessage
-        "Unexpanders should match the function name against an antiquotation `$_` so as to be independent of the specific pretty printing of the name. [linter.suspiciousUnexpanderPatterns]"
-        range
+    logLint linter.suspiciousUnexpanderPatterns patHead
+      "Unexpanders should match the function name against an antiquotation `$_` so as to be independent of the specific pretty printing of the name."
 
 builtin_initialize addLinter suspiciousUnexpanderPatterns
 
diff --git a/src/Lean/Linter/MissingDocs.lean b/src/Lean/Linter/MissingDocs.lean
index 76e58c11d4..19baec793a 100644
--- a/src/Lean/Linter/MissingDocs.lean
+++ b/src/Lean/Linter/MissingDocs.lean
@@ -99,7 +99,7 @@ builtin_initialize
   mkAttr false `missingDocsHandler
 
 def lint (stx : Syntax) (msg : String) : CommandElabM Unit :=
-  logWarningAt stx s!"missing doc string for {msg} [linter.missingDocs]"
+  logLint linter.missingDocs stx m!"missing doc string for {msg}"
 
 def lintNamed (stx : Syntax) (msg : String) : CommandElabM Unit :=
   lint stx s!"{msg} {stx.getId}"
diff --git a/src/Lean/Linter/UnusedVariables.lean b/src/Lean/Linter/UnusedVariables.lean
index 4bc2886eda..cec35d72bd 100644
--- a/src/Lean/Linter/UnusedVariables.lean
+++ b/src/Lean/Linter/UnusedVariables.lean
@@ -235,8 +235,7 @@ def unusedVariables : Linter := fun cmdStx => do
       continue
 
     -- publish warning if variable is unused and not ignored
-    publishMessage (.tagged decl_name%
-      m!"unused variable `{localDecl.userName}` [linter.unusedVariables]") range
+    logLint linter.unusedVariables declStx m!"unused variable `{localDecl.userName}`"
 
   return ()
 where
@@ -256,4 +255,4 @@ builtin_initialize addLinter unusedVariables
 end Linter
 
 def MessageData.isUnusedVariableWarning (msg : MessageData) : Bool :=
-  msg.hasTag (· == ``Linter.unusedVariables)
+  msg.hasTag (· == Linter.linter.unusedVariables.name)
diff --git a/src/Lean/Linter/Util.lean b/src/Lean/Linter/Util.lean
index a8d9f09c8b..e38e54ddbc 100644
--- a/src/Lean/Linter/Util.lean
+++ b/src/Lean/Linter/Util.lean
@@ -15,12 +15,8 @@ def getLinterValue (opt : Lean.Option Bool) (o : Options) : Bool := o.get opt.na
 
 open Lean.Elab Lean.Elab.Command
 
-def publishMessage
-  (content : MessageData) (range : String.Range) (severity : MessageSeverity := .warning) : CommandElabM Unit :=
-do
-  let ctx := (← read)
-  let messages := (← get).messages |>.add (mkMessageCore ctx.fileName ctx.fileMap content severity range.start range.stop)
-  modify ({ · with messages := messages })
+def logLint (linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) : CommandElabM Unit :=
+  logWarningAt stx (.tagged linterOption.name m!"{msg} [{linterOption.name}]")
 
 /-- Go upwards through the given `tree` starting from the smallest node that
 contains the given `range` and collect all `MacroExpansionInfo`s on the way up.
diff --git a/tests/lean/warningAsError.lean b/tests/lean/warningAsError.lean
index f612f4fa12..cd35d1f688 100644
--- a/tests/lean/warningAsError.lean
+++ b/tests/lean/warningAsError.lean
@@ -8,3 +8,6 @@ def g (x : Nat) := x + 1
 set_option warningAsError true
 
 #eval g 0 -- error
+
+set_option linter.unusedVariables true
+def h (unused : Nat) := 0  -- error
diff --git a/tests/lean/warningAsError.lean.expected.out b/tests/lean/warningAsError.lean.expected.out
index 9f30e68807..aba481ace9 100644
--- a/tests/lean/warningAsError.lean.expected.out
+++ b/tests/lean/warningAsError.lean.expected.out
@@ -2,3 +2,4 @@ warningAsError.lean:6:6-6:7: warning: `g` has been deprecated, use `f` instead
 1
 warningAsError.lean:10:6-10:7: error: `g` has been deprecated, use `f` instead
 1
+warningAsError.lean:13:7-13:13: error: unused variable `unused` [linter.unusedVariables]