Stream: Coq users

Topic: ✔ How do I debug Ltac being stuck?

view this post on Zulip abab9579 (Sep 07 2022 at 11:51):

I have some part of Ltac code which gets stuck for unknown reason.
I want to know what it is trying, and why it is hanging there.
What is a good way to profile such Ltac? General directions/tips on such profiling would be great!

view this post on Zulip Michael Soegtrop (Sep 07 2022 at 12:08):

The procedure I usually use is to prepare a file debug.vI run through coqtop with this content:

< do whatever to get to the point before the failing ltac command >
  Set Ltac Debug.
  Set Ltac Batch Debug.
< run the failing ltac command >

I then call

coqtop <-Q/-R option> -lv debug.v 1>debug.log 2>&1

This produces a full log with goal and state. I have some shell scripts to strip this to various levels of verbosity, which I can share.

The other method is to use the Ltac debugger (available in CoqIDE) by @Jim Fehrle - see Ltac-debugger.

Which method is more suitable depends on the complexity. For 3rd party highly intricate Ltac code, batch tracing is better. For self written and not too complex code the interactive debugger is better.

There is also an Ltac profiler, but I use it only for performance analysis, not for debugging.

view this post on Zulip abab9579 (Sep 07 2022 at 12:11):

Thank you for directions! What do you mean by batch tracing?

view this post on Zulip Michael Soegtrop (Sep 07 2022 at 12:14):

With batch tracing I mean the first method I outlined. Usually if you set Set Ltac Debug. it stops after every command. If you set Set Ltac Batch Debug it runs the tactic to the end in batch mode.

view this post on Zulip abab9579 (Sep 08 2022 at 00:38):

Just tried it, it is not the behavior I want - it seems like each step is entire Ltac tactic. I guess I chose the wrong wording.
It seems like this particular tactic usage rewrite frdiffE hangs for indefinitely long (it does seem to stop at some point though), and I need to know what is happening internally. I will try to use profiling for this.

view this post on Zulip abab9579 (Sep 08 2022 at 00:45):

OH, nevermind. It seems like rewrite itself is a primitive tactic.
Thank you for general guidance! I will use this debugging for more complex tactics.

view this post on Zulip Notification Bot (Sep 08 2022 at 00:45):

abab9579 has marked this topic as resolved.

Last updated: Dec 05 2023 at 06:01 UTC