coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonathan <jonikelee AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] idtac and other msgs in PG
- Date: Mon, 15 Dec 2014 11:04:49 -0500
On 12/15/2014 10:13 AM, Pierre Courtieu wrote:
Hi Jonathan,
Indeed pg is a bit out of sync with coq trunk currently.
I am trying to save some time to fix it. I aim at maintaining the same kind
of features as for coq 8.4. Understand: I don't have enough time to
implement something using asynchronous protocol for now. Maybe later if
other emerging interfaces do not grow mature enough.
Best regards,
Pierre
Thanks, Pierre! Not having the asynchronous protocol is not a problem for me (it doesn't work well with my scripts in CoqIDE due to my use of extraction after most function definitions).
-- Jonathan
Le Sat Dec 13 2014 at 5:27:27 PM, Jonathan
<jonikelee AT gmail.com>
a écrit :
For a while now I've been flipping back and forth between using PG and
CoqIDE, mostly because for some reason PG no longer shows idtac messages
(and other non-failure messages, such as from the Time command) in most
cases. It only shows them when the message-producing tactic also solves
the goal.
I'm wondering if anyone else has this issue with idtac in PG, or if I
somehow have it misconfigured.
I'm using a recent trunk version of Coq and the most recent development
version of PG (which is more than a year old).
-- Jonathan
- [Coq-Club] idtac and other msgs in PG, Jonathan, 12/13/2014
- Re: [Coq-Club] idtac and other msgs in PG, Pierre Courtieu, 12/15/2014
- Re: [Coq-Club] idtac and other msgs in PG, Jonathan, 12/15/2014
- Re: [Coq-Club] idtac and other msgs in PG, Enrico Tassi, 12/16/2014
- Re: [Coq-Club] idtac and other msgs in PG, Jonathan, 12/15/2014
- Re: [Coq-Club] idtac and other msgs in PG, Kazuhiko Sakaguchi, 12/15/2014
- Re: [Coq-Club] idtac and other msgs in PG, Pierre Courtieu, 12/15/2014
- Re: [Coq-Club] idtac and other msgs in PG, Pierre Courtieu, 12/16/2014
- Re: [Coq-Club] idtac and other msgs in PG, Jonathan, 12/16/2014
- Re: [Coq-Club] idtac and other msgs in PG, Jonathan, 12/16/2014
- Re: [Coq-Club] idtac and other msgs in PG, Jonathan, 12/16/2014
- Re: [Coq-Club] idtac and other msgs in PG, Pierre Courtieu, 12/16/2014
- Re: [Coq-Club] idtac and other msgs in PG, Jonathan, 12/15/2014
- Re: [Coq-Club] idtac and other msgs in PG, Pierre Courtieu, 12/15/2014
- Re: [Coq-Club] idtac and other msgs in PG, Pierre Courtieu, 12/15/2014
Archive powered by MHonArc 2.6.18.