The Coq mailing list

[Tej Chajed <tchajed AT mit.edu>]

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