[Why3-club] problem with why3config

Andrei Paskevich andrei at tertium.org
Thu Feb 16 03:40:22 CET 2012


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?

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.

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

Best regards,
Andrei

On Wed, 15 Feb 2012 at 15:18:39 (+0100), Alan Schmitt wrote:
> Hello,
> 
> I just compiled and installed the git version of why3, and I have an
> error running why3config:
> 
> == Found /usr/local/lib/why3/plugins/genequlin.cmxs ==
> The plugin /usr/local/lib/why3/plugins/genequlin.cmxs dynlink failed :
> Dynlink error : error loading shared library:
> dlopen(/usr/local/lib/why3/plugins/genequlin.cmxs, 134): Symbol not
> found: _camlRandom
>   Referenced from: /usr/local/lib/why3/plugins/genequlin.cmxs
>   Expected in: flat namespace
>  in /usr/local/lib/why3/plugins/genequlin.cmxs
> == Found /usr/local/lib/why3/plugins/tptp.cmxs ==
> The plugin /usr/local/lib/why3/plugins/tptp.cmxs dynlink failed :
> Dynlink error : error loading shared library:
> dlopen(/usr/local/lib/why3/plugins/tptp.cmxs, 134): Symbol not
> found: _camlParsing
>   Referenced from: /usr/local/lib/why3/plugins/tptp.cmxs
>   Expected in: flat namespace
>  in /usr/local/lib/why3/plugins/tptp.cmxs
> == Found /usr/local/lib/why3/plugins/tptpfof.cmxs ==
> The plugin /usr/local/lib/why3/plugins/tptpfof.cmxs dynlink failed :
> Dynlink error : error loading shared library:
> dlopen(/usr/local/lib/why3/plugins/tptpfof.cmxs, 134): Symbol not
> found: _camlString
>   Referenced from: /usr/local/lib/why3/plugins/tptpfof.cmxs
>   Expected in: flat namespace
>  in /usr/local/lib/why3/plugins/tptpfof.cmxs
> 
> It seems that some libraries are not loaded before loading these
> plugins.
> 
> Alan
> 
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club





More information about the Why3-club mailing list