[Why3-club] problem with why3config

Alan Schmitt alan.schmitt at polytechnique.org
Fri Feb 17 07:40:18 CET 2012


On 16 Feb 2012, at 3:40, Andrei Paskevich wrote:

> Hello,
>
> Having seen your questions on caml-list, I have to assume that
> you have compiled why3 on a mac os x system in native code.
> Is this correct?

Yes, this is what I'm trying to do.

> If you get the warning "-read_only_relocs cannot be used with x86_64"
> during compilation (although you do not mention this in your email
> to why3-club, it was mentioned in your posting to caml-list), then
> I'd suggest to reopen http://caml.inria.fr/mantis/view.php?id=4863
> since that bug does not seem to be fixed in your ocaml setup.

That was part of my question on the list, and it's something I really 
don't understand. I get the warning, yet many of my tests of native 
dynlink work. Except for why3.

> In the meantime, you should be able to compile why3 in bytecode
> (by giving the option --disable-native-code to ./configure).

Thank you for the suggestion. I'll keep investigating.

Alan



More information about the Why3-club mailing list