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!
The procedure I usually use is to prepare a file debug.v
I 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.
Thank you for directions! What do you mean by batch tracing?
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.
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.
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.
abab9579 has marked this topic as resolved.
Last updated: Dec 05 2023 at 06:01 UTC