diff options
Diffstat (limited to 'sysinit')
| -rw-r--r-- | sysinit/coqargs.ml | 39 | ||||
| -rw-r--r-- | sysinit/coqargs.mli | 9 | ||||
| -rw-r--r-- | sysinit/coqinit.ml | 14 | ||||
| -rw-r--r-- | sysinit/usage.ml | 1 |
4 files changed, 22 insertions, 41 deletions
diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml index c4f12f6bb7..56d88e6bd6 100644 --- a/sysinit/coqargs.ml +++ b/sysinit/coqargs.ml @@ -44,6 +44,7 @@ type option_command = type injection_command = | OptionInjection of (Goptions.option_name * option_command) | RequireInjection of (string * string option * bool option) + | WarnNoNative of string type coqargs_logic_config = { impredicative_set : Declarations.set_predicativity; @@ -75,8 +76,6 @@ type coqargs_pre = { load_vernacular_list : (string * bool) list; injections : injection_command list; - - inputstate : string option; } type coqargs_query = @@ -133,7 +132,6 @@ let default_pre = { vo_includes = []; load_vernacular_list = []; injections = []; - inputstate = None; } let default_queries = [] @@ -184,18 +182,6 @@ let set_query opts q = | Queries queries -> Queries (queries@[q]) } -let warn_deprecated_sprop_cumul = - CWarnings.create ~name:"deprecated-spropcumul" ~category:"deprecated" - (fun () -> Pp.strbrk "Use the \"Cumulative StrictProp\" flag instead.") - -let warn_deprecated_inputstate = - CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" - (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.") - -let set_inputstate opts s = - warn_deprecated_inputstate (); - { opts with pre = { opts.pre with inputstate = Some s }} - (******************************************************************************) (* Parsing helpers *) (******************************************************************************) @@ -255,12 +241,6 @@ let parse_option_set opt = let v = String.sub opt (eqi+1) (len - eqi - 1) in to_opt_key (String.sub opt 0 eqi), Some v -let warn_no_native_compiler = - CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler" - Pp.(fun s -> strbrk "Native compiler is disabled," ++ - strbrk " -native-compiler " ++ strbrk s ++ - strbrk " option ignored.") - let get_native_compiler s = (* We use two boolean flags because the four states make sense, even if only three are accessible to the user at the moment. The selection of the @@ -274,10 +254,8 @@ let get_native_compiler s = | _ -> error_wrong_arg ("Error: (yes|no|ondemand) expected after option -native-compiler") in if Coq_config.native_compiler = NativeOff && n <> NativeOff then - let () = warn_no_native_compiler s in - NativeOff - else - n + NativeOff, Some (WarnNoNative s) + else n, None (* Main parsing routine *) (*s Parsing of the command line *) @@ -333,9 +311,6 @@ let parse_args ~usage ~init arglist : t * string list = |"-init-file" -> { oval with config = { oval.config with rcfile = Some (next ()); }} - |"-inputstate"|"-is" -> - set_inputstate oval (next ()) - |"-load-vernac-object" -> add_vo_require oval (next ()) None None @@ -385,8 +360,9 @@ let parse_args ~usage ~init arglist : t * string list = { oval with config = { oval.config with enable_VM = get_bool ~opt (next ()) }} |"-native-compiler" -> - let native_compiler = get_native_compiler (next ()) in - { oval with config = { oval.config with native_compiler }} + let native_compiler, warn = get_native_compiler (next ()) in + { oval with config = { oval.config with native_compiler }; + pre = { oval.pre with injections = Option.List.cons warn oval.pre.injections }} | "-set" -> let opt, v = parse_option_set @@ next() in @@ -419,9 +395,6 @@ let parse_args ~usage ~init arglist : t * string list = add_set_option oval Vernacentries.allow_sprop_opt_name (OptionSet None) |"-disallow-sprop" -> add_set_option oval Vernacentries.allow_sprop_opt_name OptionUnset - |"-sprop-cumulative" -> - warn_deprecated_sprop_cumul(); - add_set_option oval Vernacentries.cumul_sprop_opt_name (OptionSet None) |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval |"-m"|"--memory" -> { oval with post = { memory_stat = true }} |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }} diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli index aef50193f2..9725a849a4 100644 --- a/sysinit/coqargs.mli +++ b/sysinit/coqargs.mli @@ -28,7 +28,12 @@ type injection_command = ready. Parameters follow [Library], that is to say, [lib,prefix,import_export] means require library [lib] from optional [prefix] and [import_export] if [Some false/Some true] - is used. *) + is used. *) + | WarnNoNative of string + (** Used so that "-w -native-compiler-disabled -native-compiler yes" + does not cause a warning. The native option must be processed + before injections (because it affects require), so the + instruction to emit a message is separated. *) type coqargs_logic_config = { impredicative_set : Declarations.set_predicativity; @@ -60,8 +65,6 @@ type coqargs_pre = { load_vernacular_list : (string * bool) list; injections : injection_command list; - - inputstate : string option; } type coqargs_query = diff --git a/sysinit/coqinit.ml b/sysinit/coqinit.ml index 16c8389de5..25da2c5302 100644 --- a/sysinit/coqinit.ml +++ b/sysinit/coqinit.ml @@ -126,10 +126,16 @@ let require_file (dir, from, exp) = let mfrom = Option.map Libnames.qualid_of_string from in Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] -let handle_injection = function - | Coqargs.RequireInjection r -> require_file r - (* | LoadInjection l -> *) - | Coqargs.OptionInjection o -> Coqargs.set_option o +let warn_no_native_compiler = + CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler" + Pp.(fun s -> strbrk "Native compiler is disabled," ++ + strbrk " -native-compiler " ++ strbrk s ++ + strbrk " option ignored.") + +let handle_injection = let open Coqargs in function + | RequireInjection r -> require_file r + | OptionInjection o -> set_option o + | WarnNoNative s -> warn_no_native_compiler s let start_library ~top injections = Flags.verbosely Declaremods.start_library top; diff --git a/sysinit/usage.ml b/sysinit/usage.ml index 1831a3f9b2..763cd54137 100644 --- a/sysinit/usage.ml +++ b/sysinit/usage.ml @@ -79,7 +79,6 @@ let print_usage_common co command = \n -impredicative-set set sort Set impredicative\ \n -allow-sprop allow using the proof irrelevant SProp sort\ \n -disallow-sprop forbid using the proof irrelevant SProp sort\ -\n -sprop-cumulative make sort SProp cumulative with the rest of the hierarchy\ \n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\ \n -type-in-type disable universe consistency checking\ \n -mangle-names x mangle auto-generated names using prefix x\ |