I took a quick look at serapi's github. It looks very nice but is serapi still in "alpha" and "subject to change"?
This is important. I don't want to switch to a protocol that will not be backward compatible for a long time. By long time I mean >= 10 years. Consider that coq old REPL stayed stable for more than 20 years (and still is). Imho this is why pg survived and all other technologies died for now: 1) almost no effort was needed to keep things working 2) each pg version worked for several versions of coq spanning over 5 years at least. This second point is not significant for coqide since it is distributed with coq but it is a huge problem for other IDEs. The protocol seems very nice and would greatly simplify pg's code but I am not going to invest time on it if it is not guaranteed to be still working in 10 years. I would better stay with the old and rough REPL (which will stay in the source for some years anyway because old versions of coq do not speak serapi). Sorry to sound like an old grumpy conservative but I think this is really important. P. Le lun. 3 déc. 2018 à 10:36, Pierre Courtieu <pierre.court...@cnam.fr> a écrit : > > > > Le dim. 2 déc. 2018 à 02:50, Emilio Jesús Gallego Arias <e...@x80.org> a > écrit : >> >> Pierre Courtieu <pierre.court...@cnam.fr> writes: >> >> > I think the most important is that your documentation should contain or >> > point to a documentation of coq stm. >> >> Why? I'd rather document SerAPI by itself, why to expose the low-level >> document manager? >> >> Note that the README is not accurate anymore, as SerAPI is not tied to >> the STM anymore, so yeah this may be confusing. > > > Does serapi avoids being based on a notion of document model? Last I checked > about stm it was based on an implicit DAG roughly representing the lemmas of > the file. Don't we need something like that to use serapi correctly? > >> I've already wrote a fair chunk of up-to-date documentation for it, >> hopefully will make it into the main branch soon. > > > Cool! > > >> >> Cheers, >> E. _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
