Some questions wrt porting Proof General to SerAPI about coq-serapi HOT 2 CLOSED

Hey Clément,

Wow!! I cannot wait to play with your emacs tool! Thanks a lot, indeed, the only way to validate something like SerAPI is have somebody using it. As you know nothing is fixed so any change you think makes sense will hopefully find its way into SerAPI.

• async processing: Definitively we want to support async processing. I did a few experiments but currently it is hard to get it working and the interface is a bit underdocumented; I'll talk with @gares to see what to do here. Regarding feedback messages, indeed, the idea is that they can arrive at any time. In fact, I could simulate it using a thread right now, but Ocaml threading, well....

• coqtop: I guess I don't want to support all legacy stuff present in coqtop, include command line arguments. Another part SerAPI won't use is coqtop's current printing infrastructure. There also exist some problems with the exception API.

• _Coqproject/Flags: IMHO this is largely orthogonal to SerAPI. My view is that a _Coqproject backend will send the proper configuration commands to SerAPI. For instance, you have (Control (LibAdd )) now. Notice this: some flags in a _CoqProject (like loading the prelude) will create a side effect and new state id. So IMHO, you would first start SerAPI, then send the proper configuration flags as control commands. For instance, options get unset on EditAt!

  Can you open a new issue with the flags you need to use? Thanks.

• 8.5 We can make SerAPI work with 8.5, if needed, but IMHO 8.6 is close enough that it may not be worth it.

• Distribution/Merging: Wow, that is a hard one... Who is responsible of merging things in Coq? I guess we should ask them... Regarding distribution, installing SerAPI will be as hard as installing a Coq Plugin. Coq devs say they want everything to be a plugin, but on the other hand not a lot is done...

from coq-serapi.

This will be moved to the FAQ, with a few issues open:

• async support: #13
• coptop: See #19
• Support for 8.5: no, there are too many API changes for serlib, and 8.6 has been just branched, with little incentive to use 8.5 over it. However, note that the reduced jsCoq protocol will support 8.5, so it could be interesting to some.
• Distribution: after talking to coq devs, it was a possibility to merge SerAPI for 8.7, however I do not want to tie the update schedule to Coq's, so SerAPI users in 8.6 will have to install it through OPAM.

from coq-serapi.