From 793cd14b3816dfec686daa8515d6fc750c6f7326 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= Date: Wed, 13 May 2026 10:40:18 +0100 Subject: [PATCH] feat: improve message of `unusedVariables` linter (#13715) This PR improves the message of `unusedVariables` linter, by replacing potentially confusing "unused variable `x`" message with "Variable name `x` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly)." Related issue: https://github.com/leanprover/lean4/issues/13269 --- src/Lean/Linter/UnusedVariables.lean | 2 +- tests/elab/13269.lean | 24 ++++ tests/elab/grind_unnecessary_hypothesis.lean | 4 +- tests/elab/guard_msgs.lean | 8 +- .../linterUnusedVariables.lean.out.expected | 112 +++++++++++++----- .../warningAsError.lean.out.expected | 4 +- tests/lake/tests/builtin-lint/test.sh | 12 +- .../semanticTokens.lean.out.expected | 2 +- 8 files changed, 128 insertions(+), 40 deletions(-) create mode 100644 tests/elab/13269.lean diff --git a/src/Lean/Linter/UnusedVariables.lean b/src/Lean/Linter/UnusedVariables.lean index abcd4c3f88..23aec7b92b 100644 --- a/src/Lean/Linter/UnusedVariables.lean +++ b/src/Lean/Linter/UnusedVariables.lean @@ -570,7 +570,7 @@ def unusedVariables : Linter where -- Sort the outputs by position for (declStx, userName) in unused.qsort (·.1.getPos?.get! < ·.1.getPos?.get!) do - logLint linter.unusedVariables declStx m!"unused variable `{userName}`" + logLint linter.unusedVariables declStx m!"Variable name `{userName}` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly)." builtin_initialize addLinter unusedVariables diff --git a/tests/elab/13269.lean b/tests/elab/13269.lean new file mode 100644 index 0000000000..c1bbc18735 --- /dev/null +++ b/tests/elab/13269.lean @@ -0,0 +1,24 @@ +set_option linter.unusedVariables true + +class Foo + +def bar [Foo] := 0 + +/-- +warning: Variable name `x` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). + +Note: This linter can be disabled with `set_option linter.unusedVariables false` +-/ +#guard_msgs in +def baz := let x := Foo.mk; bar -- unused variable `x` + +/-- +error: failed to synthesize instance of type class + Foo + +Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. +-/ +#guard_msgs in +def baz':= bar -- failed to synthesize instance of type class Foo diff --git a/tests/elab/grind_unnecessary_hypothesis.lean b/tests/elab/grind_unnecessary_hypothesis.lean index 9b29b2e3b7..6d0695585c 100644 --- a/tests/elab/grind_unnecessary_hypothesis.lean +++ b/tests/elab/grind_unnecessary_hypothesis.lean @@ -53,7 +53,9 @@ info: idxToCount''.go.{u_1} {α : Type u_1} [BEq α] (xs : List α) (i : Nat) (h set_option linter.unusedVariables true -- Another example from the Zulip thread /-- -warning: unused variable `hi` +warning: Variable name `hi` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -/ diff --git a/tests/elab/guard_msgs.lean b/tests/elab/guard_msgs.lean index c0f46b2310..26c808d6ec 100644 --- a/tests/elab/guard_msgs.lean +++ b/tests/elab/guard_msgs.lean @@ -154,7 +154,9 @@ set_option linter.unusedVariables true #guard_msgs in /-- -warning: unused variable `n` +warning: Variable name `n` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -/ @@ -163,7 +165,9 @@ example (n : Nat) : True := trivial #guard_msgs in /-- -warning: unused variable `n` +warning: Variable name `n` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -/ diff --git a/tests/elab_fail/linterUnusedVariables.lean.out.expected b/tests/elab_fail/linterUnusedVariables.lean.out.expected index 27186e13a3..0a3837213f 100644 --- a/tests/elab_fail/linterUnusedVariables.lean.out.expected +++ b/tests/elab_fail/linterUnusedVariables.lean.out.expected @@ -1,82 +1,136 @@ -linterUnusedVariables.lean:18:21-18:22: warning: unused variable `x` +linterUnusedVariables.lean:18:21-18:22: warning: Variable name `x` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -linterUnusedVariables.lean:19:6-19:7: warning: unused variable `y` +linterUnusedVariables.lean:19:6-19:7: warning: Variable name `y` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -linterUnusedVariables.lean:24:8-24:9: warning: unused variable `x` +linterUnusedVariables.lean:24:8-24:9: warning: Variable name `x` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -linterUnusedVariables.lean:40:5-40:6: warning: unused variable `x` +linterUnusedVariables.lean:40:5-40:6: warning: Variable name `x` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -linterUnusedVariables.lean:45:5-45:6: warning: unused variable `x` +linterUnusedVariables.lean:45:5-45:6: warning: Variable name `x` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -linterUnusedVariables.lean:48:7-48:8: warning: unused variable `x` +linterUnusedVariables.lean:48:7-48:8: warning: Variable name `x` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -linterUnusedVariables.lean:51:8-51:9: warning: unused variable `x` +linterUnusedVariables.lean:51:8-51:9: warning: Variable name `x` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -linterUnusedVariables.lean:55:9-55:10: warning: unused variable `z` +linterUnusedVariables.lean:55:9-55:10: warning: Variable name `z` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -linterUnusedVariables.lean:57:11-57:12: warning: unused variable `z` +linterUnusedVariables.lean:57:11-57:12: warning: Variable name `z` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -linterUnusedVariables.lean:62:14-62:15: warning: unused variable `y` +linterUnusedVariables.lean:62:14-62:15: warning: Variable name `y` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -linterUnusedVariables.lean:68:20-68:21: warning: unused variable `y` +linterUnusedVariables.lean:68:20-68:21: warning: Variable name `y` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -linterUnusedVariables.lean:73:34-73:38: warning: unused variable `inst` +linterUnusedVariables.lean:73:34-73:38: warning: Variable name `inst` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -linterUnusedVariables.lean:114:25-114:26: warning: unused variable `x` +linterUnusedVariables.lean:114:25-114:26: warning: Variable name `x` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -linterUnusedVariables.lean:115:6-115:7: warning: unused variable `y` +linterUnusedVariables.lean:115:6-115:7: warning: Variable name `y` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -linterUnusedVariables.lean:121:6-121:7: warning: unused variable `a` +linterUnusedVariables.lean:121:6-121:7: warning: Variable name `a` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -linterUnusedVariables.lean:131:26-131:27: warning: unused variable `z` +linterUnusedVariables.lean:131:26-131:27: warning: Variable name `z` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -linterUnusedVariables.lean:140:9-140:10: warning: unused variable `h` +linterUnusedVariables.lean:140:9-140:10: warning: Variable name `h` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -linterUnusedVariables.lean:154:8-154:9: warning: unused variable `y` +linterUnusedVariables.lean:154:8-154:9: warning: Variable name `y` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -linterUnusedVariables.lean:157:28-157:29: warning: unused variable `β` +linterUnusedVariables.lean:157:28-157:29: warning: Variable name `β` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -linterUnusedVariables.lean:158:7-158:8: warning: unused variable `x` +linterUnusedVariables.lean:158:7-158:8: warning: Variable name `x` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -linterUnusedVariables.lean:168:6-168:7: warning: unused variable `s` +linterUnusedVariables.lean:168:6-168:7: warning: Variable name `s` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -linterUnusedVariables.lean:192:6-192:7: warning: unused variable `y` +linterUnusedVariables.lean:192:6-192:7: warning: Variable name `y` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -linterUnusedVariables.lean:202:19-202:20: warning: unused variable `x` +linterUnusedVariables.lean:202:19-202:20: warning: Variable name `x` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -linterUnusedVariables.lean:206:6-206:7: warning: unused variable `y` +linterUnusedVariables.lean:206:6-206:7: warning: Variable name `y` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -linterUnusedVariables.lean:211:6-211:7: warning: unused variable `y` +linterUnusedVariables.lean:211:6-211:7: warning: Variable name `y` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -linterUnusedVariables.lean:216:6-216:7: warning: unused variable `y` +linterUnusedVariables.lean:216:6-216:7: warning: Variable name `y` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` -linterUnusedVariables.lean:227:32-227:33: warning: unused variable `b` +linterUnusedVariables.lean:227:32-227:33: warning: Variable name `b` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` linterUnusedVariables.lean:245:27-245:28: error: don't know how to synthesize placeholder @@ -93,6 +147,8 @@ a : Nat ⊢ Nat linterUnusedVariables.lean:249:0-249:40: error: type of theorem `async` is not a proposition Nat → Nat -linterUnusedVariables.lean:284:41-284:43: warning: unused variable `ha` +linterUnusedVariables.lean:284:41-284:43: warning: Variable name `ha` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` diff --git a/tests/elab_fail/warningAsError.lean.out.expected b/tests/elab_fail/warningAsError.lean.out.expected index 557a4edda1..f09530097d 100644 --- a/tests/elab_fail/warningAsError.lean.out.expected +++ b/tests/elab_fail/warningAsError.lean.out.expected @@ -2,6 +2,8 @@ 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` +warningAsError.lean:15:7-15:13: error: Variable name `unused` is not explicitly referenced. + +The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false` diff --git a/tests/lake/tests/builtin-lint/test.sh b/tests/lake/tests/builtin-lint/test.sh index e2de9f1baf..edbb83fd78 100755 --- a/tests/lake/tests/builtin-lint/test.sh +++ b/tests/lake/tests/builtin-lint/test.sh @@ -13,21 +13,21 @@ test_run lint --builtin-only Clean # is captured in `lintLogExt`, and is re-emitted by `lake lint` post-build. # `linter.missingDocs` (defValue=false) must NOT fire without --lint-all/--lint-only. lake_out lint --builtin-only TextLints || true -match_pat 'unused variable `unusedLet`' produced.out +match_pat 'Variable name `unusedLet` is not explicitly referenced' produced.out no_match_pat 'missing doc string' produced.out # --lint-all enables all linters, so missingDocs fires too. lake_out lint --lint-all TextLints || true -match_pat 'unused variable `unusedLet`' produced.out +match_pat 'Variable name `unusedLet` is not explicitly referenced' produced.out match_pat 'missing doc string for public def undocumentedPublicDef' produced.out # --lint-only filters entries by suffix match against the linter name. lake_out lint --lint-only missingDocs TextLints || true match_pat 'missing doc string for public def undocumentedPublicDef' produced.out -no_match_pat 'unused variable' produced.out +no_match_pat 'is not explicitly referenced' produced.out lake_out lint --lint-only unusedVariables TextLints || true -match_pat 'unused variable `unusedLet`' produced.out +match_pat 'Variable name `unusedLet` is not explicitly referenced' produced.out no_match_pat 'missing doc string' produced.out # --builtin-lint should detect the defLemma violation in Main (the default target) @@ -64,7 +64,7 @@ match_pat 'shouldBeTheoremInSub' produced.out # `linter.unusedVariables` (defValue=true) fires on every build, so its entry # lands in `Main.Sub.olean` unconditionally. -match_pat 'unused variable `unusedInSub`' produced.out +match_pat 'Variable name `unusedInSub` is not explicitly referenced' produced.out # Explicit arg with --lint-all: the override applies to the whole package of # `Main`, so `Main.Sub` is also built with `linter.all=true` and the @@ -116,7 +116,7 @@ match_pat 'shouldBeTheoremUnderExtra' produced.out # linters run under --extra). `linter.missingDocs` is still off-by-default # and only enabled by `--lint-all`/`--lint-only`. lake_out lint --extra TextLints || true -match_pat 'unused variable `unusedLet`' produced.out +match_pat 'Variable name `unusedLet` is not explicitly referenced' produced.out no_match_pat 'missing doc string' produced.out # --lint-all should run both default and extra linters, for both the diff --git a/tests/server_interactive/semanticTokens.lean.out.expected b/tests/server_interactive/semanticTokens.lean.out.expected index 38c8cd057d..1951312f85 100644 --- a/tests/server_interactive/semanticTokens.lean.out.expected +++ b/tests/server_interactive/semanticTokens.lean.out.expected @@ -17,7 +17,7 @@ "range": {"start": {"line": 3, "character": 6}, "end": {"line": 3, "character": 7}}, "message": - "unused variable `y`\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`", + "Variable name `y` is not explicitly referenced.\n\nThe binding can be removed (if unused) or named `_` (if used implicitly).\n\nNote: This linter can be disabled with `set_option linter.unusedVariables false`", "fullRange": {"start": {"line": 3, "character": 6}, "end": {"line": 3, "character": 7}}}, {"source": "Lean 4",