I am all for it, where can I find the serapi documentation please? Cheers,
Le ven. 30 nov. 2018 à 03:15, Emilio Jesús Gallego Arias <e...@x80.org> a écrit : > > [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 _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
