coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.)
- [Coq-Club] No more info tactical?!, Luke Maurer
- Re: [Coq-Club] No more info tactical?!,
Arnaud Spiwack
- Re: [Coq-Club] No more info tactical?!,
Adam Chlipala
- Re: [Coq-Club] No more info tactical?!, Pierre Courtieu
- Re: [Coq-Club] No more info tactical?!,
Adam Chlipala
- Re: [Coq-Club] No more info tactical?!,
Pierre Courtieu
- Re: [Coq-Club] No more info tactical?!,
Adam Chlipala
- Re: [Coq-Club] No more info tactical?!, Luke Maurer
- Re: [Coq-Club] No more info tactical?!, Paul Broome
- Re: [Coq-Club] No more info tactical?!, Arnaud Spiwack
- Re: [Coq-Club] No more info tactical?!,
Adam Chlipala
- Re: [Coq-Club] No more info tactical?!,
Pierre Courtieu
- Re: [Coq-Club] No more info tactical?!,
Adam Chlipala
- Re: [Coq-Club] No more info tactical?!, Pierre Courtieu
- Re: [Coq-Club] No more info tactical?!, Luke Maurer
- Re: [Coq-Club] No more info tactical?!, Jonas B. Jensen
- Re: [Coq-Club] No more info tactical?!,
Adam Chlipala
- Re: [Coq-Club] No more info tactical?!,
Arnaud Spiwack
Archive powered by MhonArc 2.6.16.