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.


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" <> 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://>. 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

Reply via email to