Merge branch 'warnings' into trunk

Was PR#213: New warnings machinery

6 files changed, 34 insertions, 15 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index a0ef5e570..8cbc3ab44 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 a0ff9e123..2f985e15a 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 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 =
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 30a346c91..710bfa19b 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 1b5e5e32a..389644692 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 53db6f5be..c729a6ce2 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