On Sun, 08 Apr 2012 14:24:45 -0400, "Edward Z. Yang" <ezy...@mit.edu> wrote:
> Excerpts from Makarius's message of Sat Apr 07 08:43:57 -0400 2012:
> > Cutting out the middleman is a good start.  The lib-ified approach sounds 
> > more like running everything in a single OCaml process, though.  The Coq 
> > guys used to have that for CoqIde, but discontinued it for the forthcoming 
> > Coq 8.4.  There are now two OCaml progresses to interact with Coq, 
> > front-end and back-end.  There are some rudiments of a protocol for the 
> > communication, e.g. see the vicinity of 
> > https://github.com/coq/coq/blob/v8.4/toplevel/ide_intf.ml
> I'm curious why they discontinued it; is it because lack of multithreaded
> support in OCaml meant it was difficult to keep the interface responsive
> while Coq was thinking hard about a calculation?

I think the two main issues are keeping the interface responsive, and
preventing bugs or infinite loops or the like from bringing down the

ProofGeneral-devel mailing list

Reply via email to