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


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