The Coq mailing list

["Randy Pollack" <rap AT dcs.ed.ac.uk>]

Jean-Christophe Filliatre replied to Randy Pollack:

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

My point was not about efficiency.  Users might want to write a
specification file with definitions and lemmas before filling in the
proofs.  Then they would want to check the specification file to see
that the definitions and lemmas typecheck.  In real life, we will
often have some lemmas proved and others not yet proved, and still
want to check the whole development.  Perhaps you reply "just write
the unproved lemmas as Axiom", but I was just asking for a mechanical
switch to do that very thing.

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

OK, there's a mechanical way to keep the .vi files up-to-date, but I
wrote "..." in my suggestion to indicate that something inevitably
goes wrong if it is possible.  E.g. I guess that some .v files fail
when compiled (or reloaded) as .vi files, so the automatically
produced Makefile may crash, and one would have to manually tweak it
....  You surely do not argue that it wouldn't be better to eliminate
a duplicate form of data (.vi files) if their purpose can be achieved
with a command-settable switch.

Randy