Clément Pit-Claudel <clement....@gmail.com> writes: > On 03/12/2018 10.33, Emilio Jesús Gallego Arias wrote: >> 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. > > Is it?
Do you mean the IDE or the coupling approach? In the first case, my opinion (and the one of quite a few of my colleagues) is yes, clearly ahead. It doesn't mean it is perfect tho. For the second, I think the importance of the coupling was said by Makarius itself. >> 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. > > One significant issue is that because Coq scripts sometimes break, > library developers often need to test with multiple versions of Coq. > If each of them requires a different Emacs package, things get hard. One thing is to have a reasonable time-frame of support, which of course should be at minimum 2 protocol versions; and in fact, we should only break the protocol in case of a major problem, or even provide version negotiation. Another is to require "at least 10 years" of immutability. Cheers, E. _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
