diff options
| -rw-r--r-- | kernel/nativelib.ml | 11 | ||||
| -rw-r--r-- | kernel/nativelib.mli | 1 | ||||
| -rw-r--r-- | toplevel/coqargs.ml | 6 | ||||
| -rw-r--r-- | toplevel/coqargs.mli | 1 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 1 | ||||
| -rw-r--r-- | toplevel/usage.ml | 1 |
6 files changed, 18 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 diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 94d0831244..949a13974c 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -56,6 +56,7 @@ type coqargs_config = { 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; @@ -123,6 +124,7 @@ let default_config = { 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; @@ -493,6 +495,10 @@ let parse_args ~help ~init arglist : t * string list = 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 f0d7851c9d..aba6811f43 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -32,6 +32,7 @@ type coqargs_config = { 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 2509e3b68b..1ea48ee766 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -241,6 +241,7 @@ let init_execution opts custom_init = (* 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 4c622c6e28..c7e1d607f4 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -95,6 +95,7 @@ let print_usage_common co command = \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" |