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.

1 files changed, 10 insertions, 4 deletions

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;