On Fri, 06 Apr 2012 12:00:39 -0400, "Edward Z. Yang" <ezy...@mit.edu> wrote:
> Yes, this is another approach that we have considered.  Actually, in this case
> I would have wanted to cut out the middleman, lib-ified Coq and just run 'open
> Coq' and directly do this (this may be worth doing anyway, independent of this
> conversation, although I don't have infinite time).

I've done a *tiny* littlbe bit of making coq usable like a library, to
write roosterbot <git://gist.github.com/1343032.git>. It doesn't do a
whole lot yet (and doesn't deal at all with proof state), but it does
show how to get an external program interfacing directly with the coq

ProofGeneral-devel mailing list

Reply via email to