The Coq mailing list

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

With -emacs, you have to interpret Coq's output to determine whether it 
is good or bad, though, which -ideslave seems to do for you.

Also, apart from the newline (which is also not sent in -emacs), the 
synchronization of -ideslave seems a lot saner than -emacs: in the 
latter, it is possible to accidentally send half a phrase, which seems 
impossible in -ideslave. In emacs, the following is possible:


| <prompt>Coq < 1 || 0 < </prompt> Foo [press return]
| [Wait, because Coq expects a terminator]

In -ideslave, this is:
| <call val="interp">Foo</call>
| <value val="fail" loc_s="3" loc_e="4">
| Syntax error: &apos;.&apos; or &apos;...&apos; expected after | 
[tactic:tactic] (in [proof_mode:subgoal_command]).</value>

So you will get an error (with usable feedback) no matter how much you 
mangle the sent commands.


Based on Pierre's examples, I am not sure how you obtain feedback on 
'state' in the -ideslave mode (I see a 'rewind' command that undoes a 
command, but do you have to synchronize this in your own IDE somehow? 
Especially since Coq's rewind can step back farther than instructed).


Carst





On 07/04/2013 11:50 PM, Benjamin Berman wrote:
> 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
> <mailto: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
>     
> <mailto: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
>         
> <mailto: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
>             <http://ide_intf.ml> or /trunk/lib/serialize.ml
>             <http://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
>             
> <mailto: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
>             
> <mailto: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
>              >
>              >
>              >