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).

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