Workaround to compile the coq archive with dynamic loading on Mac OS 10.5

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11777 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 29 insertions, 9 deletions

diff --git a/Makefile.build b/Makefile.build
index bada7f20e2..9cfe95d1cf 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -883,7 +883,25 @@ endif
 
 %.cmxs: %.cmxa
 	$(SHOW)'OCAMLOPT  $<'
+ifneq ($(HASNATDYNLINK),os5fixme)
 	$(HIDE)$(OCAMLOPT) -linkall -shared -o $@ $<
+else
+	$(HIDE)$(OCAMLOPT) -dstartup -linkall -shared -o $@ $<
+#	Fix1: add a dummy instruction before the caml generic functions
+#	Fix2: make all caml generic functions private
+	$(HIDE)rm -f $@ $@.startup.fixed.s
+	$(HIDE)cat $@.startup.s | sed \
+	  -e "s/_caml_shared_startup__code_begin:/_caml_shared_startup__code_begin:	ret/" \
+	  -e "s/.globl	_caml_curry/.private_extern	_caml_curry/" \
+	  -e "s/.globl	_caml_apply/.private_extern	_caml_apply/" \
+	  -e "s/.globl	_caml_tuplify/.private_extern	_caml_tuplify/" \
+	  > $@.startup.fixed.s
+#	Recompile fixed startup code
+	$(HIDE)as -o $@.startup.o $@.startup.fixed.s
+#	Build fixed .cmxs (assume plugins are on directory base and include all files)
+	$(HIDE)ld -bundle -flat_namespace -undefined warning -read_only_relocs suppress -o $@ `dirname $@`/*.o
+	$(HIDE)rm $@.startup.o $@.startup.s $@.startup.fixed.s
+endif
 
 %.cmxs: %.cmx
 	$(SHOW)'OCAMLOPT  $<'
diff --git a/Makefile.common b/Makefile.common
index 0642c5ce25..7ff2c6b051 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -30,7 +30,7 @@ CHICKENOPT:=bin/coqchk.opt$(EXE)
 BESTCHICKEN:=bin/coqchk.$(BEST)$(EXE)
 CHICKEN:=bin/coqchk$(EXE)
 
-ifeq ($(HASNATDYNLINK),true)
+ifneq ($(HASNATDYNLINK),false)
   DYNLINKCMXA:=dynlink.cmxa
   NATDYNLINKDEF:=-DHasDynlink
 endif
@@ -340,7 +340,7 @@ CONTRIBSTATIC:=\
         $(CCCMO)  $(FOCMO) $(SUBTACCMO) $(RTAUTOCMO) \
         $(FUNINDCMO)
 
-ifeq ($(HASNATDYNLINK),true)
+ifneq ($(HASNATDYNLINK),false)
  CONTRIBSTATIC:=$(SUBTACCMO)
  INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) $(DPCMA) \
 	$(XMLCMA) $(FUNINDCMA) #$(SUBTACCMA)
diff --git a/configure b/configure
index e1b17a64f2..ee298d1280 100755
--- a/configure
+++ b/configure
@@ -445,16 +445,18 @@ fi
 
 # Native dynlink
 if [ "$natdynlink" = "yes" -a -f `"$CAMLC" -where`/dynlink.cmxa ]; then
-    case `uname -s`,`uname -r`,$CAMLVERSION in
-        Darwin,9.*,3.11.0)  # ocaml 3.11.0 dynlink on MacOS 10.5 is buggy
-            HASNATDYNLINK=false;;
-        *)
-            HASNATDYNLINK=true;;
-    esac
+    HASNATDYNLINK=true
 else
     HASNATDYNLINK=false
 fi
 
+case $HASNATDYNLINK,`uname -s`,`uname -r`,$CAMLVERSION in
+    true,Darwin,9.*,3.11.*)  # ocaml 3.11.0 dynlink on MacOS 10.5 is buggy
+        NATDYNLINKFLAG=os5fixme;;
+    *)
+        NATDYNLINKFLAG=$HASNATDYNLINK;;
+esac
+
 # Camlp4 / Camlp5 configuration
 
 if [ "$camlp5dir" != "" ]; then
@@ -998,7 +1000,7 @@ sed -e "s|LOCALINSTALLATION|$local|" \
     -e "s|COQIDEOPT|$COQIDE|" \
     -e "s|CHECKEDOUTSOURCETREE|$checkedout|" \
     -e "s|WITHDOCOPT|$with_doc|" \
-    -e "s|HASNATIVEDYNLINK|$HASNATDYNLINK|" \
+    -e "s|HASNATIVEDYNLINK|$NATDYNLINKFLAG|" \
       "$COQSRC/config/Makefile.template" > "$COQSRC/config/Makefile"
 
 chmod a-w "$COQSRC/config/Makefile"