Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] No more info tactical?!

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] No more info tactical?!


chronological Thread 
  • From: Pierre Courtieu <Pierre.Courtieu AT cnam.fr>
  • To: Adam Chlipala <adamc AT csail.mit.edu>
  • Cc: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>, coq-club AT inria.fr
  • Subject: Re: [Coq-Club] No more info tactical?!
  • Date: Fri, 6 Jan 2012 15:09:23 +0100

For this use there is a debug mechanism for Ltac. It has been there
for a while but is now shortly documented
(http://coq.inria.fr/coq/refman/Reference-Manual012.html#@default763).

Set Ltac Debug.

It is not allowed in coqide. In ProofGeneral it is possible to use it:
when scriting a tactic, just switch to the *coq* buffer and hit
commands there.

Best regards,
P.

2012/1/6 Adam Chlipala 
<adamc AT csail.mit.edu>:
> Arnaud Spiwack wrote:
>>
>>
>>    As a devoted Adamizer of proof scripts (with a summer's worth of
>>    Ltackery to prove it), I can't imagine life without info ...
>>
>>
>> I'd be interested in knowing how you use it.
>
>
> The usual scenario is that some complex Ltac program isn't behaving as
> expected, so you run that tactic with [info], which outputs the sequence of
> steps taken "at one level lower in the abstraction stack."  Then you run
> each of these tactics, until one behaves unexpectedly.  Now run that tactic
> with [info] and repeat.  This can really be a lifesaver in Ltac debugging.
>  I don't know if some new 8.4 facility compensates.  (I try to stick to the
> Debian testing packages only, so I've only yet experienced behaviors up to
> 8.3.)




Archive powered by MhonArc 2.6.16.

Top of Page