On 16/06/16 00:07, Clément Pit--Claudel wrote: > On 2016-06-15 17:51, Makarius wrote: >> Concerning the "new" prover APIs of Coq and Isabelle in general: I was >> in contact with Enrico Tassi when he introduced this for Coq -- it was >> part of our Paral-ITP project at that time. My general impression is >> that the new Coq API is more conservative than the PIDE protocol of >> Isabelle: PIDE is quite demanding on the other side to process a lot of >> information in real-time. > > Not sure whether this is what you had in mind, but there does exist a PIDE > implementation built on top of the new Coq API > (https://bitbucket.org/coqpide/pidetop). It's used by at least one Coq IDE > (Coqoon — it's pretty cool, btw).
Yes, that is by Carst Tankink -- I was working with him over 6 months,
before I left France. Later the Coqoon guys also joined the move,
because I encouraged them to do that, but it never became first-class
for Coq.
You see, I am somehow behind many of the prover IDE modernization
projects, but not all of them.
Ultimately, what counts is what really works, and what is really maintained.
Makarius
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
