diff options
| -rw-r--r-- | kernel/nativelib.ml | 8 | ||||
| -rw-r--r-- | kernel/nativelib.mli | 2 | ||||
| -rw-r--r-- | toplevel/coqargs.ml | 12 | ||||
| -rw-r--r-- | toplevel/coqargs.mli | 1 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 3 | ||||
| -rw-r--r-- | toplevel/usage.ml | 1 |
6 files changed, 20 insertions, 7 deletions
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 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 <directory> set the output directory for native objects\ \n -h, -help, --help print this list of options\ \n" |