Debug traces for non-terminating tactic

Stream: lean4

[Alexander Bentkamp]

How can I debug a tactic that does not terminate? I thought dbg_trace should do that, put I cannot see the output anywhere.

namespace Lean.Elab.Tactic

syntax (name := test) "test" : tactic

@[tactic test]
partial def evalTest : Tactic
| `(tactic| test) => do
  dbg_trace "Test"
  let rec loop := fun (a : Nat) => loop (a + 1)
  loop 0
| _ => throwUnsupportedSyntax

end Lean.Elab.Tactic

example : False := by
  test

Or should I try to update Lean? I am on leanprover/lean4:nightly-2021-10-21.

[Gabriel Ebner]

I cannot see the output anywhere.

That's because it doesn't terminate. You can see it on the command-line though.

[Gabriel Ebner]

There's also no automatic timeout like in Lean 3, you need to check for heartbeats yourself.

[Gabriel Ebner]

For example this terminates, and shows "Test" in the infoview:

import Lean
open Lean Elab Elab.Tactic

syntax (name := test) "test" : tactic

@[tactic test]
partial def evalTest : Tactic
| `(tactic| test) => do
  dbg_trace "Test"
  let rec loop := fun (a : Nat) => do
    checkMaxHeartbeats "test"
    loop (a + 1)
  loop 0
| _ => throwUnsupportedSyntax

example : False := by
  test

[Alexander Bentkamp]

Thanks!