coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Enrico Tassi <enrico.tassi AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Printing a structured representation of a Prop?
- Date: Thu, 2 Jul 2015 09:40:22 +0200
On Wed, Jul 01, 2015 at 09:29:31PM -0700, Clément Pit--Claudel wrote:
> Thanks for this pointer. I have no idea what the parameter to
> print_adt is, however. Is it connected to the PrintAst constructor in
> ide.ml?
I guess the best documentation is the underlying API in stm/stm.mli.
When CoqIDE sends a sentence to Coq is performs an "add" call.
The result is a unique id (called Stateid.t). print_ast takes this
id and prints the AST of the sentence corresponding to that id.
The best way to see how the protocol works is to start CoqIDE with
-debug and look at the debugging output in the terminal. There is much
more than the protocol, but there is no better way. The messages are
also documented in ide/interface.mli IIRC.
I told you you should have come to the CoqCS ;-P
--
Enrico Tassi
- Re: [Coq-Club] Printing a structured representation of a Prop?, (continued)
- Re: [Coq-Club] Printing a structured representation of a Prop?, Clément Pit--Claudel, 07/01/2015
- Re: [Coq-Club] Printing a structured representation of a Prop?, Clément Pit--Claudel, 07/01/2015
- Re: [Coq-Club] Printing a structured representation of a Prop?, Emilio Jesús Gallego Arias, 07/01/2015
- Re: [Coq-Club] Printing a structured representation of a Prop?, Pierre Courtieu, 07/01/2015
- Re: [Coq-Club] Printing a structured representation of a Prop?, Emilio Jesús Gallego Arias, 07/01/2015
- Re: [Coq-Club] Printing a structured representation of a Prop?, Clément Pit--Claudel, 07/02/2015
- Re: [Coq-Club] Printing a structured representation of a Prop?, Emilio Jesús Gallego Arias, 07/01/2015
- Re: [Coq-Club] Printing a structured representation of a Prop?, Pierre Courtieu, 07/01/2015
- Re: [Coq-Club] Printing a structured representation of a Prop?, Enrico Tassi, 07/01/2015
- Re: [Coq-Club] Printing a structured representation of a Prop?, Clément Pit--Claudel, 07/02/2015
- Re: [Coq-Club] Printing a structured representation of a Prop?, Valentin Robert, 07/02/2015
- Re: [Coq-Club] Printing a structured representation of a Prop?, Clément Pit--Claudel, 07/02/2015
- Re: [Coq-Club] Printing a structured representation of a Prop?, Enrico Tassi, 07/02/2015
- Re: [Coq-Club] Printing a structured representation of a Prop?, Valentin Robert, 07/02/2015
- Re: [Coq-Club] Printing a structured representation of a Prop?, Clément Pit--Claudel, 07/02/2015
- Re: [Coq-Club] Printing a structured representation of a Prop?, Clément Pit--Claudel, 07/02/2015
Archive powered by MHonArc 2.6.18.