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: Jason Gross <jasongross9 AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Designing [info] again
  • Date: Fri, 25 Jul 2014 11:50:36 +0100

I started using Coq only shortly before [info] disappeared, but there are many cases where I wish I had something that gave me an Ltac stack trace (on either success or error), so that I could see which tactics were called with which arguments in what order, possibly (optionally?) including when things failed and backtracking happened.  It might be nice to also have a variant of [idtac] that only printed it message when being run under [info], so that I could add debug information that will otherwise be ignored.

-Jason


On Fri, Jul 25, 2014 at 11:32 AM, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> 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




Archive powered by MHonArc 2.6.18.

Top of Page