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 ++++++------------
 1 file changed, 6 insertions(+), 12 deletions(-)

(limited to 'sysinit/coqargs.ml')

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
-- 
cgit v1.2.3