The Coq mailing list

[Jianzhou Zhao <jianzhou AT seas.upenn.edu>]

Does Float8.2-1.2.tgz also have this problem? I could install
Float8.2-1.2 in Coq 8.3-rc1 after replacing 'Require Export Zbinary'
by 'Require Export Zdigits' in Others/IEEE.v.

BTW: Does this library have a document? I cannot find anyone in the
release. The Float.v has a comment saying the code formalizes IEEE
754. Does this standard include all single-precision,
double-precision, 128-bit precision floats, and 80-bit floats in x86?

On Thu, Oct 28, 2010 at 6:22 PM, Michael
<michaelschausten AT googlemail.com>
 wrote:
> 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,
>



-- 
Jianzhou