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 /toplevel | |
| 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 'toplevel')
| -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 |
4 files changed, 9 insertions, 0 deletions
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" |