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

Reviewed-by: gares
Reviewed-by: maximedenes

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