The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

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.


-- Jonathan