The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

Hi,
There is no documentation. Pieces of information have to be extracted from 
/branches/v8.4/toplevel/ide_intf.ml or /trunk/lib/serialize.ml

In an hurry :
- start coqtop with the option -ideslave
- then speak in xml.

you can only send "<call val="foo"></call>" where foo is "interp" a coq 
sentence "about", "quit", "search" a coq regexp, etc
coqtop answers a list <message></message> (always empty in v8.4) and then a 
"<value val="good"(or "fail")></value>"

"<call val="interp" verbose="" raw="">a coq sentence.</call>" is universal 
but you want more structured answers than only string. Therefore, please ask 
coqdev to add the missing primitives you need ...

here is a log of a toy interaction :

eduroam-prg-sg-1-44-231:~ pirbo$ 
/Applications/CoqIdE_8.4pl2.app/Contents/Resources/bin/coqtop -ideslave

<call val="interp">Print nat.</call>
<value val="good"><string>Warning: query commands should not be inserted in 
scripts
Inductive nat : Set :=  O : nat | S : nat -&gt; nat

For S: Argument scope is [nat_scope]
</string></value>
<call val="interp">intuition.</call>
<value val="fail">
Error: Unknown command of the non proof-editing mode.</value>
<call val="about"/>
<value 
val="good"><coq_info><string>8.4pl2</string><string>20120710</string><string>May
 2013</string><string>May 15 2013 18:00:03</string></coq_info></value>
<call val="interp">Definition bar := I.</call>
<value val="good"><string></string></value> 
<call val="rewind" steps="1"/>
<value val="good"><int>0</int></value>
<call val="interp">Goal False.</call>
<value val="good"><string></string></value><goal/>
<value val="fail">Incorrect query.</value>    
<call val="goal"/>
<value val="good"><option 
val="some"><goals><list><goal><string>1</string><list/><string>False</string></goal></list><list/></goals></option></value>
<call val="quit"/>
<value val="good"><unit/></value>eduroam-prg-sg-1-44-231:~ pirbo$

All the best,
Pierre B.


Le 4 juil. 2013 à 17:17, Valentin Robert 
<valentin.robert.42 AT gmail.com>
 a écrit :

> Hello,
>  
> I cannot provide good answers to your questions, but some people recently 
> wrote a vim plugin for using Coq. Their development is available on github. 
> I suggest looking at this file in particular:
>  
> https://github.com/trefis/coquille/blob/pathogen-bundle/autoload/coquille.py
>  
> It might give you some insight.
>  
> Best luck,
> - Valentin
> 
> 
> On Thu, Jul 4, 2013 at 4:10 PM, Abhishek Anand 
> <abhishek.anand.iitg AT gmail.com>
>  wrote:
> Hi,
> I'm trying to develop a Coq plugin for my fav. IDE(https://netbeans.org/) 
> as a hobby project.
> The plugin needs programmatically talk to coqtop. 
> Is there some description of a "protocol" one should follow while
> programmatically talking to coqtop?
> So far, I did some reverse engineering and found out:
> (please correct me if I am wrong)
> 
> 1) Coqtop prints "coq<" on stderr when ready to accept an input. I guess I 
> need to wait until prints "coq < " on stderr before writing to coq's 
> inputstream.
> 2) If coqtop didn't like the previous command, the last line is of the form 
> "error ...". 
>    So, while sending the contents of user's editor window to coqtop, I need 
> to stop as soon
>    as I encounter one of these and prompt the user about the error.
> 
> I need more information so that I can reliably parse coqtop's output, 
> especially proof state and present them to the user in a more intuitive 
> way. I can try to reverse engineering most of these, but would appreciate 
> if some description of a protocol that coqtop follows is available 
> somewhere.
> Some brief description of how CoqIDE works might also be useful.
> 
> Thanks,
> -- Abhishek
> https://github.com/aa755/nbcoq
> 
> 
>