[native compiler] Allow to set the output directory for cmx objects

This is useful in order to implement native support in Dune for
example, which as of today as strict target rules.

Hopefully this option could go away; it is really internal, but I've
chosen to document it.

6 files changed, 20 insertions, 7 deletions

diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index a62b51e8aa..60d4d84705 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -25,7 +25,7 @@ let open_header = ["Nativevalues";
 let open_header = List.map mk_open open_header
 
 (* Directory where compiled files are stored *)
-let output_dir = ".coq-native"
+let output_dir = ref ".coq-native"
 
 (* Extension of generated ml files, stored for debugging purposes *)
 let source_ext = ".native"
@@ -88,7 +88,7 @@ let error_native_compiler_failed e =
 
 let call_compiler ?profile:(profile=false) ml_filename =
   let load_path = !get_load_paths () in
-  let load_path = List.map (fun dn -> dn / output_dir) load_path in
+  let load_path = List.map (fun dn -> dn / !output_dir) load_path 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
@@ -139,7 +139,7 @@ let compile_library dir code fn =
   let fn = fn ^ source_ext in
   let basename = Filename.basename fn in
   let dirname = Filename.dirname fn in
-  let dirname = dirname / output_dir in
+  let dirname = dirname / !output_dir in
   let () =
     try Unix.mkdir dirname 0o755
     with Unix.Unix_error (Unix.EEXIST, _, _) -> ()
@@ -181,5 +181,5 @@ let call_linker ?(fatal=true) env ~prefix f upds =
   match upds with Some upds -> update_locations upds | _ -> ()
 
 let link_library env ~prefix ~dirname ~basename =
-  let f = dirname / output_dir / basename in
+  let f = dirname / !output_dir / basename in
   call_linker env ~fatal:false ~prefix f None
diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli
index 52d18acca6..4d95f822e7 100644
--- a/kernel/nativelib.mli
+++ b/kernel/nativelib.mli
@@ -13,7 +13,7 @@ open Nativecode
 used by the native compiler. *)
 
 (* Directory where compiled files are stored *)
-val output_dir : string
+val output_dir : CUnix.physical_path ref
 
 val get_load_paths : (unit -> string list) ref
 
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 2b79bff1b2..94d0831244 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -55,6 +55,7 @@ type coqargs_config = {
   color       : color;
   enable_VM   : bool;
   native_compiler : native_compiler;
+  native_output_dir : CUnix.physical_path;
   stm_flags   : Stm.AsyncOpts.stm_opt;
   debug       : bool;
   diffs_set   : bool;
@@ -121,6 +122,7 @@ let default_config = {
   color        = `AUTO;
   enable_VM    = true;
   native_compiler = default_native;
+  native_output_dir = ".coq-native";
   stm_flags    = Stm.AsyncOpts.default_opts;
   debug        = false;
   diffs_set    = false;
@@ -261,8 +263,10 @@ let get_cache opt = function
 let get_native_name s =
   (* We ignore even critical errors because this mode has to be super silent *)
   try
-    String.concat "/" [Filename.dirname s;
-      Nativelib.output_dir; Library.native_name_from_filename s]
+    Filename.(List.fold_left concat (dirname s)
+                [ !Nativelib.output_dir
+                ; Library.native_name_from_filename s
+                ])
   with _ -> ""
 
 let get_compat_file = function
@@ -485,6 +489,10 @@ let parse_args ~help ~init arglist : t * string list =
       let opt = to_opt_key opt in
       { oval with config = { oval.config with set_options = (opt, OptionUnset) :: oval.config.set_options }}
 
+    |"-native-output-dir" ->
+      let native_output_dir = next () in
+      { oval with config = { oval.config with native_output_dir } }
+
     (* Options with zero arg *)
     |"-async-queries-always-delegate"
     |"-async-proofs-always-delegate"
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index f38381a086..f0d7851c9d 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -31,6 +31,7 @@ type coqargs_config = {
   color       : color;
   enable_VM   : bool;
   native_compiler : native_compiler;
+  native_output_dir : CUnix.physical_path;
   stm_flags   : Stm.AsyncOpts.stm_opt;
   debug       : bool;
   diffs_set   : bool;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 46dd693155..2509e3b68b 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -239,6 +239,9 @@ let init_execution opts custom_init =
 
   set_options opts.config.set_options;
 
+  (* Native output dir *)
+  Nativelib.output_dir := opts.config.native_output_dir;
+
   (* Allow the user to load an arbitrary state here *)
   inputstate opts.pre;
 
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index ba3deeb2f6..4c622c6e28 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -94,6 +94,7 @@ let print_usage_common co command =
 \n                          for full Gc stats dump)\
 \n  -bytecode-compiler (yes|no)        enable the vm_compute reduction machine\
 \n  -native-compiler (yes|no|ondemand) enable the native_compute reduction machine\
+\n  -native-output-dir     <directory> set the output directory for native objects\
 \n  -h, -help, --help      print this list of options\
 \n"