Clément Pit-Claudel <clement....@gmail.com> writes: > On 03/12/2018 11.57, Emilio Jesús Gallego Arias wrote: >> In the first case, my opinion (and the one of quite a few of my >> colleagues) is yes, clearly ahead. > > But can you give concrete examples of extra features that they have?
I will mention three that already make a large difference: - Isabelle / PIDE understands complete projects; - reliable async support and integration with external tools; - better error reporting and handling. > And, re the coupling, are these worth being stuck with a single editor? Indeed not for me, I wish Coq didn't have to go that way. But most Isabelle users I talk to seem to prefer the tradeoff of having a single nice working IDE over 2 less featured ones. And they ones I've talked to do and that have done some Coq too, clearly state that they miss Isabelle's IDE _a lot_. Note that I am not advocating for coupling at all, but I cannot either accept 10-years immutability; in the end, if you want advanced features you need to allow for some room for development. Cheers, E. _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
