The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

On 06/30/2015 05:24 AM, Tej Chajed 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.

That not enough for my purposes; ideally, I don't want to be doing any 
parsing myself; the best I can get with Unset Printing Notations is the 
following, which is still non-trivial to parse:
   forall (A : Type) (x y : A), eq x y -> eq y x
      : Prop

> 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 
> <http://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
>  
> <mailto: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 <http://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>'
>