From 3549ad5533b9e1b0057513eaedd1cf950c781da8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 17 Apr 2024 20:03:13 +0200 Subject: [PATCH] feat: make linter options more explicitly discoverable --- src/Lean/Linter/Util.lean | 3 +- .../lean/linterMissingDocs.lean.expected.out | 111 ++++++++++++------ ...iciousUnexpanderPatterns.lean.expected.out | 6 +- .../linterUnusedVariables.lean.expected.out | 90 +++++++++----- tests/lean/run/ext.lean | 5 +- tests/lean/run/guard_msgs.lean | 10 +- tests/lean/warningAsError.lean.expected.out | 3 +- 7 files changed, 154 insertions(+), 74 deletions(-) diff --git a/src/Lean/Linter/Util.lean b/src/Lean/Linter/Util.lean index 7b91ab86d0d7..65f67ffbf50e 100644 --- a/src/Lean/Linter/Util.lean +++ b/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`. -/ diff --git a/tests/lean/linterMissingDocs.lean.expected.out b/tests/lean/linterMissingDocs.lean.expected.out index ba55c4705b63..af2cec082712 100644 --- a/tests/lean/linterMissingDocs.lean.expected.out +++ b/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` diff --git a/tests/lean/linterSuspiciousUnexpanderPatterns.lean.expected.out b/tests/lean/linterSuspiciousUnexpanderPatterns.lean.expected.out index 4e031777372b..09dc2b958710 100644 --- a/tests/lean/linterSuspiciousUnexpanderPatterns.lean.expected.out +++ b/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` diff --git a/tests/lean/linterUnusedVariables.lean.expected.out b/tests/lean/linterUnusedVariables.lean.expected.out index 455b091eb58f..01bc4647cdf1 100644 --- a/tests/lean/linterUnusedVariables.lean.expected.out +++ b/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` diff --git a/tests/lean/run/ext.lean b/tests/lean/run/ext.lean index e628caf53d0c..014d27a8ce23 100644 --- a/tests/lean/run/ext.lean +++ b/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 diff --git a/tests/lean/run/guard_msgs.lean b/tests/lean/run/guard_msgs.lean index df1db337f2c3..28d2d9550527 100644 --- a/tests/lean/run/guard_msgs.lean +++ b/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 diff --git a/tests/lean/warningAsError.lean.expected.out b/tests/lean/warningAsError.lean.expected.out index 648ec65610fd..97388297b478 100644 --- a/tests/lean/warningAsError.lean.expected.out +++ b/tests/lean/warningAsError.lean.expected.out @@ -2,4 +2,5 @@ warningAsError.lean:8:6-8:7: warning: `g` has been deprecated, use `f` instead 1 warningAsError.lean:12:6-12:7: error: `g` has been deprecated, use `f` instead 1 -warningAsError.lean:15:7-15:13: error: unused variable `unused` [linter.unusedVariables] +warningAsError.lean:15:7-15:13: error: unused variable `unused` +note: this linter can be disabled with `set_option linter.unusedVariables false`