The Coq mailing list

[Valentin Robert <valentin.robert.42 AT gmail.com>]

Clément: Here is a sample of a short session interacting with coqtop 8.5beta2. The <call> is what you write, then upon pressing Enter, coqtop sends the <value>.

vrobert@localhost ~$ coqtop -ideslave -main-channel stdfds

<call val="Init"><option val="none"/></call>

<value val="good"><state_id val="1"/></value>

<call val="Add">

  <pair>

    <pair>

      <string>Theorem t : forall n, 0 + n = 0.</string>

      <int>0</int>

    </pair>

    <pair>

      <state_id val="1"/>

      <bool val="false"/>

    </pair>

  </pair>

</call>

<value val="good"><pair><state_id val="2"/><pair><union val="in_l"><unit/></union><string></string></pair></pair></value>

<call val="PrintAst"><state_id val="2"/></call>

<value val="good"><gallina begin="0" end="32"><theorem begin="0" end="32" type="Theorem" name="t"><apply begin="12" end="31"><operator begin="12" end="31" name="forall"/><constant begin="19" end="20" name="n"/><apply begin="22" end="31"><operator begin="22" end="31" name="_ = _"/><apply begin="22" end="27"><operator begin="22" end="27" name="_ + _"/><token begin="22" end="23">0</token><constant begin="26" end="27" name="n"/></apply><token begin="30" end="31">0</token></apply></apply></theorem></gallina></value>

<call val="Quit"><unit/></call>

vrobert@localhost ~$

- Valentin

On Wed, Jul 1, 2015 at 9:30 PM Clément Pit--Claudel <clement.pit AT gmail.com> wrote:

Hi Enrico,

Thanks for the pointers! Still, in the interest of understanding how the API works, could you point me to a command-line snippet that would let me send a query (any query in fact) to Coq? It would be really cool to just understand how to even start interacting with the API... I tried the command suggested by Valentin, but I can't get a response to my queries:

  bin/coqtop -ideslave -main-channel stdfds -I ide -I stm -coqlib . <<< '<call val="mkcases">nat</call>'

On 07/01/2015 01:22 PM, Enrico Tassi wrote:
> (...)
> Look at stm.mli/print_ast.  What you get in an XML representation of the
> AST, eventually annotated with extra info for each notation node
> (something like the "format" attribute for example).

Thanks for this pointer. I have no idea what the parameter to print_adt is, however. Is it connected to the PrintAst constructor in ide.ml?

> I don't think there is a CoqIDE message for calling that.
> Adding it would be easy.  An alternative option is to have Coq
> systematically feedback the AST (what PIDE based UI's do IIRC).

Hmm. I was thinking of something that would take the name of a lemma, and print its AST. Is that also what you had in mind, or are you talking about the goal in particular?

Cheers,
Clément.