The Coq mailing list

[Frederic Blanqui <frederic.blanqui AT inria.fr>]

Hello.

I think that, to use an external contrib, it is better to compile it 
with the -R option to give it a symbolic name and avoid name clashes:

coq_makefile -R . Floats `find . -name *.v` > Makefile
make

But make sure that there is no "Add LoadPath" in the contrib. Remove 
them otherwise.

Then, for using this contrib in ProofGeneral or CoqIDE, add the 
following line in your ~/.coqrc file:

Add Rec LoadPath "<directory>" as Floats.

Then, in your development, you can use modules from Floats as follows:

Require Import <module>.
or
Require Import Floats.<module>.

And, to compile your file, do:

coqc -R <directory> Floats my_file.v

Or, if you also have many files:

coq_makefile -R <directory> Floats `find . -name \*.v` > Makefile
make

And you can even give a symbolic name to your own files so that other 
people can easily reuse your own development:

coq_makefile -R <directory> Floats -R . MyContrib `find . -name \*.v` > 
Makefile

Hope it will help.

Frederic.

Le 29/10/2010 06:22, Michael a écrit :
> Hello,
>
> I downloaded Floats8.2.tgz from https://lipforge.ens-lyon.fr/projects/pff/ and
> tried to compile and install ist.
> I first try to use the Makefile included in the archive, with "make depend&&
> make all&&  sudo make install", however it did not find some dependencies.
> I then tried to create the Makefile on my own, with "coq_makefile *.v>
> Makefile". However, it already gives a warning:
> "Warning: install target will copy files at the first level of the coq
> contributions installation directory; option -R is recommended"
> I think it is because of the subdirectories in the Float8.2 package. If I
> ignore the warning, make simply puts all *.vo files in the
> /usr/lib/coq/user-contrib/Float/, but withouth any subdirectories. The result
> is, that a lot of libraries can't be found by other proof skripts later (even
> moving them to the right subdirectories manually later on does not help).
>
> Can somebody help me, how to get the installation correctly done? Maybe it's
> just because of the option "-R" recommended in the warning, but I don't know
> how to apply it on all subdirectories.
>
>
> Sincerely,