aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2014-04-29 14:41:49 -0400
committerGravatar Maxime Dénès <mail@maximedenes.fr>2014-04-29 14:41:49 -0400
commit6acf543800fe176ca7d47ef7165ebc14588efb6f (patch)
tree1bf524ee47195cc4d3ebdd48113aaeeaf1bc5c1d /kernel
parent3b176883b7fcd9af6881ae1049bbd078c8d19577 (diff)
Native compiler: hide compiled files in a .coq-native subdirectory.
Diffstat (limited to 'kernel')
-rw-r--r--kernel/nativelib.ml38
-rw-r--r--kernel/nativelib.mli12
-rw-r--r--kernel/nativelibrary.ml7
-rw-r--r--kernel/nativelibrary.mli3
4 files changed, 36 insertions, 24 deletions
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index a69b9d472..05e470da9 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -20,10 +20,16 @@ let get_load_paths =
let open_header = ["Nativevalues";
"Nativecode";
"Nativelib";
- "Nativeconv";
+ "Nativeconv";
"Declaremods"]
let open_header = List.map mk_open open_header
+(* Directory where compiled files are stored *)
+let output_dir = ".coq-native"
+
+(* Extension of genereted ml files, stored for debugging purposes *)
+let source_ext = ".native"
+
(* Global settings and utilies for interface with OCaml *)
let compiler_name =
Filename.quote (if Dynlink.is_native then ocamlopt () else ocamlc ())
@@ -42,18 +48,19 @@ let rt1 = ref (dummy_value ())
let rt2 = ref (dummy_value ())
let get_ml_filename () =
- let filename = Filename.temp_file "Coq_native" ".native" in
+ let filename = Filename.temp_file "Coq_native" source_ext in
let prefix = Filename.chop_extension (Filename.basename filename) ^ "." in
filename, prefix
-let write_ml_code ml_filename ?(header=[]) code =
+let write_ml_code fn ?(header=[]) code =
let header = open_header@header in
- let ch_out = open_out ml_filename in
+ let ch_out = open_out fn in
let fmt = Format.formatter_of_out_channel ch_out in
List.iter (pp_global fmt) (header@code);
close_out ch_out
let call_compiler ml_filename load_path =
+ let load_path = List.map (fun dn -> dn / output_dir) load_path in
let include_dirs = List.map Filename.quote (include_dirs () @ load_path) in
let include_dirs = String.concat " -I " include_dirs in
let f = Filename.chop_extension ml_filename in
@@ -66,15 +73,26 @@ let call_compiler ml_filename load_path =
in
Sys.command comp_cmd, link_filename
-let compile ml_filename code =
- write_ml_code ml_filename code;
- call_compiler ml_filename (!get_load_paths())
+let compile fn code =
+ write_ml_code fn code;
+ call_compiler fn (!get_load_paths())
+
+let compile_library dir code load_path fn =
+ let header = mk_library_header dir in
+ let fn = fn ^ source_ext in
+ let basename = Filename.basename fn in
+ let dirname = Filename.dirname fn in
+ let dirname = dirname / output_dir in
+ if not (Sys.file_exists dirname) then Unix.mkdir dirname 0o755;
+ let fn = dirname / basename in
+ write_ml_code fn ~header code;
+ fst (call_compiler fn load_path)
(* call_linker links dynamically the code for constants in environment or a *)
(* conversion test. Silently fails if the file does not exist in bytecode *)
(* mode, since the standard library is not compiled to bytecode with default *)
(* settings. *)
-let call_linker ~fatal prefix f upds =
+let call_linker ?(fatal=true) prefix f upds =
rt1 := dummy_value ();
rt2 := dummy_value ();
if Dynlink.is_native || Sys.file_exists f then
@@ -88,3 +106,7 @@ let call_linker ~fatal prefix f upds =
let msg = "Dynlink error" in
if fatal then anomaly (Pp.str msg) else Pp.msg_warning (Pp.str msg));
match upds with Some upds -> update_locations upds | _ -> ()
+
+let link_library ~prefix ~dirname ~basename =
+ let f = dirname / output_dir / basename in
+ call_linker ~fatal:false prefix f None
diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli
index 9ef8c06a3..e577a9032 100644
--- a/kernel/nativelib.mli
+++ b/kernel/nativelib.mli
@@ -16,15 +16,15 @@ val load_obj : (string -> unit) ref
val get_ml_filename : unit -> string * string
-val write_ml_code : string ->
- ?header:Nativecode.global list -> global list -> unit
-
-val call_compiler : string -> string list -> int * string
-
val compile : string -> global list -> int * string
+val compile_library : Names.dir_path ->
+ global list -> string list -> string -> int
+
val call_linker :
- fatal:bool -> string -> string -> code_location_updates option -> unit
+ ?fatal:bool -> string -> string -> code_location_updates option -> unit
+
+val link_library : prefix:string -> dirname:string -> basename:string -> unit
val rt1 : Nativevalues.t ref
val rt2 : Nativevalues.t ref
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 6749dbfdb..f33e1eaa6 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -72,10 +72,3 @@ let dump_library mp dp env mod_expr =
let mlcode = add_header_comment (List.rev mlcode) time_info in
mlcode, get_symbols_tbl ()
| _ -> assert false
-
-
-let compile_library dir code load_path f =
- let header = mk_library_header dir in
- let ml_filename = f^".native" in
- write_ml_code ml_filename ~header code;
- fst (call_compiler ml_filename load_path)
diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli
index a45402a43..1de26b72c 100644
--- a/kernel/nativelibrary.mli
+++ b/kernel/nativelibrary.mli
@@ -15,6 +15,3 @@ compiler *)
val dump_library : module_path -> dir_path -> env -> module_signature ->
global list * symbol array
-
-val compile_library :
- dir_path -> global list -> string list -> string -> int