Hi Stefan! Stefan Monnier <monn...@iro.umontreal.ca> 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
