diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2014-04-29 14:41:49 -0400 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2014-04-29 14:41:49 -0400 |
commit | 6acf543800fe176ca7d47ef7165ebc14588efb6f (patch) | |
tree | 1bf524ee47195cc4d3ebdd48113aaeeaf1bc5c1d /kernel | |
parent | 3b176883b7fcd9af6881ae1049bbd078c8d19577 (diff) |
Native compiler: hide compiled files in a .coq-native subdirectory.
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/nativelib.ml | 38 | ||||
-rw-r--r-- | kernel/nativelib.mli | 12 | ||||
-rw-r--r-- | kernel/nativelibrary.ml | 7 | ||||
-rw-r--r-- | kernel/nativelibrary.mli | 3 |
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 |