From 74aabc032014b0b83f2d54996dbb76cb5a78ea4d Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 4 Feb 2021 12:14:32 +0100 Subject: 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. --- sysinit/coqargs.ml | 18 ++++++------------ sysinit/coqargs.mli | 7 ++++++- sysinit/coqinit.ml | 14 ++++++++++---- .../output/bug_13821_native_command_line_warn.out | 0 test-suite/output/bug_13821_native_command_line_warn.v | 1 + 5 files changed, 23 insertions(+), 17 deletions(-) create mode 100644 test-suite/output/bug_13821_native_command_line_warn.out create mode 100644 test-suite/output/bug_13821_native_command_line_warn.v 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 diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli index aef50193f2..ce0a0cdf16 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; 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/test-suite/output/bug_13821_native_command_line_warn.out b/test-suite/output/bug_13821_native_command_line_warn.out new file mode 100644 index 0000000000..e69de29bb2 diff --git a/test-suite/output/bug_13821_native_command_line_warn.v b/test-suite/output/bug_13821_native_command_line_warn.v new file mode 100644 index 0000000000..a28210b6c2 --- /dev/null +++ b/test-suite/output/bug_13821_native_command_line_warn.v @@ -0,0 +1 @@ +(* -*- coq-prog-args: ("-w" "-native-compiler-disabled" "-native-compiler" "ondemand"); -*- *) -- cgit v1.2.3