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

@@ -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
 

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

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`
 -/

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`
 -/

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`

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`

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

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",