Stream: Coq users

Topic: ✔ How do I debug Ltac being stuck?


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: Jan 29 2023 at 06:02 UTC