Re: [PG-devel] Supported version of Emacs
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 a écrit : > > [ccing Maxime as he is working on the core Coq document platform these days] > > Clément Pit-Claudel 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
Re: [PG-devel] Supported version of Emacs
> I guess at some point it would make sense to tie PG to an specific Coq > range; I think the required changes could be made in the range of Coq >= > 8.8. FWIW, Debian stable has Coq-8.6 (which is only about 2 years old), so that's what I use on some of my machines. Stefan ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] SerAPI
Looking at SerAPI, I'm wondering about the choice of "sexp". I know it may sound odd to want something else than sexps when working in Elisp, but in reality sexps only work well if they use *exactly* the same syntax. E.g. in https://github.com/ejgallego/coq-serapi I see: (Query ((sid 3) (pp ((pp_format PpStr Goals) > (Answer 3 Ack) > (Answer 3 (ObjList ((CoqString > "\ >\n n : nat\ >\n\ >\nn + 0 = n" > (Answer 3 Completed) which seems to show that the strings don't use the same escape syntax as Elisp. This little detail will likely end up forcing the Elisp side to either re-implement a sexp-reader by hand (in Elisp, which will be slowish), or require ugly hacks to try and pre-process the answer before passing it to the sexp reader (or post-process the sexp), which will likely always end up flaky. Same thing when it comes to turning Elisp sexps into the print representation of SerAPI sexps, of course. This said, I don't see any hand parsing or pre/post processing tricks when reading SerAPI's sexps: I only see the prin1-to-sexp hack which works around the nil-vs-() difference. So maybe the syntax is closer to that of Elisp than shown in the README.md. Otherwise I see 2 convenient options: tweak the sexp syntax so it is a 100% subset of that of Elisp or use some other widespread standard such as XML or JSON (modern Emacsen can link to efficient parsers of those two). The first option is of course more convenient for Emacs, but I understand that the second is more convenient for all the non-Emacs clients and it's not that bad for Emacs. Stefan ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] SerAPI
> This said, I don't see any hand parsing or pre/post processing tricks > when reading SerAPI's sexps: I only see the prin1-to-sexp hack which > works around the nil-vs-() difference. So maybe the syntax is closer to > that of Elisp than shown in the README.md. Indeed; in practice it works OK. There's a minimal example of an IDE implementation based on SerAPI at https://github.com/cpitclaudel/elcoq/blob/master/elcoq.el Clément. On 30/11/2018 10.46, Stefan Monnier wrote: > Looking at SerAPI, I'm wondering about the choice of "sexp". I know it > may sound odd to want something else than sexps when working in Elisp, > but in reality sexps only work well if they use *exactly* the same > syntax. E.g. in https://github.com/ejgallego/coq-serapi I see: > > (Query ((sid 3) (pp ((pp_format PpStr Goals) > > (Answer 3 Ack) > > (Answer 3 (ObjList ((CoqString > > "\ > >\n n : nat\ > >\n\ > >\nn + 0 = n" > > (Answer 3 Completed) > > which seems to show that the strings don't use the same escape syntax as > Elisp. This little detail will likely end up forcing the Elisp side to > either re-implement a sexp-reader by hand (in Elisp, which will be > slowish), or require ugly hacks to try and pre-process the answer before > passing it to the sexp reader (or post-process the sexp), which will > likely always end up flaky. > > Same thing when it comes to turning Elisp sexps into the print > representation of SerAPI sexps, of course. > > This said, I don't see any hand parsing or pre/post processing tricks > when reading SerAPI's sexps: I only see the prin1-to-sexp hack which > works around the nil-vs-() difference. So maybe the syntax is closer to > that of Elisp than shown in the README.md. > > Otherwise I see 2 convenient options: tweak the sexp syntax so it is > a 100% subset of that of Elisp or use some other widespread standard > such as XML or JSON (modern Emacsen can link to efficient parsers of > those two). The first option is of course more convenient for Emacs, > but I understand that the second is more convenient for all the > non-Emacs clients and it's not that bad for Emacs. > > > Stefan > signature.asc Description: OpenPGP digital signature ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Supported version of Emacs
Pierre Courtieu writes: > I am all for it, where can I find the serapi documentation please? That's a good point, the documentation is fairly sketchy as we didn't see the need to make the API stable yet. In fact one of the problems Paul has pointed out was lack of specification of the XML protocol [which was 100% undocumented when the effort started IIRC] I will add some specification for the 8.9 version, any recommendation on to best document such a protocol? As the protocol is programmatically derived from https://github.com/ejgallego/coq-serapi/blob/v8.9/serapi/serapi_protocol.mli I think I will use OCaml's `odoc` format. Binaries command line is reasonably documented with --help. Cheers, E. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] SerAPI
Hi Stefan! Stefan Monnier writes: > Looking at SerAPI, I'm wondering about the choice of "sexp". I know it > may sound odd to want something else than sexps when working in Elisp, > but in reality sexps only work well if they use *exactly* the same > syntax. E.g. in https://github.com/ejgallego/coq-serapi I see: > > (Query ((sid 3) (pp ((pp_format PpStr Goals) > > (Answer 3 Ack) > > (Answer 3 (ObjList ((CoqString > > "\ > >\n n : nat\ > >\n\ > >\nn + 0 = n" > > (Answer 3 Completed) > > which seems to show that the strings don't use the same escape syntax as > Elisp. This little detail will likely end up forcing the Elisp side to > either re-implement a sexp-reader by hand (in Elisp, which will be > slowish), or require ugly hacks to try and pre-process the answer before > passing it to the sexp reader (or post-process the sexp), which will > likely always end up flaky. The choice of serializer is due to sexp being one of the most mature serialization backends in the OCaml world. [SerAPI serializes > 1000 types theses days] A couple of points: - the above example is "beautified" as to make it look better, actual machine-friendly sexps are slightly different: $ sertop --printer=sertop (Add () "Lemma addn0 n : n + 0 = n. Proof.") (Exec 3) (Query ((sid 3) (pp ((pp_format PpStr Goals) => (Answer 4(ObjList((CoqString"\n n : nat\n\nn + 0 = n" - we have our own custom sexp printer and IMHO there will be no problem in getting SerAPI to output the right quoting for Emacs. > Same thing when it comes to turning Elisp sexps into the print > representation of SerAPI sexps, of course. We can also add to SerAPI a special parser / unquoter for Emacs. IMHO we should handle this in the OCaml land. That being said, if Emacs does prefer a different serialization format that'd be possible too. > Otherwise I see 2 convenient options: tweak the sexp syntax so it is > a 100% subset of that of Elisp or use some other widespread standard > such as XML or JSON (modern Emacsen can link to efficient parsers of > those two). The first option is of course more convenient for Emacs, > but I understand that the second is more convenient for all the > non-Emacs clients and it's not that bad for Emacs. Actually I do prefer 1 as XML or JSON have some other pitfalls wrt serialization. For example the LSP mode of SerAPI uses JSON but it cannot output structured data easily. Cheers, E. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Supported version of Emacs
Stefan Monnier writes: > FWIW, Debian stable has Coq-8.6 (which is only about 2 years old), > so that's what I use on some of my machines. Now that you have mentioned it, we consider this pretty unoptimal and we agreed on removing Coq from Debian due to the perils of shipping an outdated version :( :( But I couldn't find the section on the policy manual that states "outdated" is RC. But indeed, the version even in unstable is way too old [and likely unsound] Cheers, E. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] SerAPI
> This little detail will likely end up forcing the Elisp side to either > re-implement a sexp-reader by hand (in Elisp, which will be slowish), > or require ugly hacks to try and pre-process the answer before passing > it to the sexp reader (or post-process the sexp), which will likely > always end up flaky. I would just like to remark that the focus of SerAPI is that when some friction arises between the client and the server, it should always be SerAPI the one to make the effort to adapt so life of the client is easier. I think I like this approach for 2 reasons: - clients have already an enough hard time dealing with display, the user, etc... more complexity in the clients is not good, and for sure clients are going to be more constrained, - in this case SerAPI has both full control and synchronous access to the prover, so it has a much better time implementing any kind of klugde. Cheers, E. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Supported version of Emacs
> Now that you have mentioned it, we consider this pretty unoptimal and we > agreed on removing Coq from Debian due to the perils of shipping an > outdated version :( :( I find it perfectly adequate for my needs, FWIW. And I'd be annoyed to have to install Coq manually. 2 years old sounds like a really weird definition of outdated to me. To take a "random" example, ProofGeneral tries to be compatible with Emacs-24.3 which is 5 years old. Stefan ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
