The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT cnam.fr>]

Le Fri, 20 Apr 2007 13:51:37 +0800,
dz dz 
<sophiee_shao AT hotmail.com>
 a ¨¦crit :

> I have tried to compile many (.v) files, but all the files can't be 
> transformed to (.vo) format.I manipulated step by step as follows:
> open XX file-> select "compile"-> select "compile buffer". Then
> coqide indicated that : compilation output: 'coqc' ¿Ú ¿Ú
> ¿Ú ......(with many squares) .I don't know what the problem is.

You should compile files by hand on the command line to see the error
messages. Probably you have to change all your Load commands by "Require
Export".

coqc filename.v

you should have the "bin" directory of coq installation in your path.
 
> I always use "Load" instead of the "Require" command , is there any 
> difference between these two command? 

Yes, Load actually reads and interpret the whole file, which is very
slow. Require (Export) loads the compiled file, which is much faster.
Moreover when using compiled files you can have several definitions
with the same name in different files without problem (use
"filename.name" to distinguish).

You definitely should compile your files. The best way is to do it on
command line with a makefile. You can use the coq_makefile tool which
is included with coq. It seems you are under windows so you should
probably install gnumake (http://www.steve.org.uk/Software/make/),
unless you are under cygwin. I never use coqc under windows. If you are
under linux, coq_makefile is what you need.

Best regards,



> Best Regards,
> Ying