The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Show Script doesn't work in 8.4. That's the reason why Qed doesn't output the script anymore. So it won't make a good replacement.

That said, we are sorry to disrupt the workflow of some of our users. But I cannot say either that the toplevel is one of our main target interface, it gets neglected often (it's almost miraculous that it is still usable as a full fledged tool). Most of the toplevel users use it for debugging Coq, most of these wouldn't quite mind not using at all if it came to disapear altogether. We are still working on some way to have a Show Script feature in the forthcoming versions of Coq. It's unlikely to make it into 8.4 though.



Arnaud

On 12 January 2012 16:02, Jonas Oberhauser <s9joober AT googlemail.com> wrote:

You could use the 'Show Script' command before saving the proof, but
I'm not sure if that's the bestest idea ever (considering you might
complete an invalid proof, and I'm unsure of any command that checks
the validity of the Proof other than Qed/Save/Defined).
Here's a link to the Show command:
http://coq.inria.fr/doc/Reference-Manual010.html#@command197

Apart from that, CoqIDE is interactive as well. I haven't ever used
ProofGeneral, but I assume it is too. Exploration of the proof in
step-by-step fashion, as you describe it, should be possible there
just as well.

Kind regards,
Jonas

2012/1/11  <alexander AT math.ohio-state.edu>:

> Hello,
>
> In Coq 8.3, when using the interactive mode, when one completes a proof and
> types Qed. or Defined., the program outputs the steps used in the proof.  This
> was a very nice feature because it allowed us to explore our way toward a proof
> step-by-step without having to constantly manually take notes on what commands
> we had issued.  In 8.4, doing proofs in interactive mode is almost useless,
> unless one tediously copies every command into a separate word processor as one
> goes.  Is there a way to turn the feature back on so that Qed/Defined lists the
> steps we used in our proof?  Or is there some command, once a lemma is defined,
> which will output the steps which were used?  (e.g., it would be nice if
> "Check" or "Print" would do so, but neither do)
>
> Thanks for keeping Coq such an actively developed software package :)
>
> -Sam Alexander