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. --- toplevel/coqargs.ml | 12 ++++++++++-- toplevel/coqargs.mli | 1 + toplevel/coqtop.ml | 3 +++ toplevel/usage.ml | 1 + 4 files changed, 15 insertions(+), 2 deletions(-) (limited to 'toplevel') diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 2b79bff1b2..94d0831244 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -55,6 +55,7 @@ type coqargs_config = { color : color; enable_VM : bool; native_compiler : native_compiler; + native_output_dir : CUnix.physical_path; stm_flags : Stm.AsyncOpts.stm_opt; debug : bool; diffs_set : bool; @@ -121,6 +122,7 @@ let default_config = { color = `AUTO; enable_VM = true; native_compiler = default_native; + native_output_dir = ".coq-native"; stm_flags = Stm.AsyncOpts.default_opts; debug = false; diffs_set = false; @@ -261,8 +263,10 @@ let get_cache opt = function let get_native_name s = (* We ignore even critical errors because this mode has to be super silent *) try - String.concat "/" [Filename.dirname s; - Nativelib.output_dir; Library.native_name_from_filename s] + Filename.(List.fold_left concat (dirname s) + [ !Nativelib.output_dir + ; Library.native_name_from_filename s + ]) with _ -> "" let get_compat_file = function @@ -485,6 +489,10 @@ let parse_args ~help ~init arglist : t * string list = let opt = to_opt_key opt in { oval with config = { oval.config with set_options = (opt, OptionUnset) :: oval.config.set_options }} + |"-native-output-dir" -> + let native_output_dir = next () in + { oval with config = { oval.config with native_output_dir } } + (* Options with zero arg *) |"-async-queries-always-delegate" |"-async-proofs-always-delegate" diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index f38381a086..f0d7851c9d 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -31,6 +31,7 @@ type coqargs_config = { color : color; enable_VM : bool; native_compiler : native_compiler; + native_output_dir : CUnix.physical_path; stm_flags : Stm.AsyncOpts.stm_opt; debug : bool; diffs_set : bool; diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 46dd693155..2509e3b68b 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -239,6 +239,9 @@ let init_execution opts custom_init = set_options opts.config.set_options; + (* Native output dir *) + Nativelib.output_dir := opts.config.native_output_dir; + (* Allow the user to load an arbitrary state here *) inputstate opts.pre; diff --git a/toplevel/usage.ml b/toplevel/usage.ml index ba3deeb2f6..4c622c6e28 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -94,6 +94,7 @@ let print_usage_common co command = \n for full Gc stats dump)\ \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 set the output directory for native objects\ \n -h, -help, --help print this list of options\ \n" -- 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. --- toplevel/coqargs.ml | 6 ++++++ toplevel/coqargs.mli | 1 + toplevel/coqtop.ml | 1 + toplevel/usage.ml | 1 + 4 files changed, 9 insertions(+) (limited to 'toplevel') 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 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" -- cgit v1.2.3