Cool! (Though, wouldn't it have been easier to write the IRC bot in OCaml ;-) How do you build coqpy.m4? I'm not sure what a 'Make' file is.
Edward Excerpts from Tom Prince's message of Fri Apr 06 18:57:25 -0400 2012: > 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
