From 2c5eef988f11979175de6d1983bc533ce18b1095 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 2 Nov 2016 15:57:19 +0100
Subject: Fix various shortcomings of the warnings infrastructure.

- The flags are now interpreted from left to right, without any other
precedence rule. The previous one did not make much sense in interactive
mode.
- Set Warnings and Set Warnings Append are now synonyms, and have the
"append" semantics, which is the most natural one for warnings.
- Warnings on unknown warnings are now printed only once (previously the
would be repeated on further calls to Set Warnings, sections closing,
module requiring...).
- Warning status strings are normalized, so that e.g. "+foo,-foo" is reduced
to "-foo" (if foo exists, "" otherwise).
---
 lib/cWarnings.ml  | 116 +++++++++++++++++++++++++++++++++++++++++-------------
 lib/cWarnings.mli |  23 +++--------
 2 files changed, 94 insertions(+), 45 deletions(-)

(limited to 'lib')

diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index 720f54606c..68664d1ab2 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -21,7 +21,7 @@ let warnings : (string, t) Hashtbl.t = Hashtbl.create 97
 let categories : (string, string list) Hashtbl.t = Hashtbl.create 97
 
 let current_loc = ref Loc.ghost
-let flags = ref "default"
+let flags = ref ""
 
 let set_current_loc = (:=) current_loc
 
@@ -62,7 +62,7 @@ let set_warning_status ~name status =
   try
     let w = Hashtbl.find warnings name in 
     Hashtbl.replace warnings name { w with status = status }
-  with Not_found -> warn_unknown_warning name
+  with Not_found -> ()
 
 let reset_default_warnings () =
   Hashtbl.iter (fun name w ->
@@ -74,6 +74,13 @@ let set_all_warnings_status status =
                 Hashtbl.replace warnings name { w with status })
     warnings
 
+let set_category_status ~name status =
+  let names = Hashtbl.find categories name in
+  List.iter (fun name -> set_warning_status name status) names
+
+let is_all_keyword name = CString.equal name "all"
+let is_none_keyword s = CString.equal s "none"
+
 let parse_flag s =
   if String.length s > 1 then
     match String.get s 0 with
@@ -82,39 +89,94 @@ let parse_flag s =
     | _ -> (Enabled, s)
   else CErrors.error "Invalid warnings flag"
 
-let rec do_all_keyword = function
-  | [] -> []
-  | (status, name as item) :: items -> 
-     if CString.equal name "all" then
-       (set_all_warnings_status status; do_all_keyword items)
-     else item :: do_all_keyword items
-
-let rec do_categories = function
-  | [] -> []
-  | (status, name as item) :: items -> 
-     try
-       let names = Hashtbl.find categories name in
-       List.iter (fun name -> set_warning_status name status) names;
-       do_categories items
-     with Not_found -> item :: do_categories items
+let string_of_flag (status,name) =
+  match status with
+  | AsError -> "+" ^ name
+  | Disabled -> "-" ^ name
+  | Enabled -> name
+
+let string_of_flags flags =
+  String.concat "," (List.map string_of_flag flags)
+
+let set_status ~name status =
+  if is_all_keyword name then
+    set_all_warnings_status status
+  else
+    try
+      set_category_status ~name status
+    with Not_found ->
+         try
+           set_warning_status ~name status
+         with Not_found -> ()
+
+let split_flags s =
+  let reg = Str.regexp "[ ,]+" in Str.split reg s
+
+let check_warning ~silent (_status,name) =
+  is_all_keyword name ||
+  Hashtbl.mem categories name ||
+  Hashtbl.mem warnings name ||
+  (if not silent then warn_unknown_warning name; false)
+
+(** [cut_before_all_rev] removes all flags subsumed by a later occurrence of the
+    "all" flag, and reverses the list. *)
+let rec cut_before_all_rev acc = function
+  | [] -> acc
+  | (_status,name as w) :: warnings ->
+     cut_before_all_rev (w :: if is_all_keyword name then [] else acc) warnings
+
+let cut_before_all_rev warnings = cut_before_all_rev [] warnings
+
+(** [uniquize_flags_rev] removes flags that are subsumed by later occurrences of
+    themselves or their categories, and reverses the list. *)
+let uniquize_flags_rev flags =
+  let rec aux acc visited = function
+    | (_,name as flag)::flags ->
+       if CString.Set.mem name visited then aux acc visited flags else
+         let visited =
+           try
+             let warnings = Hashtbl.find categories name in
+             CString.Set.union visited (CString.Set.of_list warnings)
+           with Not_found ->
+             visited
+         in
+         aux (flag::acc) (CString.Set.add name visited) flags
+    | [] -> acc
+  in aux [] CString.Set.empty flags
+
+(** [normalize_flags] removes unknown or redundant warnings. If [silent] is
+    true, it emits a warning when an unknown warning is met. *)
+let normalize_flags ~silent warnings =
+  let warnings = List.filter (check_warning ~silent) warnings in
+  let warnings = cut_before_all_rev warnings in
+  uniquize_flags_rev warnings
+
+let flags_of_string s = List.map parse_flag (split_flags s)
+
+let normalize_flags_string s =
+  if is_none_keyword s then s
+  else
+    let flags = flags_of_string s in
+    let flags = normalize_flags ~silent:false flags in
+    string_of_flags flags
 
 let rec parse_warnings items =
-  List.iter (fun (status, name) -> set_warning_status ~name status) items
+  CList.iter (fun (status, name) -> set_status ~name status) items
 
 (* For compatibility, we accept "none" *)
-let parse_flags s = 
-  if CString.equal s "none" then begin
+let parse_flags s =
+  if is_none_keyword s then begin
       Flags.make_warn false;
-      set_all_warnings_status Disabled
+      set_all_warnings_status Disabled;
+      "none"
     end
   else begin
       Flags.make_warn true;
-      let reg = Str.regexp "[ ,]+" in
-      let items = List.map parse_flag (Str.split reg s) in
-      let items = do_all_keyword items in
-      let items = do_categories items in
-      parse_warnings items
+      let flags = flags_of_string s in
+      let flags = normalize_flags ~silent:true flags in
+      parse_warnings flags;
+      string_of_flags flags
     end
 
 let set_flags s =
-  flags := s; reset_default_warnings (); parse_flags s
+  reset_default_warnings (); let s = parse_flags s in flags := s
diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli
index 3515542840..3f6cee31b7 100644
--- a/lib/cWarnings.mli
+++ b/lib/cWarnings.mli
@@ -6,29 +6,16 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-type status =
-  Disabled | Enabled | AsError
-
-(*
-type 'a repr = {
-  print : 'a -> Pp.std_ppcmds;
-  kind : string;
-  enabled : bool;
-}
- *)
+type status = Disabled | Enabled | AsError
 
 val set_current_loc : Loc.t -> unit
 
 val create : name:string -> category:string -> ?default:status ->
              ('a -> Pp.std_ppcmds) -> ?loc:Loc.t -> 'a -> unit
 
-(*
-val emit : 'a t -> 'a -> unit
-
-type any = Any : string * string * 'a repr -> any
-
-val dump : unit -> any list
- *)
-
 val get_flags : unit -> string
 val set_flags : string -> unit
+
+(** Cleans up a user provided warnings status string, e.g. removing unknown
+    warnings (in which case a warning is emitted) or subsumed warnings . *)
+val normalize_flags_string : string -> string
-- 
cgit v1.2.3


From dd558cc1a9b87d2b1dda5d1ff2baf9f02a32e519 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 3 Nov 2016 18:20:36 +0100
Subject: Remove an OCaml 4.02 construct.

This was not detected by running coq-contribs, so it probably means that
we are not testing with the right version of OCaml.
---
 lib/cWarnings.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index 68664d1ab2..1a1944d61f 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -136,7 +136,7 @@ let uniquize_flags_rev flags =
          let visited =
            try
              let warnings = Hashtbl.find categories name in
-             CString.Set.union visited (CString.Set.of_list warnings)
+             List.fold_left (fun v w -> CString.Set.add w v) visited warnings
            with Not_found ->
              visited
          in
-- 
cgit v1.2.3


From 1d637f15de540c82289d6b3a16181a625a0d9cdf Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 4 Nov 2016 13:28:08 +0100
Subject: Fix #4837: ./configure -local makes coqdep issue many warnings

We simply remove the warnings about paths mixing Win32 and Unix
separators, since that situation does not seem problematic (c.f.
discussion on the bug tracker).
---
 lib/minisys.ml | 8 --------
 lib/system.ml  | 1 -
 lib/system.mli | 5 -----
 3 files changed, 14 deletions(-)

(limited to 'lib')

diff --git a/lib/minisys.ml b/lib/minisys.ml
index 25e4d79c4e..f15021c655 100644
--- a/lib/minisys.ml
+++ b/lib/minisys.ml
@@ -46,14 +46,6 @@ let ok_dirname f =
 let exists_dir dir =
   try Sys.is_directory dir with Sys_error _ -> false
 
-let check_unix_dir warn dir =
-  if (Sys.os_type = "Win32" || Sys.os_type = "Cygwin") &&
-    (String.length dir > 2 && dir.[1] = ':' ||
-     String.contains dir '\\' ||
-     String.contains dir ';')
-  then warn ("assuming " ^ dir ^
-             " to be a Unix path even if looking like a Win32 path.")
-
 let apply_subdir f path name =
   (* we avoid all files and subdirs starting by '.' (e.g. .svn) *)
   (* as well as skipped files like CVS, ... *)
diff --git a/lib/system.ml b/lib/system.ml
index af9aa5c074..4b99de707b 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -33,7 +33,6 @@ let all_subdirs ~unix_path:root =
       | _ -> ()
     in process_directory f path
   in
-  check_unix_dir (fun s -> Feedback.msg_warning (str s)) root;
   if exists_dir root then traverse root []
   else warn_cannot_open_dir root;
   List.rev !l
diff --git a/lib/system.mli b/lib/system.mli
index 4dbb3695d2..214369095c 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -20,11 +20,6 @@ val (//) : unix_path -> string -> unix_path
 
 val exists_dir : unix_path -> bool
 
-(** [check_unix_dir warn path] calls [warn] with an appropriate
-     message if [path] looks does not look like a Unix path on Windows *)
-
-val check_unix_dir : (string -> unit) -> unix_path -> unit
-
 (** [exclude_search_in_dirname path] excludes [path] when processing
     directories *)
 
-- 
cgit v1.2.3


From ed2ec9362c0c0010b9caaaba4dcc771878ee2b7c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 5 Nov 2016 12:09:14 +0100
Subject: Removing a special treatment for empty lines in comments.

This made the whole pp code complicated only for the purpose of the
beautifier, while it is not clear when this was useful.

Removing the code for simplicity, not excluding to later address
beautifier issues when they show up.
---
 lib/pp.ml | 51 ++++++++++++---------------------------------------
 1 file changed, 12 insertions(+), 39 deletions(-)

(limited to 'lib')

diff --git a/lib/pp.ml b/lib/pp.ml
index 5520498026..f3bb475392 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -243,32 +243,15 @@ let qstring s = str "\"" ++ str (escape_string s) ++ str "\""
 let qs = qstring
 let quote s = h 0 (str "\"" ++ s ++ str "\"")
 
-(* This flag tells if the last printed comment ends with a newline, to
-  avoid empty lines *)
-let com_eol = ref false
-
-let com_brk ft = com_eol := false
-let com_if ft f =
-  if !com_eol then (com_eol := false; Format.pp_force_newline ft ())
-  else Lazy.force f
-
 let rec pr_com ft s =
   let (s1,os) =
     try
       let n = String.index s '\n' in
       String.sub s 0 n, Some (String.sub s (n+1) (String.length s - n - 1))
     with Not_found -> s,None in
-  com_if ft (Lazy.from_val());
-(*  let s1 =
-    if String.length s1 <> 0 && s1.[0] = ' ' then
-      (Format.pp_print_space ft (); String.sub s1 1 (String.length s1 - 1))
-    else s1 in*)
   Format.pp_print_as ft (utf8_length s1) s1;
   match os with
-      Some s2 ->
-        if Int.equal (String.length s2) 0 then (com_eol := true)
-        else
-          (Format.pp_force_newline ft (); pr_com ft s2)
+      Some s2 -> Format.pp_force_newline ft (); pr_com ft s2
     | None -> ()
 
 type tag_handler = Tag.t -> Format.tag
@@ -287,33 +270,24 @@ let pp_dirs ?pp_tag ft =
         begin match tok with
         | Str_def s ->
           let n = utf8_length s in
-          com_if ft (Lazy.from_val()); Format.pp_print_as ft n s
+          Format.pp_print_as ft n s
         | Str_len (s, n) ->
-          com_if ft (Lazy.from_val()); Format.pp_print_as ft n s
+          Format.pp_print_as ft n s
         end
     | Ppcmd_box(bty,ss)       -> (* Prevent evaluation of the stream! *)
-        com_if ft (Lazy.from_val());
         pp_open_box bty ;
         if not (Format.over_max_boxes ()) then Glue.iter pp_cmd ss;
         Format.pp_close_box ft ()
-    | Ppcmd_open_box bty      -> com_if ft (Lazy.from_val()); pp_open_box bty
+    | Ppcmd_open_box bty      -> pp_open_box bty
     | Ppcmd_close_box         -> Format.pp_close_box ft ()
     | Ppcmd_close_tbox        -> Format.pp_close_tbox ft ()
-    | Ppcmd_white_space n     ->
-        com_if ft (Lazy.from_fun (fun()->Format.pp_print_break ft n 0))
-    | Ppcmd_print_break(m,n)  ->
-        com_if ft (Lazy.from_fun(fun()->Format.pp_print_break ft m n))
+    | Ppcmd_white_space n     -> Format.pp_print_break ft n 0
+    | Ppcmd_print_break(m,n)  -> Format.pp_print_break ft m n
     | Ppcmd_set_tab           -> Format.pp_set_tab ft ()
-    | Ppcmd_print_tbreak(m,n) ->
-        com_if ft (Lazy.from_fun(fun()->Format.pp_print_tbreak ft m n))
-    | Ppcmd_force_newline     ->
-        com_brk ft; Format.pp_force_newline ft ()
-    | Ppcmd_print_if_broken   ->
-        com_if ft (Lazy.from_fun(fun()->Format.pp_print_if_newline ft ()))
-    | Ppcmd_comment coms      ->
-(*        Format.pp_open_hvbox ft 0;*)
-        List.iter (pr_com ft) coms(*;
-        Format.pp_close_box ft ()*)
+    | Ppcmd_print_tbreak(m,n) -> Format.pp_print_tbreak ft m n
+    | Ppcmd_force_newline     -> Format.pp_force_newline ft ()
+    | Ppcmd_print_if_broken   -> Format.pp_print_if_newline ft ()
+    | Ppcmd_comment coms      -> List.iter (pr_com ft) coms
     | Ppcmd_open_tag tag ->
       begin match pp_tag with
       | None -> ()
@@ -327,13 +301,12 @@ let pp_dirs ?pp_tag ft =
   in
   let pp_dir = function
     | Ppdir_ppcmds cmdstream -> Glue.iter pp_cmd cmdstream
-    | Ppdir_print_newline    ->
-        com_brk ft; Format.pp_print_newline ft ()
+    | Ppdir_print_newline    -> Format.pp_print_newline ft ()
     | Ppdir_print_flush      -> Format.pp_print_flush ft ()
   in
   fun (dirstream : _ ppdirs) ->
     try
-      Glue.iter pp_dir dirstream; com_brk ft
+      Glue.iter pp_dir dirstream
     with reraise ->
       let reraise = Backtrace.add_backtrace reraise in
       let () = Format.pp_print_flush ft () in
-- 
cgit v1.2.3


From 8fe6da32544ee73201f7c64b3dd45afb56c75b71 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 10 Nov 2016 13:24:54 +0100
Subject: Fix bug in warnings: -w foo was silent when foo did not exist.

---
 lib/cWarnings.ml | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

(limited to 'lib')

diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index 1a1944d61f..cc2463e224 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -35,6 +35,10 @@ let add_warning_in_category ~name ~category =
   in
   Hashtbl.replace categories category (name::ws)
 
+let refine_loc = function
+  | None when not (Loc.is_ghost !current_loc) -> Some !current_loc
+  | loc -> loc
+
 let create ~name ~category ?(default=Enabled) pp =
   Hashtbl.add warnings name { default; category; status = default };
   add_warning_in_category ~name ~category;
@@ -44,15 +48,17 @@ let create ~name ~category ?(default=Enabled) pp =
            match w.status with
            | Disabled -> ()
            | AsError ->
-              let loc = Option.default !current_loc loc in
-              CErrors.user_err_loc (loc,"_",pp x)
+              begin match refine_loc loc with
+              | Some loc -> CErrors.user_err_loc (loc,"_",pp x)
+              | None -> CErrors.errorlabstrm "_" (pp x)
+              end
            | Enabled ->
               let msg =
                 pp x ++ spc () ++ str "[" ++ str name ++ str "," ++
                   str category ++ str "]"
               in
-              let loc = Option.default !current_loc loc in
-              Feedback.msg_warning ~loc msg
+              let loc = refine_loc loc in
+              Feedback.msg_warning ?loc msg
 
 let warn_unknown_warning =
   create ~name:"unknown-warning" ~category:"toplevel"
-- 
cgit v1.2.3