diff options
| -rw-r--r-- | config/coq_config.mli | 3 | ||||
| -rw-r--r-- | configure.ml | 35 | ||||
| -rw-r--r-- | toplevel/coqargs.ml | 10 | ||||
| -rw-r--r-- | toplevel/coqargs.mli | 3 |
4 files changed, 36 insertions, 15 deletions
diff --git a/config/coq_config.mli b/config/coq_config.mli index 12856cb6e6..809fa3d758 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -57,4 +57,5 @@ val wwwstdlib : string val localwwwrefman : string val bytecode_compiler : bool -val native_compiler : bool +type native_compiler = NativeOff | NativeOn of { ondemand : bool } +val native_compiler : native_compiler diff --git a/configure.ml b/configure.ml index 6a4b1f9a75..e32f780a3d 100644 --- a/configure.ml +++ b/configure.ml @@ -225,6 +225,8 @@ let short_date, full_date = get_date () type ide = Opt | Byte | No +type nativecompiler = NativeYes | NativeNo | NativeOndemand + type preferences = { prefix : string option; local : bool; @@ -252,7 +254,7 @@ type preferences = { bin_annot : bool; annot : bool; bytecodecompiler : bool; - nativecompiler : bool; + nativecompiler : nativecompiler; coqwebsite : string; force_caml_version : bool; force_findlib_version : bool; @@ -288,7 +290,8 @@ let default = { bin_annot = false; annot = false; bytecodecompiler = true; - nativecompiler = not (os_type_win32 || os_type_cygwin); + nativecompiler = + if os_type_win32 || os_type_cygwin then NativeNo else NativeOndemand; coqwebsite = "http://coq.inria.fr/"; force_caml_version = false; force_findlib_version = false; @@ -332,6 +335,12 @@ let get_ide = function | "no" -> No | s -> raise (Arg.Bad ("(opt|byte|no) argument expected instead of "^s)) +let get_native = function + | "yes" -> NativeYes + | "no" -> NativeNo + | "ondemand" -> NativeOndemand + | s -> raise (Arg.Bad ("(yes|no|ondemand) argument expected instead of "^s)) + let arg_bool f = Arg.String (fun s -> prefs := f !prefs (get_bool s)) let arg_string f = Arg.String (fun s -> prefs := f !prefs s) @@ -346,6 +355,8 @@ let arg_clear_option f = Arg.Unit (fun () -> prefs := f !prefs (Some false)) let arg_ide f = Arg.String (fun s -> prefs := f !prefs (Some (get_ide s))) +let arg_native f = Arg.String (fun s -> prefs := f !prefs (get_native s)) + let arg_profile = Arg.String (fun s -> prefs := Profiles.get s !prefs) (* TODO : earlier any option -foo was also available as --foo *) @@ -407,8 +418,11 @@ let args_options = Arg.align [ " Dumps ml binary annotation files while compiling Coq (e.g. for Merlin)"; "-bytecode-compiler", arg_bool (fun p bytecodecompiler -> { p with bytecodecompiler }), "(yes|no) Enable Coq's bytecode reduction machine (VM)"; - "-native-compiler", arg_bool (fun p nativecompiler -> { p with nativecompiler }), - "(yes|no) Compilation to native code for conversion and normalization"; + "-native-compiler", arg_native (fun p nativecompiler -> { p with nativecompiler }), + "(yes|no|ondemand) Compilation to native code for conversion and normalization + yes: -native-compiler option of coqc will default to 'yes', stdlib will be precompiled + no: no native compilation available at all + ondemand (default): -native-compiler option of coqc will default to 'ondemand', stdlib will not be precompiled"; "-coqwebsite", arg_string (fun p coqwebsite -> { p with coqwebsite }), " URL of the coq website"; "-force-caml-version", arg_set (fun p force_caml_version -> { p with force_caml_version }), @@ -991,6 +1005,9 @@ let esc s = if String.contains s ' ' then "\"" ^ s ^ "\"" else s (** * Summary of the configuration *) +let pr_native = function + | NativeYes -> "yes" | NativeNo -> "no" | NativeOndemand -> "ondemand" + let print_summary () = let pr s = printf s in pr "\n"; @@ -1016,7 +1033,7 @@ let print_summary () = pr " Web browser : %s\n" browser; pr " Coq web site : %s\n" !prefs.coqwebsite; pr " Bytecode VM enabled : %B\n" !prefs.bytecodecompiler; - pr " Native Compiler enabled : %B\n\n" !prefs.nativecompiler; + pr " Native Compiler enabled : %s\n\n" (pr_native !prefs.nativecompiler); if !prefs.local then pr " Local build, no installation...\n" else @@ -1095,7 +1112,11 @@ let write_configml f = pr_s "wwwstdlib" (!prefs.coqwebsite ^ "distrib/V" ^ coq_version ^ "/stdlib/"); pr_s "localwwwrefman" ("file:/" ^ docdir ^ "/html/refman"); pr_b "bytecode_compiler" !prefs.bytecodecompiler; - pr_b "native_compiler" !prefs.nativecompiler; + pr "type native_compiler = NativeOff | NativeOn of { ondemand : bool }\n"; + pr "let native_compiler = %s\n" + (match !prefs.nativecompiler with + | NativeYes -> "NativeOn {ondemand=false}" | NativeNo -> "NativeOff" + | NativeOndemand -> "NativeOn {ondemand=true}"); let core_src_dirs = [ "config"; "lib"; "clib"; "kernel"; "library"; "engine"; "pretyping"; "interp"; "gramlib"; "gramlib/.pack"; "parsing"; "proofs"; @@ -1217,7 +1238,7 @@ let write_makefile f = pr "# Option to control compilation and installation of the documentation\n"; pr "WITHDOC=%s\n\n" (if !prefs.withdoc then "all" else "no"); pr "# Option to produce precompiled files for native_compute\n"; - pr "NATIVECOMPUTE=%s\n" (if !prefs.nativecompiler then "-native-compiler yes" else ""); + pr "NATIVECOMPUTE=%s\n" (if !prefs.nativecompiler = NativeYes then "-native-compiler yes" else ""); pr "COQWARNERROR=%s\n" (if !prefs.warn_error then "-w +default" else ""); close_out o; Unix.chmod f 0o444 diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index c6ccf2a427..ec339c69c6 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -36,7 +36,8 @@ let set_type_in_type () = type color = [`ON | `AUTO | `EMACS | `OFF] -type native_compiler = NativeOff | NativeOn of { ondemand : bool } +type native_compiler = Coq_config.native_compiler = + NativeOff | NativeOn of { ondemand : bool } type coqargs_logic_config = { impredicative_set : Declarations.set_predicativity; @@ -96,10 +97,7 @@ type t = { let default_toplevel = Names.(DirPath.make [Id.of_string "Top"]) -let default_native = - if Coq_config.native_compiler - then NativeOn {ondemand=true} - else NativeOff +let default_native = Coq_config.native_compiler let default_logic_config = { impredicative_set = Declarations.PredicativeSet; @@ -301,7 +299,7 @@ let get_native_compiler s = | ("no" | "off") -> NativeOff | _ -> error_wrong_arg ("Error: (yes|no|ondemand) expected after option -native-compiler") in - if not Coq_config.native_compiler && n <> NativeOff then + if Coq_config.native_compiler = NativeOff && n <> NativeOff then let () = warn_no_native_compiler s in NativeOff else diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index c8634b7847..f6222e4ec4 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -12,7 +12,8 @@ type color = [`ON | `AUTO | `EMACS | `OFF] val default_toplevel : Names.DirPath.t -type native_compiler = NativeOff | NativeOn of { ondemand : bool } +type native_compiler = Coq_config.native_compiler = + NativeOff | NativeOn of { ondemand : bool } type coqargs_logic_config = { impredicative_set : Declarations.set_predicativity; |