Pierre Courtieu <pierre.court...@cnam.fr> writes: > I took a quick look at serapi's github. It looks very nice but is > serapi still in "alpha" and "subject to change"?
I feel like this may be the moment to make it a bit more "stable". However, I would expect adding PG support to SerAPI to require at least one or two Coq releases where it would be marked "experimental" and thus subject to change. IMHO we want to leave space to fix / improve / evolve aspects of the protocol before declaring it "stable". In fact, "stability" may be a diffuse notion when advanced features are needed, and I would dare to say that a futile goal in state of the art IDE/UI. For example, I understand Isabelle doesn't have any stability guarantee on the protocol level, thus they have to couple the IDE with the prover. > 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. While I understand and I am indeed sympathetic to that position, I would be quite worried if in 10 years it turns out we are using the same IDE protocol than we are using today. Likely by then, most Coq users would have switched to a different system that would provide them with more advanced functionality. IMHO it is impossible to have that kind of stability and yet serve the needs of that large-scale proof development for example. That's my opinion of course. > Consider that coq old REPL stayed stable for more than 20 years (and > still is). Well, it has not been 100% "stable", but more importantly, second, it is easy to make a REPL "stable", as well, it basically provides no features at the protocol level. > Imho this is why pg survived and all other technologies died for now: What do you mean by "all other technologies"? Maybe I got confused by the "all" quantifier, but I see quite a few "other technologies" alive and doing pretty well. > 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. I can understand that point of view, but I also understand the point of view of users that are driven away from Coq due PG / CoqIDE being the only IDEs available. To many eyes the "stability" of PG is seen as a great failure / pitfall of PG not as something positive. And while I (we) love Emacs and it is my primary work tool, I am afraid the group of PG users is getting smaller and smaller, so it could be well that in 10 years we are just a handful of people using it. Well, if in 10 years it is still stuck at this level of functionality I am sure I will have to move on to a different tool set. Frankly, in UI terms, 10 years is a ridiculous time span. Not even key Emacs packages these days [company, spaceemacs, magit] have something close to that requirement. In my view what should happen is that PG / Coq development is properly coordinated, so evolution and change is possible, but controlled. Cheers, E. _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
