From 9d52407e9fccf27d02d952d40f3758dfe1898767 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 1 Apr 2019 19:09:59 +0200
Subject: [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.
---
 kernel/nativelib.ml  | 8 ++++----
 kernel/nativelib.mli | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'kernel')

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
 
-- 
cgit v1.2.3


From d8ee64ace969287dbec6ba2777c08f19a25cab26 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 12 Feb 2020 11:55:54 +0100
Subject: [native compiler] Allow to set OCaml include dirs for compilation

`Nativelib` currently assumes that objects are built in some
particular directories, but this is not true in some cases, for
example, when building with Dune.

We add a new option `-nI` to allow clients to specify the OCaml
include dirs.
---
 kernel/nativelib.ml  | 11 ++++++++---
 kernel/nativelib.mli |  1 +
 2 files changed, 9 insertions(+), 3 deletions(-)

(limited to 'kernel')

diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 60d4d84705..86eaaddc90 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -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
@@ -89,7 +94,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 include_dirs = List.flatten (List.map (fun x -> ["-I"; x]) (include_dirs () @ 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
diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli
index 4d95f822e7..155fde54e9 100644
--- a/kernel/nativelib.mli
+++ b/kernel/nativelib.mli
@@ -14,6 +14,7 @@ used by the native compiler. *)
 
 (* Directory where compiled files are stored *)
 val output_dir : CUnix.physical_path ref
+val include_dirs : CUnix.physical_path list ref
 
 val get_load_paths : (unit -> string list) ref
 
-- 
cgit v1.2.3