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

Reviewed-by: gares
Reviewed-by: maximedenes

4 files changed, 24 insertions, 2 deletions

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"