Le lun. 3 déc. 2018 à 13:11, Emilio Jesús Gallego Arias <e...@x80.org> a écrit : > > I feel like this may be the moment to make it a bit more "stable".
Good news! > 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. Of course. > 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. Of cours evolution is equally important. Please correct "stable" by "backward compatible". The changes should not make valid commands become invalid, or at least before having it tagged "obsolete" for several years. Actually coq has a very good policy about backward compatibility for *commands*, it should be exactly the same for protocol commands (Add, Edit,...). > 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. Yes this is the exact opposite of what the coq team is aiming at. So the compatibility policy should not be the same. > > 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. Enriching the protocol is not a problem (and should far enough for 10 years of new features I guess), but if you say all of a sudden: "the sexpr now take curly brackets", or "the command Add takes one more mandatory argument" or "now the protocol is sent with reverse polish notation to avoid parenthesis" then everything breaks and every tool based on your protocol is forced to do gory checkup at start or be incompatible with older coq versions. > Maybe I got confused by the "all" quantifier, but I see quite a few > "other technologies" alive and doing pretty well. I consider "dead" an ide that cannot follow coq's release cycle (because people will switch to another one), and I consider as "overheating" IDEs the ones that do not support coq beta versions within a month: From https://coq.inria.fr/related-tools: " The Proof General Emacs/XEmacs interface by David Aspinall with Coq support by Pierre Courtieu; **** works for v8.9beta and master and at least from v8.4 The Coqoon Eclipse plugin for Coq development (based on Wenzel's asynchronous PIDE framework); **************** Support for v8.7 and v8.8 is highly experimental The Coq PIDE Jedit (proof of concept) plugin for Coq development (also based on asynchronous PIDE framework); ***** DEAD the ProofWeb online web interface for Coq (and other proof assistants), with a focus on teaching; *********** DEAD (Welcome to Coq trunk (Nov. 2006)) the PeaCoq online web interface for Coq (by Valentin Robert); ******* officially supports 8.5. There is v8.8 branch but not a lot of things commited in it, lack of dev time? ProverEditor is an experimental Eclipse plugin with support for Coq; ********* DEAD " **More Found in cocorico: " vscoq A Visual Studio based interface developed in 2016. *** README says "v8.5" ? supports probably 8.8. jscoq A port of Coq to the browser; runs standalone using js_of_ocaml. ** looks up to date except for v8.9beta CoqTail CoqTail is a vim plugin aiming to bring the interactivity of CoqIDE into your favorite editor. ** looks up to date except for v8.9beta " So: 1) more deads than alives 2) the only officially supporting ides for v8.9 currently are coqide (with a problem with opam) and pg. 3) the last three are very promising BUT they are in a critical moment: will they adapt easily to v8.9? Note that 8.9 and master compatibility took 0 commit in pg. Of course new features may not be supported at first but *at least* one can play old proofs with the new coq. I remember having to support the new "[goalid]: {" syntax. I am not sure I I think your work on protocols is great, please take all this as passionate comments. I do really want to see more tools around and you are by far the one who contrinbutes the most to that purpose. Best Pierre > > > 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
