The Coq mailing list

[Valentin Robert <vrobert AT cs.ucsd.edu>]

I am currently working on understanding the new XML protocol on 8.5, with help from Stuart Pernsteiner.

So far, we have found that:

- the simplest command to invoke it is:

coqtop -ideslave -main-channel stdfds

- a useful command to learn about the new protocol is:

coqtop -ideslave --help-XML-protocol

- the new system sends <message> and <feedback> messages, with some information in this file:

https://github.com/coq/coq/blob/trunk/lib/feedback.ml

- this file contains some information about what the commands actually do and the type of their arguments:

https://github.com/coq/coq/blob/trunk/ide/interface.mli

Best luck,

- Valentin

On Tue, Jun 30, 2015 at 5:26 AM Tej Chajed <tchajed AT mit.edu> wrote:

Can you just disable notation? (Unset Printing Notations, or the View menu in CoqIDE). If you're using Check you might have to re-run the command after disabling.

As far as launching coqtop with ideslave in trunk, this works for me but I don't understand the new async proofs protocol (I picked the control channel port randomly):

coqtop -main-channel stdfds -control-channel 127.0.0.1:60875 -ideslave -async-proofs on

I would also like to hear more generally how to understand the XML protocol.

-Tej

On Tue, Jun 30, 2015 at 4:01 AM Clément Pit--Claudel <clement.pit AT gmail.com> wrote:

Hi all,

Is there a way to print a structured representation of a lemma's statement in Coq? Ideally I'd like to get something like (forall ((A type) (x A) (y A)) (impl (eq x y) (eq y x))) given the lemma [forall A (x y: A), x = y -> y = x].

* Basic extracting to JSON doesn't do, because Props are erased before extraction.
* The PrintAst XML command looks promising, but I'm not sure what its syntax is. [1]
* The code in texmacspp.ml also looks promising, but I have no idea how to call into it.

Thanks!

[1] More generally, I'm not sure how to invoke the IDE slave mode in trunk: the following command works with 8.4pl2, but on trunk it prints "Fatal error: ideslave communication channels not set.":
      coqtop -ideslave <<< '<call val="mkcases">nat</call>'