coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin
Chronological Thread
- From: Benjamin Berman <bnjmnbrmn AT gmail.com>
- To: t x <txrev319 AT gmail.com>
- Cc: Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>, Valentin Robert <valentin.robert.42 AT gmail.com>, Abhishek Anand <abhishek.anand.iitg AT gmail.com>, "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin
- Date: Thu, 4 Jul 2013 16:50:36 -0500
Try "coqtop -emacs". You might also consider redirecting stderr to stdout (redirectErrorStream in the java.lang.ProcessBuilder)
--Ben
On Thu, Jul 4, 2013 at 4:40 PM, t x <txrev319 AT gmail.com> wrote:
Along this line: what is the easiest way to parase output from coqtop -ideslave? I know that I can set notation off -- however, is it possible to get back an lisp sexp or an xml abstract syntax tree?
(I don't care about human readability; I can convert it from machine readable to human readable in my client code.)On Thu, Jul 4, 2013 at 2:37 PM, t x <txrev319 AT gmail.com> wrote:
https://github.com/vim-scripts/CoqIDE/blob/master/plugin/coq_IDE.vim#L111-L119 is the most concise description of the "coqtop -ideslave" interface I know of.
One tip: coq does not seem to send back "\n", so when reading back from Coq, care needs to be taken care of to avoid hanging with Java IO routines. (I spent days troubleshooting this.)On Thu, Jul 4, 2013 at 9:35 AM, Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr> 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 -> 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
>
>
>
- [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, Abhishek Anand, 07/04/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, Beta Ziliani, 07/04/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, Valentin Robert, 07/04/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, Pierre Boutillier, 07/04/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, t x, 07/04/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, t x, 07/04/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, Benjamin Berman, 07/04/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, Carst Tankink, 07/05/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, Pierre Boutillier, 07/05/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, Pierre Courtieu, 07/08/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, Abhishek Anand, 07/23/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, Abhishek Anand, 07/23/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, Thomas Refis, 07/23/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, Abhishek Anand, 07/23/2013
- Re: [Coq-Club] help w/ coqtop programmatic interaction for Netbeans plugin, Pierre Boutillier, 07/24/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, Carst Tankink, 07/05/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, Benjamin Berman, 07/04/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, t x, 07/04/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, t x, 07/04/2013
- Re: [Coq-Club] Fwd: help w/ coqtop programmatic interaction for Netbeans plugin, Pierre Boutillier, 07/04/2013
Archive powered by MHonArc 2.6.18.