The Coq mailing list

[Jean-Christophe Filliatre <filliatr AT lri.fr>]

In his message of Thu February 4, 1999, Randy Pollack writes: 

> Sometimes I want to load a .v file, skipping the proofs and treating
> the lemmas as axioms.  Coq supports the compiled .vi file for this
> purpose, but then you must maintain the .vi files up-to-date ....
> 
> Here is a suggestion for a different approach: have a top-level switch
> [...]

Thanks for those suggestions. It would be more flexible to load .vo
files without proof terms with only a switch, I agree.

However, there is no need to "maintain" the .vi files when using
GNU make and a good Makefile automatically produced by do_Makefile
without any effort. There is a target "spec" to make the .vi files,
and the correct dependencies are produced with the target "depend"
(similar to the dependencies for .vo files).

Regarding the loading of .v files (with the command Load) it would
necessitate much more work, and Coq users are rather encouraged to split
their developements in multiple files and to compile them with the Coq
compiler, and not to load them entirely. So your first suggestion about
.vo files would be the most interesting.

Best regards,
-- 
Jean-Christophe FILLIATRE
  
mailto:Jean-Christophe.Filliatre AT lri.fr
  http://www.lri.fr/~filliatr