Merge PR #13202: Infrastructure for fine-grained debug flags

Reviewed-by: gares
Ack-by: herbelin
Ack-by: Zimmi48
Ack-by: jfehrle
Ack-by: SkySkimmer
Ack-by: ejgallego

2 files changed, 6 insertions, 8 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 1ff1425dea..587bb90d43 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -149,7 +149,7 @@ let remove_load_path dir =
   load_paths := List.filter2 (fun p d -> p <> dir) physical logical
 
 let add_load_path (phys_path,coq_path) =
-  if !Flags.debug then
+  if CDebug.(get_flag misc) then
     Feedback.msg_notice (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
            str phys_path);
   let phys_path = CUnix.canonical_path_name phys_path in
diff --git a/checker/checker.ml b/checker/checker.ml
index 3a16b7f407..ba5e3c6d1a 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -130,8 +130,6 @@ let init_load_path () =
   includes := []
 
 
-let set_debug () = Flags.debug := true
-
 let impredicative_set = ref Declarations.PredicativeSet
 let set_impredicative_set () = impredicative_set := Declarations.ImpredicativeSet
 
@@ -218,7 +216,7 @@ let guill s = str "\"" ++ str s ++ str "\""
 let where = function
 | None -> mt ()
 | Some s ->
-  if !Flags.debug then  (str"in " ++ str s ++ str":" ++ spc ()) else (mt ())
+  if CDebug.(get_flag misc) then  (str"in " ++ str s ++ str":" ++ spc ()) else (mt ())
 
 let explain_exn = function
   | Stream.Failure ->
@@ -247,7 +245,7 @@ let explain_exn = function
     hov 0 (fnl () ++ str "User interrupt.")
   | Univ.UniverseInconsistency i ->
     let msg =
-      if !Flags.debug then
+      if CDebug.(get_flag misc) then
         str "." ++ spc() ++
           Univ.explain_universe_inconsistency Univ.Level.pr i
       else
@@ -335,7 +333,7 @@ let parse_args argv =
     | ("-Q"|"-R") :: d :: p :: rem -> set_include d p;parse rem
     | ("-Q"|"-R") :: ([] | [_]) -> usage ()
 
-    | "-debug" :: rem -> set_debug (); parse rem
+    | "-debug" :: rem -> CDebug.set_debug_all true; parse rem
 
     | "-where" :: _ ->
       Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x));
@@ -373,7 +371,7 @@ let init_with_argv argv =
   try
     parse_args argv;
     CWarnings.set_flags ("+"^Typeops.warn_bad_relevance_name);
-    if !Flags.debug then Printexc.record_backtrace true;
+    if CDebug.(get_flag misc) then Printexc.record_backtrace true;
     Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x));
     Flags.if_verbose print_header ();
     init_load_path ();
@@ -388,7 +386,7 @@ let run senv =
     let senv = compile_files senv in
     flush_all(); senv
   with e ->
-    if !Flags.debug then Printexc.print_backtrace stderr;
+    if CDebug.(get_flag misc) then Printexc.print_backtrace stderr;
     fatal_error (explain_exn e) (is_anomaly e)
 
 let start () =