The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Selon Wojciech Moczydlowski 
<wm174746 AT zodiac.mimuw.edu.pl>:

Hello,

  You're right. Cut and paste from a coqtop shell to a .v file is not a good
method for developping and saving proofs.


  The coqide tool allows you to edit your proof interactively in a .v file
(all you need to do is saving your buffer from time to time ...).
 coqide contains tools for safely undoing steps, searching already proven
theorems, etc.
 coqide is available from the Coq distribution, and is described in the
Reference Manual.



  There are also Pcoq (developped by the Lemme project) and the coq mode for
Proof General, if you  want to work with (X)emacs and its keys.



Hope this helps,

Pierre








(*) available with the coq distribution.

>   Hello,
>
> I have a question regarding saving proofs in Coq, namely, how to do it.
> That is, I would like to be able to do the following (in coqtop).
> 1. State some lemma.
> 2. Prove it (using coqtop).
> 3. Somehow save the proof (and lemma) so that next time I can proceed with
> the development with the lemma proved.
>
> What I've been doing so far was stating the lemmas in the .v file, and
> simply pasting proofs to this file; this methodology, though, stopped
> being sufficient once proofs got large. The Write State command, which
> from the description could be what I'm looking for, doesn't seem to be
> working.
>
> Thanks,
>
> Wojtek
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>


-- 
Pierre Casteran
(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.