The Coq mailing list

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

Hi,
I have been using this plugin for more than a month and think it might be useful for people working on large coq developments spanning multiple files. Installation instructions and a demo video can be found at
https://github.com/aa755/nbcoq/blob/master/README.md

Also, I have the following questions about coqtop related to this plugin:

1) In the --ideslave mode, how to I tell coqtop to abort the current computation and ignore the last command?(eg when I send repeat(simpl)).

2)In the development version of coq and hott branch, executing queries return an XML output containing a forest of nodes(there is no single root node).
For future versions of coq, should I not assume that the XML output would have a single root node?

-- Abhishek
http://www.cs.cornell.edu/~aa755/

2 days ago I answered :
Le 19 juil. 2013 à 01:07, t x <txrev319 AT gmail.com> a écrit :

> Hi,
>
>  I'm wondering if there's a solution to this (besides "use proof general" :-) )
>
>  I'm using Coq inside of Vim, which is running coq via "coqtop.opt -ideslave"
>
>  In trying to debug one of my tactics, I want to execute:
>
>  "Set Printing Implicit."
>
>  Unfortunately, I get back the response 
>
>  "Use CoqIDE display menu instead."
>
>  Thus, I'm wondering:
>  1) Does the CoqIDE display menu send a different message to "coqtop.opt -ideslave"?

it sends <call id="-2" val="interp" raw="">Set Printing Implicit.</call>
>
>  2) And if so, how can I mimic this message?

you should add the 'raw=""' in your call :-)
>
>
> Thanks!

Cheers,
Pierre B.

Le 23 juil. 2013 à 23:13, Abhishek Anand <abhishek.anand.iitg AT gmail.com> a écrit :

> Thanks for that example.
>
> When I send "Set Printing Universes."  or other set command , (coqtop -ideslave) replies back :
> <?xml version="1.0"?>
> <value val="fail" loc_s="0" loc_e="23">
> Error: Use CoqIDE display menu instead</value>
> How do I get around this?
>
> Thanks
>

2 days ago I answered :

Le 19 juil. 2013 à 01:07, t x <txrev319 AT gmail.com> a écrit :

Hi,

 I'm wondering if there's a solution to this (besides "use proof general" :-) )

 I'm using Coq inside of Vim, which is running coq via "coqtop.opt -ideslave"

 In trying to debug one of my tactics, I want to execute:

 "Set Printing Implicit."

 Unfortunately, I get back the response 

 "Use CoqIDE display menu instead."

 Thus, I'm wondering:
 1) Does the CoqIDE display menu send a different message to "coqtop.opt -ideslave"?

it sends <call id="-2" val="interp" raw="">Set Printing Implicit.</call>

 2) And if so, how can I mimic this message?

you should add the 'raw=""' in your call :-)

Thanks!

Cheers,
Pierre B.

Le 23 juil. 2013 à 23:13, Abhishek Anand <abhishek.anand.iitg AT gmail.com> a écrit :

Thanks for that example.

When I send "Set Printing Universes."  or other set command , (coqtop -ideslave) replies back :

<?xml version="1.0"?>

<value val="fail" loc_s="0" loc_e="23">

Error: Use CoqIDE display menu instead</value>

How do I get around this?

Thanks

On Tue, Jul 23, 2013 at 2:17 AM, Thomas Refis <thomas.refis AT gmail.com> wrote:

2013/7/23 Abhishek Anand <abhishek.anand.iitg AT gmail.com>:

> I think I know that I'm doing something wrong. when I process the line +
> Case "->";  auto.  ,
> I need to send it to CoqTop in 2 steps. First send "+ " and then "Case "->";
> auto."

Precisely.
Note that you get the same behavior when you send something after a
dot (i.e. it is ignored), see http://paste.awesom.eu/IFp .