The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi Emilio, Could you please be more precise?

The coq team just spent some time in the last two years making an xml protocol in order to de-correlate coq from its ide. The idea being that

1) ide can run in a different thread, ide can even talk with different forks (workers) of the same coq.

2) the codes are well separated and a bug in coq leaves the interface alive

3) protocols are essentially APIs that one cannot easily shunt, so it forces good practice.

So any argument in favor of going back to a linked interface should be looked at very carefully. I think a lot of things can be done via a well designed protocol.

P.

 

2015-07-01 11:25 GMT+02:00 Emilio Jesús Gallego Arias <gallego AT cri.ensmp.fr>:

Hi Clément,

Clément Pit--Claudel <clement.pit AT gmail.com> writes:

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

That's very interesting, please let us know if you make any progress.

In our case, we resorted to linking directly to Coq (I happen to be in
Ocaml-land).

I just can't see how to do some of the more advances interaction/display
features we have in mind just using the protocol.

Best,
E.