From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q1RHnvrl004061 for ; Mon, 27 Feb 2012 18:49:57 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AvMBAObBS0/RVaC2kGdsb2JhbAApGoUnnFOISAGJFwgiAQEBAQkJDQcUBCOBcwEBAQMBEgIPHQEbEgsBAwELBgMCCxodAgIiAREBBQEKEgYTEhCHXwULKZpECosmTIJxhR4/iHQBBQuMbBkIAwEBAVAJAQqEWQEbEAEmEQgGBQMBBAQHBQYDAggDBQOCF4EWBIJdkmCOLj2EBA X-IronPort-AV: E=Sophos;i="4.73,491,1325458800"; d="scan'208";a="133223341" Received: from mail-gy0-f182.google.com ([209.85.160.182]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 27 Feb 2012 18:49:51 +0100 Received: by ghrr20 with SMTP id r20so1759956ghr.27 for ; Mon, 27 Feb 2012 09:49:50 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=6iyVn7fMuRkVeilGHObRIBS0+Bjcmx9v6VSVHYnEj4M=; b=EQS6Ef1QQoFzK5kLsesCgHkyZr8PwwFS5K1eg3W8hc5qvfBZgrlCZbrpww1+kXitfh LRRhehemcHF3v2IjUwLeGgqZsQqlIxi+n483RXtu8ZqaKN7ePsMW829lrzd+LxZlLfZw 6XmthL8DtdK4I2M8eYGgnWQyDhX0ZliNqw7tY= Received: by 10.236.116.195 with SMTP id g43mr16952887yhh.26.1330364990277; Mon, 27 Feb 2012 09:49:50 -0800 (PST) MIME-Version: 1.0 Received: by 10.236.67.47 with HTTP; Mon, 27 Feb 2012 09:49:30 -0800 (PST) In-Reply-To: References: <74F89B4A-9C34-4A33-8DAA-8A12CF9EF03B@polytechnique.org> From: Pierre-Alexandre Voye Date: Mon, 27 Feb 2012 18:49:30 +0100 Message-ID: To: Damien Doligez Cc: caml-list Content-Type: multipart/alternative; boundary=20cf303dd654aac90904b9f5bc5c Subject: Re: [Caml-list] state of native dynlink on os x --20cf303dd654aac90904b9f5bc5c Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable 2012/2/27 Damien Doligez > Hi Alan, > > Following a suggestion by Daniel B=C3=BCnzli, I used the minimum exampl= e from > http://caml.inria.fr/mantis/view.php?id=3D5093 then I can see that native > dynlink does work. > > > > However two questions remain. I get `ld: warning: -read_only_relocs > cannot be used with x86_64` each time I link natively. Does this mean I > should reopen http://caml.inria.fr/mantis/view.php?id=3D4863 (the patch > there is applied to my version of caml)? > > Which version of Mac OS X, which version of OCaml, and what is the output > of configure? > I had it in Mac Lion ( 10.7.3 - 11.3.0 Darwin Kernel Version 11.3.0: Thu Jan 12 18:47:41 PST 2012; root:xnu-1699.24.23~1/RELEASE_X86_64 x86_64 ) Example, compiling Ocsigen : (end of make...) ocamlfind ocamlc -thread -o ocsigenserver -linkpkg -linkall -thread -I ../baselib -I ../http -package lwt.ssl -package lwt.extra -package netstring -package findlib -package cryptokit -package tyxml -package tyxml.parser -package dynlink -package tyxml.syntax -I . ../baselib/parsecommandline.cma ../baselib/baselib.cma ../baselib/polytables.cma ../http/http.cma ocsigenserver.cma server_main.cmo File "_none_", line 1, characters 0-1: Error: Error while linking /opt/local/lib/ocaml/camlp4/camlp4lib.cma(Camlp4): Reference to undefined global `Dynlink' make[4]: *** [ocsigenserver] Error 2 make[3]: *** [all] Error 2 make[2]: *** [all] Error 2 make[1]: *** [do-ocsigenserver-build] Error 2 make: *** [.ocsigenserver-build] Error 2 > > Also, when running why3, I get some undefined symbols (_camlRandom, > _camlParsing, _camlString). Where are these symbols defined? > > Looks like modules of the standard library, right ? > > > Here, i have : File "_none_", line 1, characters 0-1: Error: Cannot find file dynlink.cmxa make: *** [bin/why3config.opt] Error 2 make: *** Waiting for unfinished jobs.... configure of why3 : $ ./configure --enable-menhirlib --enable-doc checking executable suffix... checking for ocamlc... ocamlc ocaml version is 3.12.1 ocaml library path is /opt/local/lib/ocaml checking for ocamlopt... ocamlopt checking ocamlopt version... ok checking for ocamlc.opt... ocamlc.opt checking ocamlc.opt version... ok checking for ocamlopt.opt... ocamlopt.opt checking ocamlc.opt version... ok checking for ocamldep... ocamldep checking for ocamldep.opt... ocamldep.opt checking for ocamllex... ocamllex checking for ocamllex.opt... ocamllex.opt checking for ocamlyacc... ocamlyacc checking for ocamldoc... ocamldoc checking for ocamldoc.opt... ocamldoc.opt checking for camlp5o... camlp5o checking for ocamlfind... yes checking for menhir... menhir ocamlfind found menhir library in /opt/local/lib/ocaml/site-lib/menhirLib checking for rubber... no configure: WARNING: cannot find rubber ocamlfind found lablgtk2 in /opt/local/lib/ocaml/lablgtk2 ocamlfind found sqlite3 in /opt/local/lib/ocaml/site-lib/sqlite3 checking for coqc... coqc checking Coq version... 8.3pl2 checking for /usr/local/lib/coq/kernel/term.cmi... yes ocamlfind found ocamlgraph in /opt/local/lib/ocaml/site-lib/ocamlgraph configure: creating ./config.status config.status: creating Makefile config.status: creating src/config.sh config.status: creating doc/version.tex config.status: creating share/provers-detection-data.conf config.status: creating META config.status: executing chmod commands Summary ----------------------------------------- OCaml version : 3.12.1 OCaml library path : /opt/local/lib/ocaml Verbose make : no Why IDE : yes Why bench tool : yes Why documentation : no Why plugins : yes Coq plugin support : no (not yet implemented) TPTP parser : yes Menhir library : yes hypothesis selection : yes profiling : no localdir : no > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa-roc.inria.fr/wws/info/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > > --=20 --------------------- https://twitter.com/#!/ontologiae/ http://linuxfr.org/users/montaigne --20cf303dd654aac90904b9f5bc5c Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable

2012/2/27 Damien Doligez <damien.= doligez@inria.fr>
Hi Alan,
> Following a suggestion by Daniel B=C3=BCnzli, I used the minimum = example from http://caml.inria.fr/mantis/view.php?id=3D5093 then I ca= n see that native dynlink does work.
>
> However two questions remain. I get `ld: warning: -read_only_relocs ca= nnot be used with x86_64` each time I link natively. Does this mean I shoul= d reopen http://caml.inria.fr/mantis/view.php?id=3D4863 (the patch t= here is applied to my version of caml)?

Which version of Mac OS X, which version of OCaml, and what is the ou= tput of configure?
I had it in Mac Lion ( 10.7.3=C2=A0= - 11.3.0 Darwin Kernel Version 11.3.0: Thu Jan 12 18:47:41 PST 2012; root:= xnu-1699.24.23~1/RELEASE_X86_64 x86_64 )
Example, compiling Ocsigen :
(end of make...)
ocamlfind ocamlc=C2=A0 = -thread -o ocsigenserver -linkpkg -linkall=C2=A0 -thread -I ../baselib -I .= ./http -package lwt.ssl -package lwt.extra -package netstring -package find= lib -package cryptokit -package tyxml -package tyxml.parser -package dynlin= k -package tyxml.syntax -I . ../baselib/parsecommandline.cma ../baselib/bas= elib.cma ../baselib/polytables.cma ../http/http.cma ocsigenserver.cma serve= r_main.cmo
File "_none_", line 1, characters 0-1:
Error: Error while link= ing /opt/local/lib/ocaml/camlp4/camlp4lib.cma(Camlp4):
Reference to unde= fined global `Dynlink'
make[4]: *** [ocsigenserver] Error 2
make[3]: *** [all] Error 2
make[2]: *** [all] Error 2
make[1]: *** [do-ocsigenserver-build] Error 2=
make: *** [.ocsigenserver-build] Error 2


> Also, when running why3, I get some undefined symbols (_camlRandom, _c= amlParsing, _camlString). Where are these symbols defined?

Looks like modules of the standard library, right ?


Here, i have :
File "_none_"= , line 1, characters 0-1:
Error: Cannot find file dynlink.cmxa
make: = *** [bin/why3config.opt] Error 2
make: *** Waiting for unfinished jobs..= ..

configure of why3 :
$ ./configure=C2=A0 --enable-menhirlib --enable-= doc
checking executable suffix... <none>
checking for ocamlc...= ocamlc
ocaml version is 3.12.1
ocaml library path is /opt/local/lib/ocaml
checking for ocamlopt... ocamlopt
checking ocamlopt version... ok
che= cking for ocamlc.opt... ocamlc.opt
checking ocamlc.opt version... ok
= checking for ocamlopt.opt... ocamlopt.opt
checking ocamlc.opt version...= ok
checking for ocamldep... ocamldep
checking for ocamldep.opt... ocamldep.= opt
checking for ocamllex... ocamllex
checking for ocamllex.opt... oc= amllex.opt
checking for ocamlyacc... ocamlyacc
checking for ocamldoc.= .. ocamldoc
checking for ocamldoc.opt... ocamldoc.opt
checking for camlp5o... camlp5= o
checking for ocamlfind... yes
checking for menhir... menhir
ocam= lfind found menhir library in /opt/local/lib/ocaml/site-lib/menhirLib
checking for rubber... no
configure: WARNING: cannot find rubber
ocam= lfind found lablgtk2 in /opt/local/lib/ocaml/lablgtk2
ocamlfind found sq= lite3 in /opt/local/lib/ocaml/site-lib/sqlite3
checking for coqc... coqc=
checking Coq version... 8.3pl2
checking for /usr/local/lib/coq/kernel/te= rm.cmi... yes
ocamlfind found ocamlgraph in /opt/local/lib/ocaml/site-li= b/ocamlgraph
configure: creating ./config.status
config.status: creat= ing Makefile
config.status: creating src/config.sh
config.status: creating doc/versio= n.tex
config.status: creating share/provers-detection-data.conf
confi= g.status: creating META
config.status: executing chmod commands

=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0 Summary
-----------------------------------------<= br>OCaml version=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0 : 3.12.1=
OCaml library path=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 : /opt/local/lib/ocaml=
Verbose make=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0 : no
Why IDE=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 : yes
Why bench tool=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 : yes<= br>Why documentation=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 : no
Why plugin= s=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 := yes
Coq plugin support=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 : no=C2=A0 (not ye= t implemented)
TPTP parser=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0 : yes
Menhir library=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 : yes
hypothesis selection=C2=A0=C2=A0=C2= =A0 : yes
profiling=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0 : no
localdir=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 : no

--
Caml-list mailing list. =C2=A0Subscription management and archives:
https://sympa-roc.inria.fr/wws/info/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs




--
-----------= ----------
https://twitter.com/#!/ontologiae/
http://linuxfr.org/users/montaigne

--20cf303dd654aac90904b9f5bc5c--