On Sun, 08 Apr 2012 14:24:45 -0400, "Edward Z. Yang" <[email protected]> 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 editor. Tom _______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
