linter エラーが設定を貫通する

[Seasawher]

ring のところに tactic does nothing という warning が出て、これをどうやっても消すことができない。

/-- `#expand` の入力に渡すための構文カテゴリ -/
syntax macro_stx := command <|> tactic <|> term

open Lean in

/-- マクロを展開するコマンド -/
elab "#expand " t:macro_stx : command => do
  let t : Syntax := match t.raw with
  | .node _ _ #[t] => t
  | _ => t.raw
  match ← Elab.liftMacroM <| Macro.expandMacro? t with
  | none => logInfo m!"Not a macro"
  | some t => logInfo m!"{t}"

set_option linter.unreachableTactic false

/--
info: first
| ring1
| try_this ring_nf
-/
#guard_msgs (info) in
  #expand ring

[Seasawher]

最小化した例

import Mathlib.Tactic

open Lean in

elab "#greet " _t:tactic : command => do
  logInfo "hello"

set_option linter.unreachableTactic false

/-- info: hello -/
#guard_msgs (info) in
  #greet simp

[Seasawher]

drop warning を追加すればいいだけだった