The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le dimanche 26 septembre 2010 à 12:51 +0200, Michael a écrit :
> Gappa installation now worked with libcoq-ocaml-dev installed.
> 
> Since I got the coq proof obligations from frama-c jessie plugin via C code,
> with the new floating point operations I now have a couple of references coq
> doesn't find.
> 
> The reference "double_value x" wasn't found at first, I could solve this
> problem by manually downloading the floating point library from the coq
> website, compliling *.v and copying it to /usr/lib/coq/user-contrib/. Then I
> could "Require Export Float." (which wasn't possible before).
> However, there's still a couple of references coq doesn't find
> (no_overflow_double, nearest_even, double_of_real_post, 
> truncate_real_to_int).
> How can I find out which modules I have to load, and where to find them?

These Coq files are part of Why. Since you didn't have Float before, my
guess is that the configure file of Why decided to ignore the Coq
libraries. So reconfiguring, recompiling, and reinstalling Why should
improve things.

I just noticed there actually exists a libwhy-coq package. So, assuming
you are already using the package for Why, it should be sufficient. (I'm
not sure though, since I would have expected it to depend on the
libfloat-coq package, which doesn't seem to be the case.)

Best regards,

Guillaume