Unused variable linter to ignore custom sorry

Stream: lean4

[Thomas Zhu]

This code triggers an unused variable linter warning on b. How do I disable it?

macro "my_sorry" : tactic => `(tactic| sorry)

theorem a (b : Nat) : True := by my_sorry

This behavior is introduced by lean4#7129. I can see in the comment in the private def hasSorry that I can disable it using a suitable @[unused_variables_ignore_fn], but I couldn't figure out how to write this function (or if using it is the best approach). Alternatively there is a temporary workaround

import Lean

open Lean Elab Tactic

elab "use_all_variables" : tactic =>
  liftMetaTactic1 fun g => do
    let mut g := g
    for ldecl in ← getLCtx do
      unless ldecl.isImplementationDetail do
        g ← g.define (← Meta.mkFreshBinderNameForTactic `use_all_variables) ldecl.type ldecl.toExpr
        (_, g) ← g.intro1P
    return g

macro "my_sorry" : tactic => `(tactic| use_all_variables <;> sorry)

theorem a (b : Nat) : True := by my_sorry

But I am not sure if this is the best solution.

[Robin Arnez]

set_option linter.unusedVariables false in?

[Robin Arnez]

or do you want this to work for all cases of my_sorry?

[Thomas Zhu]

@Robin Arnez I still want the unused variable linter to work when a proof doesn't use sorry, and to automatically disable it when the proof has my_sorry without having to manually set_option.