feat: make linter options more explicitly discoverable

src/Lean/Linter/Util.lean

@@ -14,7 +14,8 @@ open Lean.Elab
 
 def logLint [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m]
     (linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) : m Unit :=
-  logWarningAt stx (.tagged linterOption.name m!"{msg} [{linterOption.name}]")
+  let disable := m!"note: this linter can be disabled with `set_option {linterOption.name} false`"
+  logWarningAt stx (.tagged linterOption.name m!"{msg}\n{disable}")
 
 /-- If `linterOption` is true, print a linter warning message at the position determined by `stx`.
 -/

tests/lean/linterMissingDocs.lean.expected.out

@@ -1,37 +1,74 @@
-linterMissingDocs.lean:8:4-8:9: warning: missing doc string for public def noDoc [linter.missingDocs]
-linterMissingDocs.lean:13:14-13:20: warning: missing doc string for public def noDoc2 [linter.missingDocs]
-linterMissingDocs.lean:17:4-17:10: warning: missing doc string for public def openIn [linter.missingDocs]
-linterMissingDocs.lean:24:4-24:16: warning: missing doc string for public def setOptionIn1 [linter.missingDocs]
-linterMissingDocs.lean:39:4-39:11: warning: missing doc string for public def lintDoc [linter.missingDocs]
-linterMissingDocs.lean:41:10-41:13: warning: missing doc string for public inductive Ind [linter.missingDocs]
-linterMissingDocs.lean:42:4-42:8: warning: missing doc string for public constructor Ind.ind1 [linter.missingDocs]
-linterMissingDocs.lean:43:4-43:8: warning: missing doc string for public constructor Ind.ind2 [linter.missingDocs]
-linterMissingDocs.lean:46:20-46:25: warning: missing doc string for computed field Ind.field [linter.missingDocs]
-linterMissingDocs.lean:49:10-49:13: warning: missing doc string for public structure Foo [linter.missingDocs]
-linterMissingDocs.lean:50:2-50:5: warning: missing doc string for public field Foo.mk1 [linter.missingDocs]
-linterMissingDocs.lean:53:3-53:6: warning: missing doc string for public field Foo.mk4 [linter.missingDocs]
-linterMissingDocs.lean:53:7-53:10: warning: missing doc string for public field Foo.mk5 [linter.missingDocs]
-linterMissingDocs.lean:54:3-54:6: warning: missing doc string for public field Foo.mk6 [linter.missingDocs]
-linterMissingDocs.lean:54:7-54:10: warning: missing doc string for public field Foo.mk7 [linter.missingDocs]
-linterMissingDocs.lean:56:6-56:9: warning: missing doc string for public structure Bar [linter.missingDocs]
-linterMissingDocs.lean:57:3-57:6: warning: missing doc string for public field Bar.foo [linter.missingDocs]
-linterMissingDocs.lean:57:7-57:10: warning: missing doc string for public field Bar.bar [linter.missingDocs]
-linterMissingDocs.lean:59:6-59:10: warning: missing doc string for public structure Bar2 [linter.missingDocs]
-linterMissingDocs.lean:60:2-60:5: warning: missing doc string for public field Bar2.bar [linter.missingDocs]
-linterMissingDocs.lean:62:6-62:10: warning: missing doc string for public structure Bar3 [linter.missingDocs]
-linterMissingDocs.lean:64:7-64:10: warning: missing doc string for public field Bar3.baz [linter.missingDocs]
-linterMissingDocs.lean:70:11-70:15: warning: missing doc string for initializer init [linter.missingDocs]
-linterMissingDocs.lean:73:19-73:24: warning: missing doc string for syntax category myCat [linter.missingDocs]
-linterMissingDocs.lean:75:0-75:6: warning: missing doc string for syntax [linter.missingDocs]
-linterMissingDocs.lean:76:16-76:24: warning: missing doc string for syntax namedSyn [linter.missingDocs]
-linterMissingDocs.lean:77:0-77:6: warning: missing doc string for infixl [linter.missingDocs]
-linterMissingDocs.lean:78:19-78:29: warning: missing doc string for infixr namedInfix [linter.missingDocs]
-linterMissingDocs.lean:79:0-79:8: warning: missing doc string for notation [linter.missingDocs]
-linterMissingDocs.lean:80:21-80:30: warning: missing doc string for notation namedNota [linter.missingDocs]
-linterMissingDocs.lean:87:0-87:4: warning: missing doc string for elab [linter.missingDocs]
-linterMissingDocs.lean:88:0-88:5: warning: missing doc string for macro [linter.missingDocs]
-linterMissingDocs.lean:90:13-90:22: warning: missing doc string for class abbrev [anonymous] [linter.missingDocs]
-linterMissingDocs.lean:92:16-92:24: warning: missing doc string for option myOption [linter.missingDocs]
-linterMissingDocs.lean:94:14-94:19: warning: missing doc string for elab myCmd [linter.missingDocs]
-linterMissingDocs.lean:100:4-100:15: warning: missing doc string for public def handleMyCmd [linter.missingDocs]
-linterMissingDocs.lean:107:11-107:12: warning: missing doc string for my_command z [linter.missingDocs]
+linterMissingDocs.lean:8:4-8:9: warning: missing doc string for public def noDoc
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:13:14-13:20: warning: missing doc string for public def noDoc2
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:17:4-17:10: warning: missing doc string for public def openIn
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:24:4-24:16: warning: missing doc string for public def setOptionIn1
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:39:4-39:11: warning: missing doc string for public def lintDoc
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:41:10-41:13: warning: missing doc string for public inductive Ind
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:42:4-42:8: warning: missing doc string for public constructor Ind.ind1
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:43:4-43:8: warning: missing doc string for public constructor Ind.ind2
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:46:20-46:25: warning: missing doc string for computed field Ind.field
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:49:10-49:13: warning: missing doc string for public structure Foo
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:50:2-50:5: warning: missing doc string for public field Foo.mk1
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:53:3-53:6: warning: missing doc string for public field Foo.mk4
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:53:7-53:10: warning: missing doc string for public field Foo.mk5
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:54:3-54:6: warning: missing doc string for public field Foo.mk6
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:54:7-54:10: warning: missing doc string for public field Foo.mk7
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:56:6-56:9: warning: missing doc string for public structure Bar
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:57:3-57:6: warning: missing doc string for public field Bar.foo
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:57:7-57:10: warning: missing doc string for public field Bar.bar
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:59:6-59:10: warning: missing doc string for public structure Bar2
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:60:2-60:5: warning: missing doc string for public field Bar2.bar
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:62:6-62:10: warning: missing doc string for public structure Bar3
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:64:7-64:10: warning: missing doc string for public field Bar3.baz
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:70:11-70:15: warning: missing doc string for initializer init
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:73:19-73:24: warning: missing doc string for syntax category myCat
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:75:0-75:6: warning: missing doc string for syntax
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:76:16-76:24: warning: missing doc string for syntax namedSyn
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:77:0-77:6: warning: missing doc string for infixl
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:78:19-78:29: warning: missing doc string for infixr namedInfix
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:79:0-79:8: warning: missing doc string for notation
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:80:21-80:30: warning: missing doc string for notation namedNota
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:87:0-87:4: warning: missing doc string for elab
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:88:0-88:5: warning: missing doc string for macro
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:90:13-90:22: warning: missing doc string for class abbrev [anonymous]
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:92:16-92:24: warning: missing doc string for option myOption
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:94:14-94:19: warning: missing doc string for elab myCmd
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:100:4-100:15: warning: missing doc string for public def handleMyCmd
+note: this linter can be disabled with `set_option linter.missingDocs false`
+linterMissingDocs.lean:107:11-107:12: warning: missing doc string for my_command z
+note: this linter can be disabled with `set_option linter.missingDocs false`

tests/lean/linterSuspiciousUnexpanderPatterns.lean.expected.out

@@ -1,2 +1,4 @@
-linterSuspiciousUnexpanderPatterns.lean:6:6-6:14: warning: Unexpanders should match the function name against an antiquotation `$_` so as to be independent of the specific pretty printing of the name. [linter.suspiciousUnexpanderPatterns]
-linterSuspiciousUnexpanderPatterns.lean:11:6-11:15: warning: Unexpanders should match the function name against an antiquotation `$_` so as to be independent of the specific pretty printing of the name. [linter.suspiciousUnexpanderPatterns]
+linterSuspiciousUnexpanderPatterns.lean:6:6-6:14: warning: Unexpanders should match the function name against an antiquotation `$_` so as to be independent of the specific pretty printing of the name.
+note: this linter can be disabled with `set_option linter.suspiciousUnexpanderPatterns false`
+linterSuspiciousUnexpanderPatterns.lean:11:6-11:15: warning: Unexpanders should match the function name against an antiquotation `$_` so as to be independent of the specific pretty printing of the name.
+note: this linter can be disabled with `set_option linter.suspiciousUnexpanderPatterns false`

tests/lean/linterUnusedVariables.lean.expected.out

@@ -1,30 +1,57 @@
-linterUnusedVariables.lean:16:21-16:22: warning: unused variable `x` [linter.unusedVariables]
-linterUnusedVariables.lean:17:6-17:7: warning: unused variable `y` [linter.unusedVariables]
-linterUnusedVariables.lean:22:8-22:9: warning: unused variable `x` [linter.unusedVariables]
-linterUnusedVariables.lean:38:5-38:6: warning: unused variable `x` [linter.unusedVariables]
-linterUnusedVariables.lean:43:5-43:6: warning: unused variable `x` [linter.unusedVariables]
-linterUnusedVariables.lean:46:7-46:8: warning: unused variable `x` [linter.unusedVariables]
-linterUnusedVariables.lean:49:8-49:9: warning: unused variable `x` [linter.unusedVariables]
-linterUnusedVariables.lean:53:9-53:10: warning: unused variable `z` [linter.unusedVariables]
-linterUnusedVariables.lean:55:11-55:12: warning: unused variable `z` [linter.unusedVariables]
-linterUnusedVariables.lean:60:14-60:15: warning: unused variable `y` [linter.unusedVariables]
-linterUnusedVariables.lean:66:20-66:21: warning: unused variable `y` [linter.unusedVariables]
-linterUnusedVariables.lean:71:34-71:38: warning: unused variable `inst` [linter.unusedVariables]
-linterUnusedVariables.lean:112:25-112:26: warning: unused variable `x` [linter.unusedVariables]
-linterUnusedVariables.lean:113:6-113:7: warning: unused variable `y` [linter.unusedVariables]
-linterUnusedVariables.lean:119:6-119:7: warning: unused variable `a` [linter.unusedVariables]
-linterUnusedVariables.lean:129:26-129:27: warning: unused variable `z` [linter.unusedVariables]
-linterUnusedVariables.lean:137:9-137:10: warning: unused variable `h` [linter.unusedVariables]
-linterUnusedVariables.lean:151:8-151:9: warning: unused variable `y` [linter.unusedVariables]
-linterUnusedVariables.lean:154:20-154:21: warning: unused variable `β` [linter.unusedVariables]
-linterUnusedVariables.lean:155:7-155:8: warning: unused variable `x` [linter.unusedVariables]
-linterUnusedVariables.lean:165:6-165:7: warning: unused variable `s` [linter.unusedVariables]
-linterUnusedVariables.lean:189:6-189:7: warning: unused variable `y` [linter.unusedVariables]
-linterUnusedVariables.lean:196:19-196:20: warning: unused variable `x` [linter.unusedVariables]
-linterUnusedVariables.lean:200:6-200:7: warning: unused variable `y` [linter.unusedVariables]
-linterUnusedVariables.lean:205:6-205:7: warning: unused variable `y` [linter.unusedVariables]
-linterUnusedVariables.lean:210:6-210:7: warning: unused variable `y` [linter.unusedVariables]
-linterUnusedVariables.lean:219:32-219:33: warning: unused variable `b` [linter.unusedVariables]
+linterUnusedVariables.lean:16:21-16:22: warning: unused variable `x`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:17:6-17:7: warning: unused variable `y`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:22:8-22:9: warning: unused variable `x`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:38:5-38:6: warning: unused variable `x`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:43:5-43:6: warning: unused variable `x`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:46:7-46:8: warning: unused variable `x`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:49:8-49:9: warning: unused variable `x`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:53:9-53:10: warning: unused variable `z`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:55:11-55:12: warning: unused variable `z`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:60:14-60:15: warning: unused variable `y`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:66:20-66:21: warning: unused variable `y`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:71:34-71:38: warning: unused variable `inst`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:112:25-112:26: warning: unused variable `x`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:113:6-113:7: warning: unused variable `y`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:119:6-119:7: warning: unused variable `a`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:129:26-129:27: warning: unused variable `z`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:137:9-137:10: warning: unused variable `h`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:151:8-151:9: warning: unused variable `y`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:154:20-154:21: warning: unused variable `β`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:155:7-155:8: warning: unused variable `x`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:165:6-165:7: warning: unused variable `s`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:189:6-189:7: warning: unused variable `y`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:196:19-196:20: warning: unused variable `x`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:200:6-200:7: warning: unused variable `y`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:205:6-205:7: warning: unused variable `y`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:210:6-210:7: warning: unused variable `y`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:219:32-219:33: warning: unused variable `b`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:236:27-236:28: error: don't know how to synthesize placeholder
 context:
 bar : ?m
@@ -45,6 +72,9 @@ bar' : Nat → Nat
 inst : ToString α
 a : Nat
 ⊢ Nat
-linterUnusedVariables.lean:249:9-249:12: warning: unused variable `ord` [linter.unusedVariables]
-linterUnusedVariables.lean:250:15-250:18: warning: unused variable `ord` [linter.unusedVariables]
-linterUnusedVariables.lean:251:9-251:10: warning: unused variable `h` [linter.unusedVariables]
+linterUnusedVariables.lean:249:9-249:12: warning: unused variable `ord`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:250:15-250:18: warning: unused variable `ord`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+linterUnusedVariables.lean:251:9-251:10: warning: unused variable `h`
+note: this linter can be disabled with `set_option linter.unusedVariables false`

tests/lean/run/ext.lean

@@ -38,7 +38,10 @@ example (f g : Nat × Nat → Nat) : f = g := by
   guard_target = f (x, y) = g (x, y); exact mySorry
 
 -- Check that we generate a warning if there are too many patterns.
-/-- warning: `ext` did not consume the patterns: [j] [linter.unusedRCasesPattern] -/
+/--
+warning: `ext` did not consume the patterns: [j]
+note: this linter can be disabled with `set_option linter.unusedRCasesPattern false`
+-/
 #guard_msgs in
 example (f g : Nat → Nat) (h : f = g) : f = g := by
   ext i j

tests/lean/run/guard_msgs.lean

@@ -136,11 +136,17 @@ Linter suppression
 
 set_option linter.unusedVariables true
 
-/-- warning: unused variable `n` [linter.unusedVariables] -/
+/--
+warning: unused variable `n`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+-/
 #guard_msgs in
 example (n : Nat) : True := trivial
 
-/-- warning: unused variable `n` [linter.unusedVariables] -/
+/--
+warning: unused variable `n`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+-/
 #guard_msgs in
 #guard_msgs (info) in
 example (n : Nat) : True := trivial