coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Luke Maurer <maurerl AT cs.uoregon.edu>
- To: <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] No more info tactical?!
- Date: Fri, 06 Jan 2012 14:38:17 -0700
Yup, intuition is precisely the case for me where the debugger fails, particularly because I like to write proof scripts inside a "repeat progress intuition" loop. If I find it hard to nail down which automated step is, for instance, unfolding something prematurely or otherwise wreaking havoc, I want to see precisely what the sequence of events is, but using the debugger that means sifting through dozens or even hundreds of steps while intuition does its thing.
CTTOI, it might be a lot easier if there were some sort of breakpoint mechanism. Even just a "break" tactical that I'd have to insert by hand could come in quite handy.
---
- Luke
On Fri, 06 Jan 2012 11:41:27 -0500, Adam Chlipala wrote:
OK, I've found that mechanism to be almost impossible to use for most
debugging tasks. [info] has been much more useful. The problem with
the tactic debugger is that it has an odd notion of the granularity of
steps, with no way to skip steps beside counting them, rather than
saying something like "run until we are done evaluating tactic [foo]".
(Or maybe I'm just not familiar with its capabilities.) This is
especially bad when debugging a tactic that calls [intuition], which
generates many steps that the debugger chooses to show when stepping!
Pierre Courtieu wrote:
It is the same command.
P.
2012/1/6 Adam Chlipala
<adamc AT csail.mit.edu>:
Pierre Courtieu wrote:
For this use there is a debug mechanism for Ltac. It has been thereIs this different from [Debug On]?
for a while but is now shortly documented
(http://coq.inria.fr/coq/refman/Reference-Manual012.html#@default763).
Set Ltac Debug.
- [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.