The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Alessandro Cavalcante Gurgel wrote:
> ...
>
>      How coul we integrate our tool with Coq ? Do you have any documentation
> about support for communication with external tools ? The source are avaible
> ?
>
> Thanks,
>
> Alessandro
>
>   
The sources of Coq are available.  Communication with external tools can 
be arranged using
the XML format.  Until now, this was arranged in such a way that Coq was 
the master and could
provide data in XML format to external tools, which would in turn give 
their answer in XML format
too.

This is documented at the end of section 9.2 of the reference manual for 
Coq (http://coq.inria.fr/V8.1pl3/refman/index.html).  You will find an 
example following this
approach in the tactic developed by L. Théry to solve problems based on 
sets of inequalities between
polynomials (ftp://ftp-sop.inria.fr/lemme/Laurent.Thery/sos).

 Aside from this a few experiments were performed where Coq was piloted 
through an external
interface: Proof-General (http://proofgeneral.inf.ed.ac.uk/),
Pcoq (http://www-sop.inria.fr/lemme/pcoq/index.html),
and a direct connection to Eclipse (http://provereditor.gforge.inria.fr/).

Yves