Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

"r <num>" and "r <string>" in coqtop Ltac debugger broken #18067

Closed
jfehrle opened this issue Sep 19, 2023 · 0 comments · Fixed by #18068
Closed

"r <num>" and "r <string>" in coqtop Ltac debugger broken #18067

jfehrle opened this issue Sep 19, 2023 · 0 comments · Fixed by #18068
Assignees
Labels
part: ltac debugger Issues and PRs related to the Ltac debugger, visual CoqIDE debugger etc.
Milestone

Comments

@jfehrle
Copy link
Member

jfehrle commented Sep 19, 2023

Description of the problem

The r <num>and r <string> commands in the coqtop Ltac debugger generate action op failures. After fixing that immediate problem, these commands never cause the debugger to stop in another breakpoint, rendering them useless.

This breaks using the Ltac debugger through Proof General (relying on coqtop). I only learned about this recently when someone made a one line comment as an aside in one of our online media (I can't remember where) that the debugger in Proof General has been broken since 8.15. If someone had reported this earlier, it would have been fixed a long time ago.

Coq Version 8.15 to 8.18

@jfehrle jfehrle added the part: ltac debugger Issues and PRs related to the Ltac debugger, visual CoqIDE debugger etc. label Sep 19, 2023
@jfehrle jfehrle added this to the 8.18.1 milestone Sep 19, 2023
@jfehrle jfehrle self-assigned this Sep 19, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
part: ltac debugger Issues and PRs related to the Ltac debugger, visual CoqIDE debugger etc.
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant