Zulip Chat Archive

Stream: general

Topic: finding a failed


Keeley Hoek (Sep 10 2018 at 07:31):

What's the easiest way to find where a "failed" was generated? I've been resorting to inserting trace statements in multiple files and now its just getting out of hand

Keeley Hoek (Sep 10 2018 at 07:44):

also, in the tactic monad, is there a way to get a stacktrace?

Mario Carneiro (Sep 10 2018 at 07:45):

There is the vm monad, which purports to be a debugger, but I don't know anyone who knows how to use it except possibly @Sebastian Ullrich

Simon Hudon (Sep 10 2018 at 16:07):

What I usually do is that, if I have a function with three lines I add the following until I find the error:

meta def my_fn : tactic unit :=
do stmt1 <|> fail "line A",
   stmt2 <|> fail "line B",
   stmt3 <|> fail "line C"

When I have found the function that fails, I repeat in that function.

Sebastian Ullrich (Sep 10 2018 at 16:45):

I've never used vm :sweat_smile: . I suppose it should be possible to write a vm_monitor that prints the stack trace whenever failed is called.

Mario Carneiro (Sep 10 2018 at 16:46):

who wrote it?

Simon Hudon (Sep 10 2018 at 19:18):

I had never used `vm_monitor and I gave it a try. Here's what I did:

set_option debugger true

@[vm_monitor]
meta def my_mon : vm_monitor unit :=
{ init := (),
  step := λ _,
  do vm.curr_fn >>= vm.trace }

run_cmd my_tactic

set_option debugger false

It sets up a monitor that, before each instruction, prints the name of the enclosing function. It does not seem to be aware of failures but at least, you can figure out where the problem is by looking at the last printout

Simon Hudon (Sep 10 2018 at 19:40):

If you use the following instead, you can get an overview of the call nesting structure:

@[vm_monitor]
meta def my_mon : vm_monitor (nat × option name) :=
{ init := (0, none),
  step := λ fn,
  do fn'  vm.curr_fn,
     n'  vm.call_stack_size,
     when (fn  (n',some fn')) $ vm.trace $ (string.join $ list.repeat "| " n') ++ to_string fn',
     pure (n',fn') }

Last updated: Dec 20 2023 at 11:08 UTC