Merge PR #11581: [native compiler] Add options to set object directories.

Reviewed-by: gares
Reviewed-by: maximedenes

6 files changed, 38 insertions, 10 deletions

diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index a62b51e8aa..86eaaddc90 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"
@@ -51,8 +51,13 @@ let () = at_exit (fun () ->
    be guessed until flags have been properly initialized. It also lets
    us avoid forcing [my_temp_dir] if we don't need it (eg stdlib file
    without native compute or native conv uses). *)
-let include_dirs () =
-  let base = [Envars.coqlib () / "kernel"; Envars.coqlib () / "library"] in
+let include_dirs = ref []
+let get_include_dirs () =
+  let base = match !include_dirs with
+  | [] ->
+    [Envars.coqlib () / "kernel"; Envars.coqlib () / "library"]
+  | _::_ as l -> l
+  in
   if Lazy.is_val my_temp_dir
   then (Lazy.force my_temp_dir) :: base
   else base
@@ -88,8 +93,8 @@ 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 include_dirs = List.flatten (List.map (fun x -> ["-I"; x]) (include_dirs () @ 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]) (get_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
@@ -139,7 +144,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 +186,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..155fde54e9 100644
--- a/kernel/nativelib.mli
+++ b/kernel/nativelib.mli
@@ -13,7 +13,8 @@ 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 include_dirs : CUnix.physical_path list ref
 
 val get_load_paths : (unit -> string list) ref
 
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 2b79bff1b2..949a13974c 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -55,6 +55,8 @@ type coqargs_config = {
   color       : color;
   enable_VM   : bool;
   native_compiler : native_compiler;
+  native_output_dir : CUnix.physical_path;
+  native_include_dirs : CUnix.physical_path list;
   stm_flags   : Stm.AsyncOpts.stm_opt;
   debug       : bool;
   diffs_set   : bool;
@@ -121,6 +123,8 @@ let default_config = {
   color        = `AUTO;
   enable_VM    = true;
   native_compiler = default_native;
+  native_output_dir = ".coq-native";
+  native_include_dirs = [];
   stm_flags    = Stm.AsyncOpts.default_opts;
   debug        = false;
   diffs_set    = false;
@@ -261,8 +265,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 +491,14 @@ 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 } }
+
+    |"-nI" ->
+      let include_dir = next () in
+      { oval with config = {oval.config with native_include_dirs = include_dir :: oval.config.native_include_dirs } }
+
     (* Options with zero arg *)
     |"-async-queries-always-delegate"
     |"-async-proofs-always-delegate"
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index f38381a086..aba6811f43 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -31,6 +31,8 @@ type coqargs_config = {
   color       : color;
   enable_VM   : bool;
   native_compiler : native_compiler;
+  native_output_dir : CUnix.physical_path;
+  native_include_dirs : CUnix.physical_path list;
   stm_flags   : Stm.AsyncOpts.stm_opt;
   debug       : bool;
   diffs_set   : bool;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 46dd693155..1ea48ee766 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -239,6 +239,10 @@ let init_execution opts custom_init =
 
   set_options opts.config.set_options;
 
+  (* Native output dir *)
+  Nativelib.output_dir := opts.config.native_output_dir;
+  Nativelib.include_dirs := opts.config.native_include_dirs;
+
   (* Allow the user to load an arbitrary state here *)
   inputstate opts.pre;
 
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index ba3deeb2f6..c7e1d607f4 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -94,6 +94,8 @@ 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  -nI dir                OCaml include directories for the native compiler (default if not set) \
 \n  -h, -help, --help      print this list of options\
 \n"