The Coq mailing list

[Carst Tankink <carst AT cs.ru.nl>]

Quick question: is -ideslave the way to programatically communicate with 
Coq, going forward?
If so, will there be documentation for this mode at some point in time?


Carst

On 07/04/2013 06:35 PM, Pierre Boutillier wrote:
> 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