coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Designing [info] again, Arnaud Spiwack, 07/25/2014
- Re: [Coq-Club] Designing [info] again, Jason Gross, 07/25/2014
- Re: [Coq-Club] Designing [info] again, Adam Chlipala, 07/25/2014
- Re: [Coq-Club] Designing [info] again, Jonathan, 07/25/2014
Archive powered by MHonArc 2.6.18.