[ccing Maxime as he is working on the core Coq document platform these days]
Clément Pit-Claudel <clement....@gmail.com> writes: > This. At least from my short experience, the protocol offered by > SerAPI (well, the one that was offered a year ago ^^ I don't know if > it changed) is much more robust than the XML-based one offered with > Coq. The question IMVHO is, how to move forward? It seems to me that we have quite a lot of separate pieces in our hands: 1. ProofGeneral `master`, which includes a lot of useful code related to project management, completion, etc... as well as the code for interacting with coqtop, 2. ProofGeneral `async`, which includes several reworks and a mode to interact with the XML protocol, 3. company-coq, providing many nice extensions to 1 (and 2?) 4. Coq's XML protocol. Not actively developed but maintained; some technical problems make it hard to evolve, 5. SerAPI, a maturing (4th major release is at the door) language server for Coq, actively developed and used, and Emacs-friendly, 6. elcoq, a proof of concept on how to talk to SerAPI [could be simplified these days due to some improvements to the protocol I think] 7. Dune Project specifications for Coq, which are very experimental but should provide a more programmatic version of _CoqProject, 8. and we will have soon: a LSP server, which will hopefully implement a nice subset of the protocol including project management. Thus, it seems to me that one possible way to move forward would be to start from 2, stripping all the XML protocol support in favor of something inspired by 6, using 5 as the language server. SerAPI has reached the stage where it could be integrated into the main Coq distribution if so wished for 8.10, it has been in OPAM for a while. IMHO LSP and SerAPI are already close enough as to allow PG to move from one to the other seamlessly. SerAPI itself will likely switch to LSP at some point in the future, at least for document manipulation, but first we need to find an intern interested in talking to the LSP folks as to propose a few extensions needed for interactive programming, which they may not be very receptive of, so it has to be done carefully. Note that some other interactive proof assistants in the "Paris/Ocaml" area on which I had some influence are adopting LSP [we started with SerAPI but SerAPI itself will move to LSP at some point] They'd love to use PG, and IMHO here we have some space to adopt a kind of "standard". I can help with all the tasks related to Coq, however my elisp-fu is pretty bad, however I am a competent user and I am using PG a lot for work so I could test for sure. Cheers, E. _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
