Get decl name in a tactic

Stream: lean4

[Adam Topaz]

How does one obtain the declaration name inside of a tactic? I tried the following:

import Lean

open Lean Elab Tactic

elab "test" : tactic => do
  IO.println decl_name%

def foo : ℕ := by
  test -- Prints `_aux_SpecSorry_test___elabRules_tacticTest_1`
  sorry

but I want test to print foo instead of the tactic's underlying name.

[Adam Topaz]

I tried this as well, with the same result

elab "test" : tactic => do
  let ctx ← read
  IO.println ctx.elaborator

[Adam Topaz]

Maybe I should mention that I don't know whether this is possible.

[Kyle Miller]

You can. I took the definition of decl_name% to make this, hence the lingering error message

import Lean

open Lean Elab Tactic

elab "test" : tactic => do
  let some declName ← Term.getDeclName?
    | throwError "invalid `decl_name%` macro, the declaration name is not available"
  IO.println declName

def foo : ℕ := by
  test -- Prints `foo`
  sorry

[Adam Topaz]

Oh great, thanks!