Updating PG way to communicate with Coq

[ejgallego]

Dear PG devs,

the topic of how Proof General interacts with Coq has been again discussed Coq upstream. I think the moment has come where we should try to add a bit more structure to PGs / Coq-EasyCrypt interface and solve many longstanding issues, including a large and tricky to maintain comint code.

I'd suggest to implement some very lightweight protocol, based on sexp or yojson, and fully specified by a typed schema in OCaml; we have enough experience already to understand that a model like the current one provided by SerAPI / jsCoq works well enough, and in fact was co-designed by @cpitclaudel .

The protocol is very easy, you have 4 commands Add, Query, Check, Cancel , which can be location-based (à la LSP) or sentence based, and then a few responses such as Goals, Cancelled, Ack.

Note that this kind of protocol avoids many tricky points with the XML one.

Another choice is just to have PG use LSP, I dunno, this would require more work.

This would also open the way to query for other interesting info, which is not possible today.

Handling of coqc output is a separate issue, but usptream is working on it.

Let me know what you folks think.

List of relevant issues:

• Every command to Coq also sends "Show." and gets error "This command requires an open proof." #458
• Why does PG show stale goals? #568
• Goal Display Changes in Coq 8.8 #212
• [coq] On goal display and silent mode. #188
• error highlighting was recently broken #614
• PG shows warnings without indication of the code they belong to #548
• PG is unusable when -w is passed to Coq via _CoqProject #113
• Proof state not refreshed after Admitted #103
• some idtac output printed multiple times #94
• [coq] On goal display and silent mode. #188
• coq compilation warnings not displayed for 8.6 #139
• allowing multiple active scripts #199
• Goal diff support #381
• https://github.com/ProofGeneral/PG/issues?q=is%3Aopen+is%3Aissue+label%3A%22pg%3A+async%22

[Matafou]

We definitely need to do something like that.

1. find the time to implement the main loop (reuse the work done by psteckler?)
2. accept dependency with a plugin (serapi or a simpler one as suggsted by @ejgallego)

I am willing to participate. Although my short future (few months) is quite busy.

[ejgallego]

I don't know enough internals as to know how hard would it be to adapt PG, last time I looked the work done in the async branch was way too complex for what's needed, for example see @cpitclaudel elcoq.el for a much simpler model. Basically all you want is a state machine.

I am talking here of creating a protocol for PG that we will ship in core Coq, so no plugin dependency needed.

[ejgallego]

You could always do a prototype with SerAPI of course, if you think that provides a good enough setup; once you are happy we can add to Coq the protocol, but without the serialization parts, so mainly Query would output text [or maybe HTML]

[Matafou]

I just had a look at elcoq.el and it seems indeed quite simple and nice.
I will give it a try when I have time, to better understand. In particular I want to evaluate how easy debugging is this model.

[Matafou]

For the format of output for Query I don"t know. @cpitclaudel @erikmd do you have an opinion? How is the rendering of [html | xml | sexp]-ified terms and goals?
Can we have something fast and:

• good presentation of terms (indentation, highlighting)
• still have intuitive copy-pasting / clicking on terms?
  I understand that in a web browser this is all fast and css configurable but I don't know how much emacs is ready for this.

[hendriktews]

The simple protocol, you are talking about - does it have a name? Is it implemented already somewhere? Where can I read the specification?

[ejgallego]

@Matafou the format of query for now can be string, one important property of query is that it is stateless, usually you'd like to put all printing options on query.

@hendriktews , for now it doesn't really have a protocol, the jsCoq / SeraPI protocol is the same, but we could call it elcoq once we make it work with Coq.

I think SerAPI can be a good starting point, you can check SerAPI docs they are usually OK [pyCoq will also implement some very similar API soon], but in my view the development of the protocol should be co-dependent with the changes in PG, so we should be free to evolve it.

For example as I mentioned we should maybe make the calls take a position and not a statement id as to relieve emacs from synchronizing that stm_id table.

I'd be happy to provide a prototype if you folks would need it.

[Matafou]

For example as I mentioned we should maybe make the calls take a position and not a statement id as to relieve emacs from synchronizing that stm_id table.

I don't understand. coq would be aware of positions in the buffer? But positions often change so that would mean coq is also aware of edition events?

I second Hendriks question: is there a documentation on stm + protocols for complete beginners? I think I need a fresh look at all this.

[ejgallego]

I don't understand. coq would be aware of positions in the buffer? But positions often change so that would mean coq is also aware of edition events?

That's how most modern protocol works, you relay edits in some way; see LSP. You can also work sentence-based, as you prefer. But indeed, it is hopeless for editors to understand PL structure with current tech in a complete way.

I second Hendriks question: is there a documentation on stm + protocols for complete beginners? I think I need a fresh look at all this.

There is of course serapi documentation, and LSP documentation, but there is nothing too fancy there, the devil is in the details. IMHO it is better to do a session in a Coq call and see the thing working, or please ask specific questions if you have some.

[hendriktews]

I don't understand. coq would be aware of positions in the buffer? But positions often change so that would mean coq is also aware of edition events?

As far as I understood from briefly reading SerAPI, when the user changes something in the buffer, the UI needs to send Cancel commands for all stuff following the change. When the user finishes, the UI can Add it again and let Coq parse it. This way, the positions are always synchronized between the UI and Coq for the parsed portion.
If one wants to permit changing proofs without canceling the declarations that follow the proof, one could also work with relative positions...

[hendriktews]

@hendriktews , for now it doesn't really have a protocol, the jsCoq / SeraPI protocol is the same, but we could call it elcoq once we make it work with Coq.

OK, I am still trying to understand the actual proposal. Let me rephrase: You propose to design a new protocol elcoq based on SerAPI. The design should/could happen in parallel with the implementation in Emacs/Proof General and in Coq. You and/or the Coq team would volunteer to work on the Coq side. Did I get that right?

Direct support from the Coq team would indeed change the motivation on the Proof General side, I believe...

[ejgallego]

when the user changes something in the buffer, the UI needs to send Cancel commands for all stuff following the change

The current design is a bit different, you send (Cancel ) only for the updated sentence, then Coq will answer with the list of statements that are not valid anymore. So the job of the IDE is easier, just relay the invalidation event, and when a Cancelled event arrives, consider there sentences also invalid.

Synchronizing the positions indeed can be done in many ways.

OK, I am still trying to understand the actual proposal. Let me rephrase: You propose to design a new protocol elcoq based on SerAPI. The design should/could happen in parallel with the implementation in Emacs/Proof General and in Coq.

Indeed, I propose we move PG to a protocol that solves all the problems we currently have, fully supported by the Coq team and included in Coq. elcoq (which was done by @cpitclaudel ) is an example of such protocol, but don't feel bound by it, we could also use something such as LSP, or a modification of this one. Whatever it works best for you folks.

I think we should indeed iterate on the design a bit, so we are sure we have a clear model and we have a bit of freedom to fix possible pain points.

You and/or the Coq team would volunteer to work on the Coq side. Did I get that right?

Correct.

[Alizter]

coq-lsp is in a usable state now. I think it would be a good time to start experimenting with PG going through lsp. I know PG has many features that would be useful for other UIs so it would be good to start upstreaming these.

[erikmd]

Thanks @Alizter for your heads-up !

This indeed deserves some dedicated discussion in some upcoming PG telco, Cc @Matafou @hendriktews

A few questions/comments:

• A migration to coq-lsp looks like a more tractable path than adapting the current code of the XML-based async branch.
• I employed the term "migration" but maybe "extension" is a better word, as we strongly focus on backward compatibility (a new release of PG should always preserve compatibility w.r.t. all Coq versions as old as 8.4, AFAICT)
• so I guess we'll need to add some layers and implement a kind of Adapter, to support both backends
• BTW @cpitclaudel: I believe you had implemented a PoC relying on lsp (?) then is it available, and what's its status?

[Alizter]

• A migration to coq-lsp looks like a more tractable path than adapting the current code of the XML-based async branch.
• I employed the term "migration" but maybe "extension" is a better word, as we strongly focus on backward compatibility (a new release of PG should always preserve compatibility w.r.t. all Coq versions as old as 8.4, AFAICT)
• so I guess we'll need to add some layers and implement a kind of Adapter, to support both backends

I agree. I'm not sure how PG interacts with Coq today (I vaguely know it is going through coqtop). LSP should allow for a more direct interface.

[erikmd]

I'm not sure how PG interacts with Coq today (I vaguely know it is going through coqtop).

Exactly. To give a few more details,

• PG first does some path resolution to find the coqtop binary
• then it queries its --version and normalizes/remembers its output
• then open a background process, thanks to scomint.el , a simplified lisp API of comint.el, and proof-shell.el
• and whenever the coqtop process is open, we can see all the background requests/responses in the *coq* buffer

[cpitclaudel]

BTW @cpitclaudel: I believe you had implemented a PoC relying on lsp (?) then is it available, and what's its status?

It was a layer using SerAPI (which was very nice to program against), not LSP. It's here: https://github.com/cpitclaudel/elcoq

LSP doesn't have support for interactive theorem proving, so it's really coq-lsp that we are going to support (not plain LSP). Are there docs on how to communicate to Coq where we are in the file, where we want to process until, or maybe where the user is looking, etc?

[Alizter]

LSP doesn't have support for interactive theorem proving, so it's really coq-lsp that we are going to support (not plain LSP).

Yes, when I mentioned LSP I was really meaning coq-lsp.

[monnier]

LSP doesn't have support for interactive theorem proving, so it's really coq-lsp that we are going to support (not plain LSP). Are there docs on how to communicate to Coq where we are in the file, where we want to process until, or maybe where the user is looking, etc?

I know nothing about `coq-lsp`, but you could probably reproduce the PG workflow by only telling the `coq-lsp` server about the section of the buffer that's currently "processed", and just adding/removing chunks at the end as the user moves the boundary. [ The LSP protocol is based on the idea that the client sends to the server the text of the buffer/file, as well as any subsequent modifications to that text and the LSP server keeps a local copy of that text. Usually that text is the whole file/buffer, but we could just as well decide to pretend that it's only the part of the buffer before the boundary, and when the user moves the present it to the LSP server as if the user had just inserted/deleted text at the end. ] Not sure if that would give you the needed info to display the current proof state when you're in the middle of a proof, tho. Stefan

[ejgallego]

You can get a working setup with pure LSP , however that becomes a bit annoying due to having to show goal info using the hover call. coq-lsp provides two extensions to help clients, see

https://github.com/ejgallego/coq-lsp/blob/main/etc/doc/PROTOCOL.md

There are very close to what lean does today, well, Lean's infoview has a much more complex protocol for some advanced features.

Another important thing that you may want to do in proof general is specifying the range of the document you'd like to be checked. coq-lsp by default will check the whole document, but the LSP specification 3.18 will include a range parameter in the Pull Diagnostics request, so indeed I'm happy to add support for this.

coq-lsp underlying checking engine already support (and relies) on checking just a part of the document.

So PG would basically use standard LSP + proof/goals request when it wants to display info about it.

IMVHO letting coq-lsp check the full document is not as wasteful as it seems, and in fact tends to speed up the proof process quite a bit, recall that coq-lsp is incremental so the common case when editing should be that you don't recheck the document, but Coq still needs a few changes to make this work better.

But indeed, if you have very long proofs, I agree that a mode with Pull Diagnotics + range is more convenient.

[ejgallego]

Another model coq-lsp can support is actually not to check anything, until the clients (in this case Emacs) sends the goals/info request. However that adds IMHO a bit of latency for most users, but of course it depends on what your constraints are.

I guess once we are a bit more mature we will support performance / powersaves mode, with the tradeoff of CPU vs latency.