coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
- To: coq-club AT inria.fr
- Cc: alexander AT math.ohio-state.edu
- Subject: Re: [Coq-Club] Outputting proof in interactive mode in Coq 8.4
- Date: Fri, 13 Jan 2012 11:25:48 +0100
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
- [Coq-Club] Outputting proof in interactive mode in Coq 8.4, alexander
- Re: [Coq-Club] Outputting proof in interactive mode in Coq 8.4,
Adam Chlipala
- Re: [Coq-Club] Outputting proof in interactive mode in Coq 8.4, Jean Goubault-Larrecq
- Re: [Coq-Club] Outputting proof in interactive mode in Coq 8.4,
Jonas Oberhauser
- Re: [Coq-Club] Outputting proof in interactive mode in Coq 8.4, Arnaud Spiwack
- Re: [Coq-Club] Outputting proof in interactive mode in Coq 8.4,
Adam Chlipala
Archive powered by MhonArc 2.6.16.