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 code. Tom _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
