Stream: Coq users

Topic: Goal display in Ltac debugger


view this post on Zulip Michael Soegtrop (Apr 04 2022 at 16:56):

@Jim Fehrle : I tried the debugger in 8.15.1 and found that the goal does not change any more when I step through ltac code - it remains what it was when debugging started. If I remember right, this was not so in previous versions. Is this expected?

view this post on Zulip Jim Fehrle (Apr 04 2022 at 19:38):

Can you provide a short example? I couldn't reproduce the problem in master or the updated v8.15 (= 8.15.1 IIUC) with this example:

image.png

image.png

The only change I recall to debugger goal printing is it that the output will show multiple goals. It's not expected. If you can reproduce this, please open an issue.

view this post on Zulip Jim Fehrle (Apr 04 2022 at 19:41):

It also appears to update multiple goals correctly:

image.png

view this post on Zulip Michael Soegtrop (Apr 05 2022 at 07:18):

@Jim Fehrle : OK, your example works and it doesn't seem to be easy to find a trivial example. My issues are with the VST "forward" tactic - let me see if I can boil it down.

view this post on Zulip Michael Soegtrop (Apr 05 2022 at 08:53):

@Jim Fehrle : the issue happens when one calls a tactic from another file. I will file an issue.


Last updated: Mar 29 2024 at 04:02 UTC