Infrastructure for fine-grained debug flags

6 files changed, 144 insertions, 3 deletions

diff --git a/lib/cDebug.ml b/lib/cDebug.ml
new file mode 100644
index 0000000000..efa7365b91
--- /dev/null
+++ b/lib/cDebug.ml
@@ -0,0 +1,92 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+type flag = bool ref
+
+type t = (unit -> Pp.t) -> unit
+
+let debug = ref CString.Map.empty
+
+(* Used to remember level of Set Debug "all" for debugs created by
+   plugins dynlinked after the Set *)
+let all_flag = ref false
+
+let set_debug_backtrace b =
+  Exninfo.record_backtrace b
+
+let set_debug_all b =
+  set_debug_backtrace b;
+  CString.Map.iter (fun _ flag -> flag := b) !debug;
+  all_flag := b
+
+let create_full ~name () =
+  let anomaly pp = CErrors.anomaly ~label:"CDebug.create" pp in
+  let () = match name with
+    | "all"|"backtrace" -> anomaly Pp.(str"The debug name \""++str name++str"\" is reserved.")
+    | _ ->
+      if CString.Map.mem name !debug then
+        anomaly Pp.(str "The debug name \"" ++ str name ++ str "\" is already used.")
+  in
+  let pp x =
+    Feedback.msg_debug Pp.(str "[" ++ str name ++ str "] " ++ x)
+  in
+  let flag = ref !all_flag in
+  debug := CString.Map.add name flag !debug;
+  let pp x =
+    if !flag
+    then pp (x ())
+  in
+  flag, pp
+
+let create ~name () =
+  snd (create_full ~name ())
+
+let get_flag flag = !flag
+
+let warn_unknown_debug = CWarnings.create ~name:"unknown-debug-flag" ~category:"option"
+    Pp.(fun name -> str "There is no debug flag \"" ++ str name ++ str "\".")
+
+let get_flags () =
+  let pp_flag name flag = if flag then name else "-"^name in
+  let flags =
+    CString.Map.fold
+      (fun name v acc -> pp_flag name !v :: acc)
+      !debug []
+  in
+  let all = pp_flag "all" !all_flag in
+  let bt = pp_flag "backtrace" (Printexc.backtrace_status()) in
+  String.concat "," (all::bt::flags)
+
+exception Error
+
+let parse_flags s =
+  let parse_flag s =
+    if CString.is_empty s then raise Error
+    else if s.[0] = '-'
+    then String.sub s 1 (String.length s - 1), false
+    else s, true
+  in
+  try
+    Some (CList.map parse_flag @@ String.split_on_char ',' s)
+  with Error -> None
+
+let set_flags s = match parse_flags s with
+  | None -> CErrors.user_err Pp.(str "Syntax error in debug flags.")
+  | Some flags ->
+    let set_one_flag (name,b) = match name with
+      | "all" -> set_debug_all b
+      | "backtrace" -> set_debug_backtrace b
+      | _ -> match CString.Map.find_opt name !debug with
+        | None -> warn_unknown_debug name
+        | Some flag -> flag := b
+    in
+    List.iter set_one_flag flags
+
+let misc, pp_misc = create_full ~name:"misc" ()
diff --git a/lib/cDebug.mli b/lib/cDebug.mli
new file mode 100644
index 0000000000..846c4b493b
--- /dev/null
+++ b/lib/cDebug.mli
@@ -0,0 +1,50 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+type flag
+
+type t = (unit -> Pp.t) -> unit
+
+(** Creates a debug component, which may be used to print debug
+    messages.
+
+    A debug component is named by the string [name]. It is either
+    active or inactive.
+
+    The special component ["all"] may be used to control all components.
+
+    There is also a special component ["backtrace"] to control
+    backtrace recording.
+*)
+val create : name:string -> unit -> t
+
+(** Useful when interacting with a component from code, typically when
+    doing something more complicated than printing.
+
+    Note that the printer function prints some metadata compared to
+    [ fun pp -> if get_flag flag then Feedback.msg_debug (pp ()) ]
+ *)
+val create_full : name:string -> unit -> flag * t
+
+val get_flag : flag -> bool
+
+(** [get_flags] and [set_flags] use the user syntax: a comma separated
+    list of activated "component" and "-component"s. [get_flags] starts
+    with "all" or "-all" and lists all components after it (even if redundant). *)
+val get_flags : unit -> string
+
+(** Components not mentioned are not affected (use the "all" component
+    at the start if you want to reset everything). *)
+val set_flags : string -> unit
+
+val set_debug_all : bool -> unit
+
+val misc : flag
+val pp_misc : t
diff --git a/lib/flags.ml b/lib/flags.ml
index 83733cf00d..57e879add7 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -46,7 +46,6 @@ let async_proofs_is_worker () = !async_proofs_worker_id <> "master"
 
 let load_vos_libraries = ref false
 
-let debug = ref false
 let xml_debug = ref false
 
 let in_debugger = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index ebd23a4d20..e10e2c8cb8 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -40,7 +40,6 @@ val async_proofs_is_worker : unit -> bool
 val load_vos_libraries : bool ref
 
 (** Debug flags *)
-val debug : bool ref
 val xml_debug : bool ref
 val in_debugger : bool ref
 val in_toplevel : bool ref
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 4e08e87084..bbc9966498 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -10,6 +10,7 @@ Loc
 Feedback
 CErrors
 CWarnings
+CDebug
 
 AcyclicGraph
 Rtree
diff --git a/lib/spawn.ml b/lib/spawn.ml
index 2fe7b31d04..27b4387b61 100644
--- a/lib/spawn.ml
+++ b/lib/spawn.ml
@@ -13,7 +13,7 @@ let prefer_sock = Sys.os_type = "Win32"
 let accept_timeout = 10.0
 
 let pr_err s = Printf.eprintf "(Spawn  ,%d) %s\n%!" (Unix.getpid ()) s
-let prerr_endline s = if !Flags.debug then begin pr_err s end else ()
+let prerr_endline s = if CDebug.(get_flag misc) then begin pr_err s end else ()
 
 type req = ReqDie | Hello of int * int