diff options
| author | Emilio Jesus Gallego Arias | 2020-02-12 11:55:54 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-26 16:10:40 -0500 |
| commit | d8ee64ace969287dbec6ba2777c08f19a25cab26 (patch) | |
| tree | 13714583d99546e125bf31d4347d08e8ea3838c1 /kernel | |
| parent | 9d52407e9fccf27d02d952d40f3758dfe1898767 (diff) | |
[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.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/nativelib.ml | 11 | ||||
| -rw-r--r-- | kernel/nativelib.mli | 1 |
2 files changed, 9 insertions, 3 deletions
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 |