diff options
-rw-r--r-- | kernel/nativeconv.ml | 2 | ||||
-rw-r--r-- | kernel/nativelib.ml | 20 | ||||
-rw-r--r-- | kernel/nativelib.mli | 4 | ||||
-rw-r--r-- | library/library.ml | 2 | ||||
-rw-r--r-- | pretyping/nativenorm.ml | 2 |
5 files changed, 16 insertions, 14 deletions
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index c7701a8b1..04747cd8b 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -135,7 +135,7 @@ let native_conv pb sigma env t1 t2 = let ml_filename, prefix = get_ml_filename () in let code, upds = mk_conv_code penv sigma prefix t1 t2 in match compile ml_filename code with - | (0,fn) -> + | (true, fn) -> begin if !Flags.debug then Pp.msg_debug (Pp.str "Running test..."); let t0 = Sys.time () in diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 811319a9b..8cda85ec6 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -32,7 +32,7 @@ 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 ()) + if Dynlink.is_native then ocamlopt () else ocamlc () let ( / ) = Filename.concat @@ -62,20 +62,22 @@ let write_ml_code fn ?(header=[]) code = let call_compiler ml_filename = let load_path = !get_load_paths () in 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 include_dirs = List.flatten (List.map (fun x -> ["-I"; x]) (include_dirs () @ load_path)) in let f = Filename.chop_extension ml_filename in let link_filename = f ^ ".cmo" in let link_filename = Dynlink.adapt_filename link_filename in let remove f = if Sys.file_exists f then Sys.remove f in remove link_filename; remove (f ^ ".cmi"); - let comp_cmd = - Format.sprintf "%s -%s -o %s -rectypes -w a -I %s -impl %s" - compiler_name (if Dynlink.is_native then "shared" else "c") - (Filename.quote link_filename) include_dirs (Filename.quote ml_filename) - in - Sys.command comp_cmd, link_filename + let args = + (if Dynlink.is_native then "-shared" else "-c") + ::"-o"::link_filename + ::"-rectypes" + ::"-w"::"a" + ::include_dirs + @ ["-impl"; ml_filename] in + if !Flags.debug then Pp.msg_debug (Pp.str (compiler_name ^ " " ^ (String.concat " " args))); + CUnix.sys_command compiler_name args = Unix.WEXITED 0, link_filename let compile fn code = write_ml_code fn code; diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli index a2633ac2c..1c60221f0 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.mli @@ -16,9 +16,9 @@ val load_obj : (string -> unit) ref val get_ml_filename : unit -> string * string -val compile : string -> global list -> int * string +val compile : string -> global list -> bool * string -val compile_library : Names.dir_path -> global list -> string -> int +val compile_library : Names.dir_path -> global list -> string -> bool val call_linker : ?fatal:bool -> string -> string -> code_location_updates option -> unit diff --git a/library/library.ml b/library/library.ml index 97c416556..4fea6b836 100644 --- a/library/library.ml +++ b/library/library.ml @@ -724,7 +724,7 @@ let save_library_to ?todo dir f otab = (* Writing native code files *) if not !Flags.no_native_compiler then let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in - if not (Int.equal (Nativelib.compile_library dir ast fn) 0) then + if not (Nativelib.compile_library dir ast fn) then msg_error (str"Could not compile the library to native code. Skipping.") with reraise -> let reraise = Errors.push reraise in diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 274357adb..9af68b46b 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -389,7 +389,7 @@ let native_norm env sigma c ty = let ml_filename, prefix = Nativelib.get_ml_filename () in let code, upd = mk_norm_code penv sigma prefix c in match Nativelib.compile ml_filename code with - | 0,fn -> + | true, fn -> if !Flags.debug then Pp.msg_debug (Pp.str "Running norm ..."); let t0 = Sys.time () in Nativelib.call_linker ~fatal:true prefix fn (Some upd); |