From 8e07227c5853de78eaed4577eefe908fb84507c0 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
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
---
 library/library.ml | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

(limited to 'library/library.ml')

diff --git a/library/library.ml b/library/library.ml
index bc7723f48..cead90700 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -271,6 +271,12 @@ exception LibUnmappedDir
 exception LibNotFound
 type library_location = LibLoaded | LibInPath
 
+let warn_several_object_files =
+  CWarnings.create ~name:"several-object-files" ~category:"require"
+         (fun (vi, vo) -> str"Loading" ++ spc () ++ str vi ++
+                            strbrk " instead of " ++ str vo ++
+                            strbrk " because it is more recent")
+
 let locate_absolute_library dir =
   (* Search in loadpath *)
   let pref, base = split_dirpath dir in
@@ -287,9 +293,8 @@ let locate_absolute_library dir =
   | [] -> raise LibNotFound
   | [file] -> file
   | [vo;vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
-       Feedback.msg_warning (str"Loading " ++ str vi ++ str " instead of " ++
-         str vo ++ str " because it is more recent");
-       vi
+    warn_several_object_files (vi, vo);
+    vi
   | [vo;vi] -> vo
   | _ -> assert false
 
@@ -311,8 +316,7 @@ let locate_qualified_library ?root ?(warn = true) qid =
     | [lpath, file] -> lpath, file
     | [lpath_vo, vo; lpath_vi, vi]
       when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
-       Feedback.msg_warning (str"Loading " ++ str vi ++ str " instead of " ++
-         str vo ++ str " because it is more recent");
+      warn_several_object_files (vi, vo);
        lpath_vi, vi
     | [lpath_vo, vo; _ ] -> lpath_vo, vo
     | _ -> assert false
@@ -753,7 +757,7 @@ let save_library_to ?todo dir f otab =
 	error "Could not compile the library to native code."
    with reraise ->
     let reraise = Errors.push reraise in
-    let () = Feedback.msg_warning (str "Removed file " ++ str f') in
+    let () = Feedback.msg_notice (str "Removed file " ++ str f') in
     let () = close_out ch in
     let () = Sys.remove f' in
     iraise reraise
-- 
cgit v1.2.3