[Why3-club] problem with why3config

Andrei Paskevich andrei at tertium.org
Fri Feb 17 10:21:37 CET 2012


Hi,

just to check, could you add the option "-linkall" to the makefile
variable OFLAGS (line 72 in Makefile.in) and see if the problem
persists?

Thanks,
Andrei

On Fri, Feb 17, 2012 at 07:40, Alan Schmitt
<alan.schmitt at polytechnique.org> wrote:
> 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