The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

I've made a lot of progress on this over the last 3 weekends and now I have a plugin that I use for all my Coq development. However, I just encountered an inconsistency between the behaviour of coqc and coqtop --ideslave . Here is the minimal example which demonstrates it:

-----------

Require String. Open Scope string_scope.

Ltac move_to_top x :=

  match reverse goal with

  | H : _ |- _ => try move x after H

  end.

Tactic Notation "assert_eq" ident(x) constr(v) :=

  let H := fresh in

  assert (x = v) as H by reflexivity;

  clear H.

Tactic Notation "Case_aux" ident(x) constr(name) :=

  first [

    set (x := name); move_to_top x

  | assert_eq x name; move_to_top x

  | fail 1 "because we are working on a different case" ].

Tactic Notation "Case" constr(name) := Case_aux Case name.

Tactic Notation "sp_iff"  ident(c) :=

  split;

  [ Case_aux c "->"

  | Case_aux c "<-"

  ].

Theorem buggy: ((1=1)->(2=2)) <-> ((1=1)->(2=2)).

Proof.

 sp_iff Case. 

   + Case "->";  auto.

   + Case "<-"; auto.

Qed.

------------

Everything upto the definition of sp_iff was taken from http://www.cis.upenn.edu/~bcpierce/sf/SfLib.html

This file compiles w/o any error when using coqc.

But when my plugin sends the contents of the file to (coqtop --ideslave) gradually, the theorem buggy fails. Specifically, + Case "->";  auto. does not seem to run auto. removing + works.

Replacing ; by . works. 

This is an annoyance, because I am working on a coq codebase in which this pattern occurs multiple times. CoqIDE and proofgeneral do not seem to have this problem. I guess it has something to do with ---ideslave mode that I am using

On Mon, Jul 8, 2013 at 3:39 AM, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

Hello,

Being the main maintainer of coq proofgeneral I would recommend -ideslave instead of -emacs. It is highly probable that ProofGenral will go to -ideslave at some point. The protocol is much better and cleaner. Some remarks however:

1) -ideslave protocol is still in beta version (please correct me if I am wrong).

2) the ParalITP branch on Enrico Tassi's github may be the ultimate protocol. Roughly speaking coq becomes an asynchronous transaction machine with the same kind of protocol than -ideslave (but asynchronous). Consider it in alpha state for now. This is part of the same effort as the on edescribed by Makarius.

My advice would be: use -ideslave for now but be warn that it is not stable.

P.

2013/7/4 Benjamin Berman <bnjmnbrmn AT gmail.com>

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 -&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
>
>
>