The Coq mailing list

[Thery Laurent <thery AT ns.di.univaq.it>]

Hi,

> For some time, Laurent Théry had a nice example available from his web-page 
> (sos.zip).  It seems he removed it because the functionality is superseded by 
> micromega, but you could ask him
> to send you the example for inspiration.  It is about connecting with csdp to 
> answer questions
> about polynomial expressions being positive.

The code of the sos is still available at:

ftp://ftp-sop.inria.fr/marelle/Laurent.Thery/sos

Here are few hints to help understanding the code.
The connection with an external tool is done using

The skeleton of the tactic that is used looks like this:

Ltac mytactic :=
  match goal with |- ?t =>
    ....
    let x := external "psos_wrapper" ""  t in
    ...
  end

it takes the goal (t) and sends it to the external command
psos_wrapper.
The result of the external command is a coq term (x) and
can be used later to actually do something

To exchange term (t as input and x as output) Coq uses an XML format.

You can see in psos_wrapper.ml how we can deal with this formal in Ocaml
using the Xml library  xml-light. The wrapper decodes the request, call 
the external command csdp via the Ocaml Sys.command and then encode
the result for Coq.

The documentation for the external command in Coq is here:

http://coq.inria.fr/doc/Reference-Manual011.html#@default680


--
Laurent