Hi Pierre, Pierre Courtieu <pierre.court...@cnam.fr> writes:
> 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,...). So indeed I would like to say that yes, that we could keep this stable for 10 years, but I'm afraid that it'd be hard to justify the use of developer resources for that. >> 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. Well, I am not sure the Coq team is aiming to maintain 10-years compatibility on the protocol, neither in the .v files, we didn't discuss that anyways, but for sure if we do I will strongly oppose; if I put in one hand: - the advantages of keeping the protocol static, - the advantages of coupling the protocol, I do believe users are much better served by the second approach. Let's face it, Isabelle IDE is years ahead of Coq on terms of features, the coupling approach was a key point. In fact they even removed the REPL support; AFAICT a few people complained but the large majority of users is quite happy with the provided feature set. On the other hand we have people and mathematicians deflecting from IDEs due to poor support for Coq. > 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. Well, as I mentioned any change in the protocol should of course properly justified and be coordinated with the IDE maintainers, and IDEs themselves should be added to Coq's CI. But it seems to me pretty logical that if you want to use Coq's 8.14, you may need to use PG 2022. I won't commit to an unachievable / unrealistic policy, what is the problem in coordinating? It seems to me that we have huge problems coordinating among ourselves, for example many of VSCoq pains could have been avoided with a bit of discussion with the Coq devs. > From https://coq.inria.fr/related-tools: This list should be indeed updated: > 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 I am not sure these are dead, but their language server `pidetop` was [until last week] in Coq's CI and thus maintained for 8.10. > the ProofWeb online web interface for Coq (and other proof > assistants), with a focus on teaching; *********** DEAD (Welcome to Coq > trunk (Nov. 2006)) No idea about this, but note that I think it used coqtop so the protocol was not to blame. Again what it seems to blame here was poor coordination with upstream, but admittedly in 2006 we didn't have github. > 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? PeaCoq was ported to SerAPI and indeed should work in 8.10, but indeed Valentin has been a bit busy to do another release. > vscoq A Visual Studio based interface developed in 2016. *** README > says "v8.5" ? supports probably 8.8. vscoq speaks the XML protocol so it should work with recent Coq; however there were some implementation problems due to LSP/Coq XML impedance so we hope to revive it once the Coq's LSP server is alive. > jscoq A port of Coq to the browser; runs standalone using js_of_ocaml. > ** looks up to date except for v8.9beta It is up to date until 8.10, however my policy is not to release new versions until the official release is out. Porting has been pretty painless so far, but it is tied to the ML API > 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? Yes they will; also it is a bit of apples-to-oranges comparison. > 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. Thanks! Indeed I understand your point of view, on the other hand progress must be made in terms of IDE support. The 10-years compatibility policy seems really strange and unachievable to me, so I dunno. In 10 years I'd dare to say that we won't even have a coqtop anymore in its current form. Cheers, E. _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
