Emilio Jesús Gallego Arias (Apr 26 2021 at 21:05): Emilio Jesús Gallego Arias (Apr 26 2021 at 21:05):Hi @Jim Fehrle and rest, I am opening this topic to discuss further evolution and design of the Ltac Debugger protocol; I am finding the Github interface quite hard to use and beyond its limits, to be honest, so I think we will have a better interaction experience here.
Also, I don't quite like Github PRs to have design discussions which are indeed more like a whiteboard meeting than a code review.
Michael Soegtrop (Apr 27 2021 at 11:00):I wonder what the plans are to support Ltac2 and Mtac2 with a debugger protocol. Also how about a debugger for compute? I don't say I want this right now, but I think it should be considered in the discussion.
IMHO Ltac is legacy.
Emilio Jesús Gallego Arias (Apr 27 2021 at 12:28):Indeed these are very good points @Michael Soegtrop , current efforts for ltac are indeed IMHO at the experimental stage, but they should serve as a basis for adding better debuggin support to other subsytems.
Enrico Tassi (Apr 27 2021 at 14:01):There was a comment about using DAP, early in the discussion, by @Maxime Dénès .
Unfortunately the pandemic took a toll on the LSP based vscoqtop thing, which in turn made it hard to experiment with it.
(DAP is not part of LSP, but it is surely easier to play with once we have an LSP native toplevel)
Jim Fehrle (Apr 27 2021 at 20:43):@Michael Soegtrop I believe Ltac2 uses much of the Ltac machinery for execution, so the current debugger may work (partially or fully) without additional effort. I have no idea about Mtac2. Perhaps you would be willing to try these? (I have little experience with Ltac2 and know nothing about Mtac2.)
Jim Fehrle (Apr 27 2021 at 20:46):@Emilio Jesús Gallego Arias Zulip is not a great option for this. For me, real-time discussion is difficult to impossible given that I'm 9 time zones away from most of the main developers.
Emilio Jesús Gallego Arias (Apr 27 2021 at 21:01):We tend to hang out at this time, so YMMV; at least here we have some hope to discuss, the Github interface is just not suited for discussion.
Jim Fehrle (Apr 28 2021 at 04:49):Also, while I'm happy to share my thoughts on debugger protocol support such as for LSP, if I want feedback on planned additions to the CoqIDE protocol before code review time, I will request it. We just did the work to make LSP and the CoqIDE protocols completely independent. Let's not try to force them to be overly similar. There doesn't have to be 1-1 mapping of calls as long as the underlying server code can reasonably handle the functional needs of both protocols. At the moment I add 3 more very vanilla messages in the next PR. And the added messages are subject to revision as better ideas are found.
Michael Soegtrop (Apr 28 2021 at 09:15):@Jim Fehrle : should I test your PR in CoqIDE or the debugger in coqtop in release Coq?
Jim Fehrle (Apr 28 2021 at 13:53):@Michael Soegtrop It would be nice if you tried it in CoqIDE (which I hope will be merged today) but checking in coqtop premerge would be about as good. One existing debugger command for skipping N steps was broken, now fixed in the PR, BTW.
Last updated: Sep 09 2024 at 05:02 UTC