How do I debug a strange prompt?

[Eduardo Ochs]

Hi all,

sometimes when I am working on Lean4 files lean4-mode asks me a
certain question that I don't understand. I tried to locate the
function that asks it by running this,

  (run-at-time 5 nil 'eval '(debug))

then reproducing the steps that makes lean4-mode ask that question,
and then waiting for the remaining of the 5 seconds for the debugger
to pop in... but then I get a very short backtrace, like this,

Debugger entered: nil
  eval((debug))
  apply(eval (debug))
  timer-event-handler([t 26592 213 999794 nil eval ((debug)) nil 982000 nil])

instead of a backtrace that includes the function that I'm trying to
locate and the call to `interactive'.

What should I do instead?

  Thanks in advance!
  Eduardo Ochs
    http://anggtwu.net/#eev
    http://anggtwu.net/emacsconf2024.html