The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

For my purposes, a top-level command would be just as good.  Likewise for [debug], BTW.

On 08/05/2014 05:12 AM, Arnaud Spiwack wrote:

Another question: is it useful that [info] be a tactic? Or can it be a toplevel command?

If it is useful as a tactic, what should something like [info (t;info u)] print?

On 25 July 2014 16:28, Jonathan <jonikelee AT gmail.com> wrote:

On 07/25/2014 06:32 AM, Arnaud Spiwack wrote:

Dear all,

I'm currently working on polishing my part for the upcoming version of Coq.
One common request I got was to bring back the [info] tactical. And, as it
happens, I'm now in a situation where I can make it happen.

But what I cannot do, is take the code for the old [info] and port it to
the current development version, I really have do write the feature from
scratch. And if I get to do [info] anew, I really want to get it right (and
possibly divide it in several features).

So, dear [info] user, I'm asking you:

    - What do you use [info] for?
    - Do you use the [info (info t)] feature?
    - If you had one or two feature request for [info] to make it even

    slightly better, what would they be?

    - Is there something which is kind of like [info] but not quite and that

    you really wished you had in your toolbox?


/Arnaud Spiwack

I have some experience with PVS (a long time ago), which has a feature allowing one to see what any non-atomic tactic was doing by causing that tactic to print out the successful part of its internal script - as an actual script.  That was very helpful for learning the tactic language (which I no longer recall).  I vaguely recall that it was also possible to capture the spilled low-level tactic script as a replacement for the high-level tactic - allowing one to shortcut the automation when replaying in favor of the direct script (and get a performance boost as a result due to eliminating all of the failed search paths).  Or, maybe that's a false memory of how I wanted it to work.

But, I also think that there needs to be a better way to debug a complicated tactic than the current Ltac debugger - and having a way to trace all of the workings of the tactic (even the failures and backtracks) would help there.  And, for really big proof searches, there should be a way to filter that trace.