Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Designing [info] again

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Designing [info] again


Chronological Thread 
  • From: Jonathan <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Designing [info] again
  • Date: Fri, 25 Jul 2014 10:28:06 -0400

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





Archive powered by MHonArc 2.6.18.

Top of Page