The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

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.