diff options
| author | Gaëtan Gilbert | 2021-02-04 12:14:32 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2021-02-04 12:21:12 +0100 |
| commit | 74aabc032014b0b83f2d54996dbb76cb5a78ea4d (patch) | |
| tree | 639390a8829b8a3a91ec6361e049db1ad69f46db /sysinit/coqargs.ml | |
| parent | 4b7feb4e022eab13ead7468687a53bc5afae0f8f (diff) | |
Properly handle ordering of -w and -native-compiler
Warnings are handled as injection commands, interleaved with options
and requires. Native compiler impacts require, so we must convert
"yes" to "no" before handling injections. As such the semantic
handling of the native command line argument must be separated from
the emission of the warning message, which this PR implements.
Fix #13819
In principle the other 2 cwarning in coqargs
(deprecated spropcumul and inputstate) should be moved to injections
too, but since they're deprecated I can't be bothered.
Diffstat (limited to 'sysinit/coqargs.ml')
| -rw-r--r-- | sysinit/coqargs.ml | 18 |
1 files changed, 6 insertions, 12 deletions
diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml index c4f12f6bb7..1738d56a54 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; @@ -255,12 +256,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 +269,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 *) @@ -385,8 +378,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 |