Turn mltop.ml4 into a regular ocaml file

 The IFDEF's in mltop.ml4 were there to support platforms with
 a native ocaml compiler but no dynlink.cmxa, a situation that
 should be pretty rare in the Coq community nowadays (playing
 with coqtop on ARM, anyone ?). So we now refuse to build
 a native coqtop unless dynlink.cmxa exists (cf ./configure),
 and we explain how to create a dummy one if necessary
 (cf dev/dynlink.ml). This way, we can clean-up mltop.ml,
 and remove ugly special rules in Makefile and myocamlbuild

 NB: I checked that this shouldn't have any impact on Coq's
 debian packages on exotic architectures (arm, mips, ...),
 since apparently on these architectures no ocamlopt at all
 are shipped, and coq packages are already byte-only

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

1 files changed, 37 insertions, 30 deletions

diff --git a/configure b/configure
index f4b5b7e2ff..1795156f15 100755
--- a/configure
+++ b/configure
@@ -465,36 +465,6 @@ if [ "$coq_debug_flag" = "-g" ]; then
     esac
 fi
 
-# Native dynlink
-if [ "$natdynlink" = "yes" -a -f "$CAMLLIB"/dynlink.cmxa ]; then
-    HASNATDYNLINK=true
-else
-    HASNATDYNLINK=false
-fi
-
-case $HASNATDYNLINK,$ARCH,`uname -r`,$CAMLVERSION in
-    true,Darwin,9.*,3.11.*)  # ocaml 3.11.0 dynlink on MacOS 10.5 is buggy
-        NATDYNLINKFLAG=os5fixme;;
-    #Possibly a problem on 10.6.0/10.6.1/10.6.2
-    #May just be a 32 vs 64 problem for all 10.6.*
-    true,Darwin,10.0.*,3.11.*) # Possibly a problem on 10.6.0
-        NATDYNLINKFLAG=os5fixme;;
-    true,Darwin,10.1.*,3.11.*) # Possibly a problem on 10.6.1
-        NATDYNLINKFLAG=os5fixme;;
-    true,Darwin,10.2.*,3.11.*) # Possibly a problem on 10.6.2
-        NATDYNLINKFLAG=os5fixme;;
-    true,Darwin,10.*,3.11.*)
-        if [ `getconf LONG_BIT` = "32" ]; then
-	    # Still a problem for x86_32
-            NATDYNLINKFLAG=os5fixme
-        else
-	    # Not a problem for x86_64
-            NATDYNLINKFLAG=$HASNATDYNLINK
-        fi;;
-    *)
-        NATDYNLINKFLAG=$HASNATDYNLINK;;
-esac
-
 # Camlp4 / Camlp5 configuration
 
 # Assume that camlp(4|5) binaries are at the same place as ocaml ones
@@ -572,6 +542,13 @@ if [ "$best_compiler" = "opt" ] ; then
 	  best_compiler=byte
 	  echo "Cannot find native-code $CAMLP4,"
 	  echo "only the bytecode version of Coq will be available."
+      elif [ ! -f "$CAMLLIB"/dynlink.cmxa ]; then
+	  best_compiler=byte
+	  echo "Cannot find native-code dynlink library,"
+	  echo "only the bytecode version of Coq will be available."
+	  echo "For building a native-code Coq, you may try to first"
+          echo "compile and install a dummy dynlink.cmxa (see dev/dynlink.ml)"
+          echo "and then run ./configure -natdynlink no"
       else
           if [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then
 	      echo "Native and bytecode compilers do not have the same version!"
@@ -584,6 +561,36 @@ if [ "$best_compiler" = "opt" ] ; then
   fi
 fi
 
+# Native dynlink
+if [ "$natdynlink" = "yes" -a -f "$CAMLLIB"/dynlink.cmxa ]; then
+    HASNATDYNLINK=true
+else
+    HASNATDYNLINK=false
+fi
+
+case $HASNATDYNLINK,$ARCH,`uname -r`,$CAMLVERSION in
+    true,Darwin,9.*,3.11.*)  # ocaml 3.11.0 dynlink on MacOS 10.5 is buggy
+        NATDYNLINKFLAG=os5fixme;;
+    #Possibly a problem on 10.6.0/10.6.1/10.6.2
+    #May just be a 32 vs 64 problem for all 10.6.*
+    true,Darwin,10.0.*,3.11.*) # Possibly a problem on 10.6.0
+        NATDYNLINKFLAG=os5fixme;;
+    true,Darwin,10.1.*,3.11.*) # Possibly a problem on 10.6.1
+        NATDYNLINKFLAG=os5fixme;;
+    true,Darwin,10.2.*,3.11.*) # Possibly a problem on 10.6.2
+        NATDYNLINKFLAG=os5fixme;;
+    true,Darwin,10.*,3.11.*)
+        if [ `getconf LONG_BIT` = "32" ]; then
+	    # Still a problem for x86_32
+            NATDYNLINKFLAG=os5fixme
+        else
+	    # Not a problem for x86_64
+            NATDYNLINKFLAG=$HASNATDYNLINK
+        fi;;
+    *)
+        NATDYNLINKFLAG=$HASNATDYNLINK;;
+esac
+
 # OS dependent libraries
 
 OSDEPLIBS="-cclib -lunix"