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

7 files changed, 99 insertions, 89 deletions

diff --git a/.gitignore b/.gitignore
index c3669497f..2b497f9a9 100644
--- a/.gitignore
+++ b/.gitignore
@@ -136,15 +136,12 @@ tactics/eqdecide.ml
 tactics/extratactics.ml
 tactics/extraargs.ml
 tools/coq_tex.ml
-toplevel/mltop.ml
 toplevel/whelp.ml
 ide/coqide_main.ml
 ide/coqide_main_opt.ml
 
 # other auto-generated files
 
-toplevel/mltop.optml
-toplevel/mltop.byteml
 kernel/byterun/coq_jumptbl.h
 kernel/copcodes.ml
 scripts/tolink.ml
diff --git a/Makefile.build b/Makefile.build
index f2fabf918..6efdf95a4 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -742,27 +742,6 @@ grammar/grammar.cma: | grammar/grammar.mllib.d
 	$(SHOW)'OCAMLC -a $@'   
 	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@
 
-# toplevel/mltop.ml4 (ifdef Byte)
-
-## NB: mltop.ml correspond to the byte version (and hence need no special rules)
-## while the opt version is in mltop.optml. Since mltop.optml uses mltop.ml.d
-## as dependency file, be sure to import the same modules in the different sections
-## of the ml4
-
-MLTOP:=toplevel/mltop
-
-$(MLTOP).cmx: $(MLTOP).optml | $(MLTOP).ml.d $(MLTOP).ml4.d
-	$(SHOW)'OCAMLOPT  $<'
-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -c -impl $< -o $@
-
-$(MLTOP).ml: $(MLTOP).ml4 config/Makefile # no camlp4deps here
-	$(SHOW)'CAMLP4O   $<'
-	$(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -DByte -DHasDynlink -impl $< -o $@
-
-$(MLTOP).optml: $(MLTOP).ml4 config/Makefile # no camlp4deps here
-	$(SHOW)'CAMLP4O   $<'
-	$(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) $(NATDYNLINKDEF) -impl $< -o $@
-
 ide/coqide_main.ml: ide/coqide_main.ml4
 	$(SHOW)'CAMLP4O   $<'
 	$(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -impl $< -o $@
diff --git a/_tags b/_tags
index 3097447c3..b50dbfed2 100644
--- a/_tags
+++ b/_tags
@@ -28,8 +28,6 @@
 
 ## tags for camlp4 files 
 
-"toplevel/mltop.ml4": is_mltop
-
 "toplevel/whelp.ml4": use_grammar
 
 "parsing/g_constr.ml4": use_compat5
diff --git a/configure b/configure
index f4b5b7e2f..1795156f1 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"
diff --git a/dev/dynlink.ml b/dev/dynlink.ml
new file mode 100644
index 000000000..810e0ffca
--- /dev/null
+++ b/dev/dynlink.ml
@@ -0,0 +1,51 @@
+
+(** Some architectures may have a native ocaml compiler but no native
+    dynlink.cmxa (e.g. ARM). If you still want to build a native coqtop
+    there, you'll need this dummy implementation of Dynlink.
+    Compile it and install with:
+
+      ocamlopt -a -o dynlink.cmxa dynlink.ml
+      sudo cp -i dynlink.cmxa `ocamlopt -where`
+
+    Then build coq this way: ./configure -natdynlink no && make world
+*)
+
+let is_native = true (* This file will only be given to the native compiler *)
+
+type linking_error =
+| Undefined_global of string
+| Unavailable_primitive of string
+| Uninitialized_global of string
+
+type error =
+| Not_a_bytecode_file of string
+| Inconsistent_import of string
+| Unavailable_unit of string
+| Unsafe_file
+| Linking_error of string * linking_error
+| Corrupted_interface of string
+| File_not_found of string
+| Cannot_open_dll of string
+| Inconsistent_implementation of string
+
+exception Error of error
+
+let error_message = function
+  | Not_a_bytecode_file s -> "Native dynamic link not supported (module "^s^")"
+  | _ -> "Native dynamic link not supported"
+
+let loadfile : string -> unit = fun s -> raise (Error (Not_a_bytecode_file s))
+let loadfile_private = loadfile
+
+let adapt_filename s = s
+
+let init () = ()
+let allow_only : string list -> unit = fun _ -> ()
+let prohibit : string list -> unit = fun _ -> ()
+let default_available_units : unit -> unit = fun _ -> ()
+let allow_unsafe_modules : bool -> unit = fun _ -> ()
+let add_interfaces : string list -> string list -> unit = fun _ _ -> ()
+let add_available_units : (string * Digest.t) list -> unit = fun _ -> ()
+let clear_available_units : unit -> unit = fun _ -> ()
+let digest_interface : string -> string list -> Digest.t =
+ fun _ _ -> failwith "digest_interface"
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index 0ed205350..793522f84 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -299,26 +299,6 @@ let extra_rules () = begin
   mlp_cmo "tools/compat5b";
   end;
 
-(** Special case of toplevel/mltop.ml4:
-    - mltop.ml will be the old mltop.optml and be used to obtain mltop.cmx
-    - we add a special mltop.ml4 --> mltop.cmo rule, before all the others
-*)
-  flag ["is_mltop"; "p4option"] flag_dynlink;
-
-(*TODO: this is rather ugly for a simple file, we should try to
-        benefit more from predefined rules *)
-  let mltop = "toplevel/mltop" in
-  let ml4 = mltop^".ml4" and mlo = mltop^".cmo" and
-      ml = mltop^".ml" and mld = mltop^".ml.depends"
-  in
-  rule "mltop_byte" ~deps:[ml4;mld]  ~prod:mlo ~insert:`top
-    (fun env build ->
-       Ocaml_compiler.prepare_compile build ml;
-       Cmd (S [!Options.ocamlc; A"-c"; A"-pp";
-	       Quote (S [camlp4o; T(tags_of_pathname ml4 ++ "p4mod");
-			 A"-DByte";A"-DHasDynlink";camlp4compat;A"-impl"]);
-	       camlp4incl; incl ml4; A"-impl"; P ml4]));
-
 (** All caml files are compiled with +camlp4/5
     and ide files need +lablgtk2 *)
 
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml
index 09dd2a67f..2ca3a4cd7 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml
@@ -37,6 +37,14 @@ open System
    (I do not know of a solution to this problem, other than to
    put all the needed names into the ML Module object.) *)
 
+
+(* NB: this module relies on OCaml's Dynlink library. The bytecode version
+   of Dynlink is always available, but there are some architectures
+   with native compilation and no dynlink.cmxa. Instead of nasty IFDEF's
+   here for hiding the calls to Dynlink, we now simply reject this rather
+   rare situation during ./configure, and give instructions there about how
+   to build a dummy dynlink.cmxa, cf. dev/dynlink.ml. *)
+
 (* This path is where we look for .cmo *)
 let coq_mlpath_copy = ref ["."]
 let keep_copy_mlpath path =
@@ -61,7 +69,7 @@ type kind_load =
 let load = ref WithoutTop
 
 (* Are we in a native version of Coq? *)
-let is_native = IFDEF Byte THEN false ELSE true END
+let is_native = Dynlink.is_native
 
 (* Sets and initializes a toplevel (if any) *)
 let set_top toplevel = load := WithTop toplevel
@@ -76,7 +84,7 @@ let is_ocaml_top () =
     |_ -> false
 
 (* Tests if we can load ML files *)
-let has_dynlink = IFDEF HasDynlink THEN true ELSE false END
+let has_dynlink = Coq_config.has_natdynlink || not is_native
 
 (* Runs the toplevel loop of Ocaml *)
 let ocaml_toploop () =
@@ -93,23 +101,13 @@ let dir_ml_load s =
        | (UserError _ | Failure _ | Anomaly _ | Not_found as u) -> raise u
        | _ -> errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++
                 str s ++ str" to Coq code."))
-(* TO DO: .cma loading without toplevel *)
     | WithoutTop ->
-      IFDEF HasDynlink THEN
-	(* WARNING
-	 * if this code section starts to use a module not used elsewhere
-	 * in this file, the Makefile dependency logic needs to be updated.
-	 *)
         let warn = Flags.is_verbose() in
         let _,gname = find_file_in_path ~warn !coq_mlpath_copy s in
         try
           Dynlink.loadfile gname;
-	with | Dynlink.Error a ->
+	with Dynlink.Error a ->
           errorlabstrm "Mltop.load_object" (str (Dynlink.error_message a))
-      ELSE
-        errorlabstrm "Mltop.no_load_object"
-            (str"Loading of ML object file forbidden in a native Coq.")
-      END
 
 (* Dynamic interpretation of .ml *)
 let dir_ml_use s =