finding a failed

Stream: general

[Keeley Hoek]

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]

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

[Mario Carneiro]

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]

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]

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]

who wrote it?

[Simon Hudon]

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]

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') }