blob: 810e0ffcaeb219b77461b099fbad9738d0a75d4e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
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"
|
