From 8e07227c5853de78eaed4577eefe908fb84507c0 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 28 Jun 2016 10:55:30 +0200
Subject: 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
---
 kernel/cbytegen.ml   |  3 ++-
 kernel/nativeconv.ml |  9 +++++++--
 kernel/nativelib.ml  | 20 +++++++++++++-------
 kernel/reduction.ml  |  8 +++++++-
 kernel/reduction.mli |  2 ++
 kernel/vconv.ml      |  7 +++----
 6 files changed, 34 insertions(+), 15 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index a0ef5e570e..8cbc3ab445 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -907,7 +907,8 @@ let compile fail_on_error ?universes:(universes=0) env c =
       Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
     Some (init_code,!fun_code, Array.of_list fv)
   with TooLargeInductive tname ->
-    let fn = if fail_on_error then Errors.errorlabstrm "compile" else Feedback.msg_warning ?loc:None in
+    let fn = if fail_on_error then Errors.errorlabstrm "compile" else
+	       (fun x -> Feedback.msg_warning x) in
       (Pp.(fn
 	   (str "Cannot compile code for virtual machine as it uses inductive " ++
 	    Id.print tname ++ str str_max_constructors));
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index a0ff9e123a..2f985e15ac 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -145,11 +145,16 @@ let native_conv_gen pb sigma env univs t1 t2 =
       end
   | _ -> anomaly (Pp.str "Compilation failure") 
 
+let warn_no_native_compiler =
+  let open Pp in
+  CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler"
+         (fun () -> strbrk "Native compiler is disabled," ++
+                      strbrk " falling back to VM conversion test.")
+
 (* Wrapper for [native_conv] above *)
 let native_conv cv_pb sigma env t1 t2 =
   if Coq_config.no_native_compiler then begin
-    let msg = "Native compiler is disabled, falling back to VM conversion test." in
-    Feedback.msg_warning (Pp.str msg);
+    warn_no_native_compiler ();
     vm_conv cv_pb env t1 t2
   end
   else
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 5b92e9554f..d4a67b3999 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 =
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 30a346c910..710bfa19b8 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -676,12 +676,18 @@ let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_sta
 let vm_conv = ref (fun cv_pb env ->
 		   gen_conv cv_pb env ~evars:((fun _->None), universes env))
 
+let warn_bytecode_compiler_failed =
+  let open Pp in
+  CWarnings.create ~name:"bytecode-compiler-failed" ~category:"bytecode-compiler"
+         (fun () -> strbrk "Bytecode compiler failed, " ++
+                      strbrk "falling back to standard conversion")
+
 let set_vm_conv (f:conv_pb -> Term.types kernel_conversion_function) = vm_conv := f
 let vm_conv cv_pb env t1 t2 =
   try
     !vm_conv cv_pb env t1 t2
   with Not_found | Invalid_argument _ ->
-    Feedback.msg_warning (Pp.str "Bytecode compilation failed, falling back to standard conversion");
+    warn_bytecode_compiler_failed ();
     gen_conv cv_pb env t1 t2
 
 let default_conv cv_pb ?(l2r=false) env t1 t2 =
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 1b5e5e32a3..3896446925 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -106,3 +106,5 @@ exception NotArity
 
 val dest_arity : env -> types -> arity (* raises NotArity if not an arity *)
 val is_arity   : env -> types -> bool
+
+val warn_bytecode_compiler_failed : ?loc:Loc.t -> unit -> unit
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 53db6f5bee..c729a6ce29 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -185,10 +185,9 @@ let vm_conv_gen cv_pb env univs t1 t2 =
     let v2 = val_of_constr env t2 in
     fst (conv_val env cv_pb (nb_rel env) v1 v2 univs)
   with Not_found | Invalid_argument _ ->
-    (Feedback.msg_warning
-      (Pp.str "Bytecode compilation failed, falling back to default conversion");
-     Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
-			    full_transparent_state env univs t1 t2)
+    warn_bytecode_compiler_failed ();
+    Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
+      full_transparent_state env univs t1 t2
 
 let vm_conv cv_pb env t1 t2 =
   let univs = Environ.universes env in
-- 
cgit v1.2.3