A new infrastructure for warnings.

On the user side, coqtop and coqc take a list of warning names or categories
after -w. No prefix means activate the warning, a "-" prefix means deactivate
it, and "+" means turn the warning into an error. Special categories include
"all", and "default" which contains the warnings enabled by default.

We also provide a vernacular Set Warnings which takes the same flags as argument.

Note that coqc now prints warnings.

The name and category of a warning are printed with the warning itself.

On the developer side, Feedback.msg_warning is still accessible, but the
recommended way to print a warning is in two steps:

1) create it by:

let warn_my_warning =
  CWarnings.create ~name:"my-warning" ~category:"my-category"
    (fun args -> Pp.strbrk ...)

2) print it by:

warn_my_warning args

1 files changed, 13 insertions, 7 deletions

diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 5b92e9554..d4a67b399 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -55,6 +55,15 @@ let write_ml_code fn ?(header=[]) code =
   List.iter (pp_global fmt) (header@code);
   close_out ch_out
 
+let warn_native_compiler_failed =
+  let print = function
+  | Inl (Unix.WEXITED n) -> Pp.(strbrk "Native compiler exited with status" ++ str" " ++ int n)
+  | Inl (Unix.WSIGNALED n) -> Pp.(strbrk "Native compiler killed by signal" ++ str" " ++ int n)
+  | Inl (Unix.WSTOPPED n) -> Pp.(strbrk "Native compiler stopped by signal" ++ str" " ++ int n)
+  | Inr e -> Pp.(strbrk "Native compiler failed with error: " ++ strbrk (Unix.error_message e))
+  in
+  CWarnings.create ~name:"native-compiler-failed" ~category:"native-compiler" print
+
 let call_compiler ml_filename =
   let load_path = !get_load_paths () in
   let load_path = List.map (fun dn -> dn / output_dir) load_path in
@@ -78,15 +87,12 @@ let call_compiler ml_filename =
     let res = CUnix.sys_command (ocamlfind ()) args in
     let res = match res with
       | Unix.WEXITED 0 -> true
-      | Unix.WEXITED n ->
-         Feedback.msg_warning Pp.(str "command exited with status " ++ int n); false
-      | Unix.WSIGNALED n ->
-         Feedback.msg_warning Pp.(str "command killed by signal " ++ int n); false
-      | Unix.WSTOPPED n ->
-         Feedback.msg_warning Pp.(str "command stopped by signal " ++ int n); false in
+      | Unix.WEXITED n | Unix.WSIGNALED n | Unix.WSTOPPED n ->
+        warn_native_compiler_failed (Inl res); false
+    in
     res, link_filename
   with Unix.Unix_error (e,_,_) ->
-    Feedback.msg_warning Pp.(str (Unix.error_message e));
+    warn_native_compiler_failed (Inr e);
     false, link_filename
 
 let compile fn code =