The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

Hi,

> when I try to compile coq codes using first
> 
> coq_makefile *.v > Make
> 
> then it prompts me directly with the following warning:
> 
> Warning: install target will copy files at the first level of the coq
> contributions installation directory; option -R is recommended
> 
> Is this expected change with the newest version of Coq, or was the
> installation something wrong?
> It seems though everything is working well.

This is just a warning. And apparently a not clear enough one. Maybe
also a bit intrusive: it only concerns what will happen if the user
issues a "make install" (the alternative could have been to generate
an "install" target only on demand).

The purpose of "make install" is to copy the current development in
the $COQLIB/user-contrib directory where COQLIB is the installation
directory of coq ($COQLIB/user-contrib is one of the root directory
where Coq is looking by default for compiled files).

In presence of a -R option, say as in "-R . MyLibrary", "make install"
copies the files in $COQLIB/user-contrib/MyLibrary instead of
$COQLIB/user-contrib/, what shifts the risk of accidental file-names
collision to a more visible risk of library-names collision.

In any cases the warning can be ignored. Or it can also be prevented
by adding a -R option as in

coq_makefile -R . MyDevelopment *.v > Makefile

Hope it helps,

Hugo Herbelin