diff options
Diffstat (limited to 'dev/dynlink.ml')
-rw-r--r-- | dev/dynlink.ml | 51 |
1 files changed, 51 insertions, 0 deletions
diff --git a/dev/dynlink.ml b/dev/dynlink.ml new file mode 100644 index 00000000..810e0ffc --- /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" |