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.

Attachment: 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

Reply via email to