Visual debugger for Ltac

[jfehrle]

Looking for feedback on the general plan and advice on selecting between some of the alternatives.

Rendered: https://github.com/jfehrle/ceps/blob/debugger/text/053-debugger.md

[maximedenes]

Did you consider basing it on the debug adapter protocol ? https://microsoft.github.io/debug-adapter-protocol/

[jfehrle]

No, I haven't thought much about that. I remember participating in a phone call, perhaps a year ago, in which we discussed protocols through which GUIs can communicate with Coq. While it would be nice to have a single protocol, IIRC we wanted to be able to support more than one protocol so we could fit into things like VsDev to create VsCoq. But I'm not aware of what has been done since then to support multiple protocols. I believe you've been working on VsCoq. (I mostly use CoqIDE.)

I believe CoqIDE should support any visual debugger we create. If VsCoq already supports the debugger adapter protocol then that might be a quicker path to getting an initial version working. Furthermore, we should consider whether that protocol should be the model for equivalent additions to the CoqIDE protocol.

BTW incremental development makes great sense--at each stage of the project, it's usually best to start and efficiently complete things that are limited in scope that have clear value to users. At times that may mean a little extra work, but I think the odds of delivering something useful in a reasonable timeframe are better. (For example, step # 1 would parse some debugger commands. That parsing code may be dropped later, in step # 4, but creating that parsing code avoids having to agree on and implement GUI protocols at the outset. It's probably keeps step # 1 simple enough for one developer to implement efficiently.)

[silene]

As I said during the call, the very first thing would be to get Set Ltac Debug to work under CoqIDE (or any other graphical interface). Currently, it only works in Coqtop.

[jfehrle]

@silene Thanks for repeating--I had some trouble making out what you were saying during the call. Support in GUIs is sorely needed. I'll consider doing that sooner rather than later, probably through a terminal-like interface (# 3 in the proposal).

[jfehrle]

Notes from the call are here

We also discussed the relationship between Stm and the debugger commands. Most but not all developers thought debugger commands should not be saved as Stm state and perhaps should not even be seen by Stm.

[gares]

To summarize what I proposed, step 0 would be to have the following "thing" to work.

On one shell

nc -l  -p 9999

and on the other shell

echo 'Goal True. Set Ltac Debug. idtac; auto. Qed.' > a.v
LTAC_DEBUG=localhost:9999 coqc a.v

If it works with coqc, then it will work with coqtop, coqidetop... Then a proper way to enable debugging and pass the side channel address should be found.

[jfehrle]

Instead of opening another connection, how about this? Maybe simpler.

Send debug commands (a line of input ending with \n) and output over the existing socket as XML messages rather than creating a new socket. Distinguish debug commands and output with a tag or new message type. I think the debugger doesn't need asynchronous behavior, except if/when we want to support an "interrupt" function akin to CTRL-C.

The existing output window can double as the debugger window. I'd tweak it so that debugger output is appended to the buffer rather than clearing it while disallowing modification above the last line. The debugger might also update the proof state window--or possibly use it to display other information.

Debugger commands can be parsed by adding new rules to our main parser under a debug_cmd nonterminal. That nonterminal could also eventually include non-state modifying commands such as "Show Proof", likely with tweaks to make them bulletproof in the middle of a tactic.

What do you think?

[gares]

Mixin debug command with XML messages is going to tie the two. PG does not use the XML protocol, rather the tty one. Soon vscoq will drop XML for LSP, which is very different. IMO the debeggung channel should be separate, and the protocol orthogonal.

Reusing the window as you suggest is fine, nc is just simulating that window/embedded terminal without patching coqide.

[jfehrle]

Creating an additional connection would be specific to CoqIDE and not reusable for other GUIs. I expect vscoq/LSP uses a single socket for both editing and debugging operations. Its existing messages for debugging are already linked to GUI behavior. We don't want to change that interface more than necessary.

We should continue to support the debugger in coqtop. It's helpful for development and testing. It makes it easy to include debugger output in the documentation through the .. coqtop:: directive. Since PG currently uses the coqtop interface, they already could support the existing debugger commands if they choose to. They don't need an additional connection.

The mixing will be superficial. Think of XML, coqtop and LSP as different transport mechanisms that invoke common code in Coq for interpreting debugger commands. In the spirit of incremental development, I'll get CoqIDE to work first with the existing debugger commands, then later revise the code, if necessary, for the other GUIs.

Does this seem reasonable?

[gares]

IMO, it will take you a hunder times more time to sneak in a few messages in the XML protocol (and the code that speak is) than use a side channel to talk directly with the ltac interpreter. But it is your time, so I won't argue further on that.

coqtop is already attached to a terminal, so it can use it as a (non side) channel. I don't see how allowing to have a side channel (in case the terminal is not there) would make things harder in coqtop: if there is a terminal, use it, if not use the socket if given.

The XML protocol has nothing to do with the LSP one, and the coqtop "protocol" (used by emacs) is yet another thing. It is not about the encoding of messages, it is that the messages are totally different, about statefulness, about synchronicity. It's like comparing http and ftp, IMO there is no hope to share anything (other than having the debugger be reachable without a terminal)

[jfehrle]

Q: For add_rty, I see this note in the code from almost 4 years ago: "The response [(id,(rc,s)] ... [s] used to contain Coq's console ouptut and has been deprecated in favor of sending feedback, it will be removed in a future version of the protocol." Looking at some test messages I only see an empty string in the field. If this is ripe for removal, I could take care of it.

type add_rty = state_id * ((unit, state_id) union * string)

EDIT: I assume s refers to the string. The "[(id,(rc,s)]" in the comment is not accurate.

[gares]

Yes

[jfehrle]

The debugger read-eval-print loop is called by Tacinterp.val_interp, the recursive routine that interprets an
Ltac expression. I expect the recursive calls mean that there's a lot of state in the call stack.

A common technique to deal with this would be to separate reading debugger commands from the eval-print and converting the latter to a state machine or perhaps (I think) continuation passing. But given the recursion and the state in the stack, I think this would be prohibitively complex. Furthermore, the changes would probably be strewn across the Ltac interpreter and would permanently add complexity there.

I think the better solution for receiving debugger commands from the GUI is to clone the inner part of Idetop.loop (which reads and parses XML messages) and run it in a different thread while Coq is in the debugger. The commands could be passed between threads a couple ways:

• a shared data structure holding a string, which is the next command. Use Thread.wait_signal so the main thread can block and resume as debugger commands are received.
• a pipe. Blocking is built in to the read operation.
• a socket. Blocking is also built in.

I think I'd prefer one of the first two. (FWIW the first may work better if we eventually want to support debugging proofs in a multithreaded/multicore environment. AFAIK that is not going to be an issue anytime soon.)

Blocking on the thread interpreting Ltac code appears to correspond to the "global lock" idea that @ppedrot mentioned in the Coq Call.

For output, it appears that calls to Feedback.msg_notice are immediately sent to the GUI, so that should not be an issue.

I thought I'd mention this now rather than surprise anyone when they see this in a PR. WDYT?

[silene]

I do not understand what you are trying to achieve. It seems you are making things way more complicated than needed. The Ltac debugger calls NonLogical.read_line, which currently reads on the standard input. Just modify this call so that it can read on another input channel, e.g., a socket as Enrico suggested. There is absolutely no reason to duplicate existing code or to involve threads.

[jfehrle]

Using a socket is likely simplistic and may not age well. It may be a quick solution to get the debugger working terminal-style in CoqIDE. But I think you'd want something more robust for a visual debugger later on. You may want calls that return structured data such as the call stack, including the corresponding source file locations so the GUI can jump there when you double-click on an entry in a stack panel. Or the list of defined variables.

For these, you need a way to marshall and unmarshall return values. I'd rather not reinvent that code. The current debugger only responds by printing things. Parsing printed output isn't appealing. CoqIDE would need additional logic to recognize that output at the right moment and forward the result to the appropriate routine, muddying the design. I'd rather not search for the user prompt in the output just to know that the debugger has completed a request.

As I mentioned earlier in this thread, I expect LSP already defines various debugger messages. While the details will be different than for CoqIDE, LSP will also need to communicate with the debugger read-eval-print loop. I suspect changing those messages to use a second socket could pose challenges for LSP/vscoq support. But hard to know without seeing a working LSP interface and then evaluating the impact.

There is absolutely no reason to duplicate existing code or to involve threads.

I should have said "share" rather than "clone". Probably just calling the same routine in 2 places. The threading code should be quite small and simple.

IMO, it will take you a hundred times more time to sneak in a few messages in the XML protocol (and the code that speak is) than use a side channel to talk directly with the ltac interpreter.

I think you exaggerate. Passing the command line into the debugger within the coqidetop process is the last step before I can demonstrate basic functionality. Maybe a day or two to do that, plus time to refine a few details.

It's a bit premature to judge this before seeing the code.

[silene]

As I mentioned earlier in this thread, I expect LSP already defines various debugger messages. While the details will be different than for CoqIDE, LSP will also need to communicate with the debugger read-eval-print loop. I suspect changing those messages to use a second socket could pose challenges for LSP/vscoq support.

Honestly, this discussion is going nowhere. Where did you even read that LSP was providing debugger messages? The LSP specification is 8k lines of text, and there are only two occurrences of the "debug" word in it (and it is for debugging the LSP protocol itself). It is the Language Server Protocol; it does not handle debugger messages!

Debugger messages are handled by the Debug Adapter Protocol, as the name implies.

LSP and DAP are two completely separate protocols and they are using two separate sockets (or pipes or whatever). And there is a good reason for having two separate communication channels. Almost no programming language ships the compiler and the debugger into the same executable!

[jfehrle]

That is a good point, my mistake. But comments like "Honestly, this discussion is going nowhere." are not so helpful.

[gares]

I think this CEP is a good example why we need CEPs and why this one is incomplete. I tried to suggest it at the Coq call, but well, I guess I failed to explain why.

This CEP, at its current state, is not talking about technical points. Nobody objects a debugger is useful.
What the CEP author(s) should do is to think about the implementation details beforehand, and look at what others do to solve similar problems, see if the same solution can be applied or not, and explaian why. Only then, I believe, discussion can really be effective.

[Zimmi48]

@jfehrle has expressed that his goal here was to get feedback on the general plan only and that he would open other discussions (including possibly CEPs) on implementation details.

If there's nothing to add on the general plan at this point, Jim is proposing to merge.

Let's do that on Monday if there are no more comments.