Re: [PG-devel] SerAPI
Hi folks, I thought I'd give an update on what has been going on w.r.t. SerAPI and its successor. First, we added a bit of documentation, it is not a wonder, and moreover, it will change, but here it is: http://ejgallego.github.io/coq-serapi/priv-serapi/Serapi_protocol/ The main change is that SerAPI will converge to something pretty much isomorphic to LSP with some extensions for proving. There will be more news about this in the summer, but I don't expect that clients supporting SerAPI today would have to do any significant change if implementing the recommended architecture. Recommended implementation architecture: For SerAPI / Coq-LSP, the recommended implementation architecture is: - the document is considered as a whole unit, - updates are in the form of diffs sent to the server, - sentences are identified by their position in the buffer, - all meta-info [goals, etc...] is functional and must be queried for. As of now, SerAPI clients have a slightly harder time as they must keep the document as a list of sentences and they also have to maintain a table position to sentence id; this will be lifted soon. Best regards, Emilio ___ 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] 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
[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
