From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q1FBH1g1007466 for ; Wed, 15 Feb 2012 12:17:05 +0100 X-IronPort-AV: E=Sophos;i="4.73,422,1325458800"; d="scan'208";a="144344739" Received: from top.irisa.fr (HELO [131.254.16.41]) ([131.254.16.41]) by mail1-relais-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 15 Feb 2012 12:17:05 +0100 From: "Alan Schmitt" To: caml-list Date: Wed, 15 Feb 2012 12:17:05 +0100 Message-ID: MIME-Version: 1.0 Content-Type: text/plain; format=flowed; markup=markdown X-Mailer: MailMate Trial (1.4r2702) Subject: [Caml-list] state of native dynlink on os x Hello, As I'm using more and more programs that use native dynlink, I'm trying to understand what is the state of things on os x. According to this message http://alan.petitepomme.net/cwn/2008.10.21.html natdynlink does not work on 10.5 and above. However, if I read correctly this patch http://caml.inria.fr/mantis/view.php?id=4863 it is enabled for 64 bits architectures. As the patch is in godi, I built a version of ocaml with it, and I'm having mixed results. For some very simple files, things seem to work fine. But if I compile why3 with it (current git version), I get some errors when 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 Note that there was a warning when compiling why3: ld: warning: -read_only_relocs cannot be used with x86_64 So I'm a bit confused as to the current state of things. My questions are: - is native dynlink on os x 64 bits architecture supported in ocaml 3.13dev? - if so, why do I get the ld warning and why does linking fails sometimes? - if not, is there hope it will be supported in the future? Thanks a lot, Alan