The Coq mailing list

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

On 06/30/2015 04:26 PM, Jason Gross wrote:
> You might or might not find Gregory's template-coq plugin 
> <https://github.com/gmalecha/template-coq> useful, which lets you dump the 
> kernel representation of terms into a Gallina datatype.

Thanks; ideally, though, I'd like to not have to depend on extra plugins, 
given that all the code required for printing seems to already exist in 
texmacspp.ml.

Clément.

> On Tue, Jun 30, 2015 at 7:07 PM, Valentin Robert 
> <vrobert AT cs.ucsd.edu
>  
> <mailto:vrobert AT cs.ucsd.edu>>
>  wrote:
> 
>     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
>  
> <mailto: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 
> <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>'
> 
>