The Coq mailing list

[pcourtie AT univ-orleans.fr]

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

>   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. 

You can deal with large proofs in the same as in programming languages: 
use several files and compile them separately (Require is fast).
You can build a makefile and use the coqdep command to build dependencies. 
The inconvenient of this is that once you have Qed'ed a proof, you need 
to compile the file to use the lemma in another file. If you keep files 
small the annoyance is acceptable.

Cheers,
Pierre

> 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
> 
>