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.
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.
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.
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)
@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.)
@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.
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.
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.
@Jim Fehrle : should I test your PR in CoqIDE or the debugger in coqtop in release Coq?
@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: Oct 16 2021 at 03:02 UTC