Zulip Chat Archive

Stream: lean4

Topic: Debug traces for non-terminating tactic


Alexander Bentkamp (Dec 20 2021 at 18:14):

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 (Dec 20 2021 at 18:30):

I cannot see the output anywhere.

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

Gabriel Ebner (Dec 20 2021 at 18:31):

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

Gabriel Ebner (Dec 20 2021 at 18:40):

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 (Dec 20 2021 at 20:05):

Thanks!


Last updated: Dec 20 2023 at 11:08 UTC