diff --git a/src/Lean/Linter/UnusedVariables.lean b/src/Lean/Linter/UnusedVariables.lean index ff349407aaa2..82471d928a6e 100644 --- a/src/Lean/Linter/UnusedVariables.lean +++ b/src/Lean/Linter/UnusedVariables.lean @@ -255,6 +255,10 @@ builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack opts => (stx.isOfKind ``Lean.Parser.Term.matchAlt && pos == 1) || (stx.isOfKind ``Lean.Parser.Tactic.inductionAltLHS && pos == 2)) +/-- `#guard_msgs in cmd` itself runs linters in `cmd` (via `elabCommandTopLevel`), so do not run them again. -/ +builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ => + stack.any fun (stx, _) => stx.isOfKind ``Lean.guardMsgsCmd) + /-- Get the current list of `IgnoreFunction`s. -/ def getUnusedVariablesIgnoreFns : CommandElabM (Array IgnoreFunction) := do return (unusedVariablesIgnoreFnsExt.getState (← getEnv)).2 diff --git a/tests/lean/run/guard_msgs.lean b/tests/lean/run/guard_msgs.lean index dbae9fd3114c..df1db337f2c3 100644 --- a/tests/lean/run/guard_msgs.lean +++ b/tests/lean/run/guard_msgs.lean @@ -129,3 +129,18 @@ info: A -/ #guard_msgs in run_meta do Lean.logInfo "B"; Lean.logInfo "A" + +/-! +Linter suppression +-/ + +set_option linter.unusedVariables true + +/-- warning: unused variable `n` [linter.unusedVariables] -/ +#guard_msgs in +example (n : Nat) : True := trivial + +/-- warning: unused variable `n` [linter.unusedVariables] -/ +#guard_msgs in +#guard_msgs (info) in +example (n : Nat) : True := trivial