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, 51 insertions, 0 deletions

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"