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: 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 there
for a while but is now shortly documented

(http://coq.inria.fr/coq/refman/Reference-Manual012.html#@default763).

Set Ltac Debug.


Is this different from [Debug On]?





Archive powered by MhonArc 2.6.16.

Top of Page