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? > 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.
signature.asc
Description: OpenPGP digital signature
_______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel