Fix for #3154: use CUnix.sys_command to call native compiler.

Patch by CJ on bugzilla. CUnix.sys_command doesn't rely on a shell, so extra
care with cmd.exe vs sh is no longer required.

3 files changed, 14 insertions, 12 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