Infrastructure for fine-grained debug flags

5 files changed, 29 insertions, 20 deletions

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index c19b883e3d..d517d215ed 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -24,6 +24,11 @@ open Environ
 compiler. mllambda represents a fragment of ML, and can easily be printed
 to OCaml code. *)
 
+let debug_native_flag, debug_native_compiler = CDebug.create_full ~name:"native-compiler" ()
+
+let keep_debug_files () =
+  CDebug.get_flag debug_native_flag
+
 (** Local names **)
 
 (* The first component is there for debugging purposes only *)
@@ -1939,7 +1944,7 @@ let compile_constant env sigma con cb =
     | Def t ->
       let t = Mod_subst.force_constr t in
       let code = lambda_of_constr env sigma t in
-      if !Flags.debug then Feedback.msg_debug (Pp.str "Generated lambda code");
+      debug_native_compiler (fun () -> Pp.str "Generated lambda code");
       let is_lazy = is_lazy t in
       let code = if is_lazy then mk_lazy code else code in
       let l = Constant.label con in
@@ -1950,11 +1955,11 @@ let compile_constant env sigma con cb =
           let (auxdefs,code) = compile_with_fv env sigma (Some univ) [] (Some l) code in
           (auxdefs,mkMLlam [|univ|] code)
       in
-      if !Flags.debug then Feedback.msg_debug (Pp.str "Generated mllambda code");
+      debug_native_compiler (fun () -> Pp.str "Generated mllambda code");
       let code =
         optimize_stk (Glet(Gconstant ("", con),code)::auxdefs)
       in
-      if !Flags.debug then Feedback.msg_debug (Pp.str "Optimized mllambda code");
+      debug_native_compiler (fun () -> Pp.str "Optimized mllambda code");
       code
     | _ ->
         let i = push_symbol (SymbConst con) in
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index aab6e1d4a0..1b14801fec 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -21,6 +21,10 @@ to OCaml code. *)
 type mllambda
 type global
 
+val debug_native_compiler : CDebug.t
+
+val keep_debug_files : unit -> bool
+
 val pp_global : Format.formatter -> global -> unit
 
 val mk_open : string -> global
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index d77ee759c6..7e73725c6c 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -159,12 +159,12 @@ let native_conv_gen pb sigma env univs t1 t2 =
   let ml_filename, prefix = get_ml_filename () in
   let code, upds = mk_conv_code env sigma prefix t1 t2 in
   let fn = compile ml_filename code ~profile:false in
-  if !Flags.debug then Feedback.msg_debug (Pp.str "Running test...");
+  debug_native_compiler (fun () -> Pp.str "Running test...");
   let t0 = Sys.time () in
   call_linker ~fatal:true ~prefix fn (Some upds);
   let t1 = Sys.time () in
   let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
-  if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
+  debug_native_compiler (fun () -> Pp.str time_info);
   (* TODO change 0 when we can have de Bruijn *)
   fst (conv_val env pb 0 !rt1 !rt2 univs)
 
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 1e1085d5ff..3eb3c949bc 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -38,7 +38,7 @@ let ( / ) = Filename.concat
 let my_temp_dir = lazy (CUnix.mktemp_dir "Coq_native" "")
 
 let () = at_exit (fun () ->
-    if not !Flags.debug && Lazy.is_val my_temp_dir then
+    if not (keep_debug_files ()) && Lazy.is_val my_temp_dir then
       try
         let d = Lazy.force my_temp_dir in
         Array.iter (fun f -> Sys.remove (Filename.concat d f)) (Sys.readdir d);
@@ -129,7 +129,7 @@ let call_compiler ?profile:(profile=false) ml_filename =
        ::"-w"::"a"
        ::include_dirs) @
       ["-impl"; ml_filename] in
-  if !Flags.debug then Feedback.msg_debug (Pp.str (Envars.ocamlfind () ^ " " ^ (String.concat " " args)));
+  debug_native_compiler (fun () -> Pp.str (Envars.ocamlfind () ^ " " ^ (String.concat " " args)));
   try
     let res = CUnix.sys_command (Envars.ocamlfind ()) args in
     match res with
@@ -142,7 +142,7 @@ let call_compiler ?profile:(profile=false) ml_filename =
 let compile fn code ~profile:profile =
   write_ml_code fn code;
   let r = call_compiler ~profile fn in
-  if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn;
+  if (not (keep_debug_files ())) && Sys.file_exists fn then Sys.remove fn;
   r
 
 type native_library = Nativecode.global list * Nativevalues.symbols
@@ -160,7 +160,7 @@ let compile_library (code, symb) fn =
   let fn = dirname / basename in
   write_ml_code fn ~header code;
   let _ = call_compiler fn in
-  if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn
+  if (not (keep_debug_files ())) && Sys.file_exists fn then Sys.remove fn
 
 (* call_linker links dynamically the code for constants in environment or a  *)
 (* conversion test. *)
@@ -171,7 +171,7 @@ let call_linker ?(fatal=true) ~prefix f upds =
     begin
       let msg = "Cannot find native compiler file " ^ f in
       if fatal then CErrors.user_err Pp.(str msg)
-      else if !Flags.debug then Feedback.msg_debug (Pp.str msg)
+      else debug_native_compiler (fun () -> Pp.str msg)
     end
   else
   (try
@@ -180,7 +180,7 @@ let call_linker ?(fatal=true) ~prefix f upds =
    with Dynlink.Error _ as exn ->
      let exn = Exninfo.capture exn in
      if fatal then Exninfo.iraise exn
-     else if !Flags.debug then Feedback.msg_debug CErrors.(iprint exn));
+     else debug_native_compiler (fun () -> CErrors.(iprint exn)));
   match upds with Some upds -> update_locations upds | _ -> ()
 
 let link_library ~prefix ~dirname ~basename =
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index c95880dc36..2e27fe071e 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -28,35 +28,35 @@ and translate_field prefix mp env acc (l,x) =
   match x with
   | SFBconst cb ->
      let con = Constant.make2 mp l in
-     (if !Flags.debug then
+     (debug_native_compiler (fun () ->
         let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in
-        Feedback.msg_debug (Pp.str msg));
+        Pp.str msg));
      compile_constant_field env prefix con acc cb
   | SFBmind mb ->
-     (if !Flags.debug then
+     (debug_native_compiler (fun () ->
         let id = mb.mind_packets.(0).mind_typename in
         let msg = Printf.sprintf "Compiling inductive %s..." (Id.to_string id) in
-        Feedback.msg_debug (Pp.str msg));
+        Pp.str msg));
      compile_mind_field mp l acc mb
   | SFBmodule md ->
      let mp = md.mod_mp in
-     (if !Flags.debug then
+     (debug_native_compiler (fun () ->
         let msg =
           Printf.sprintf "Compiling module %s..." (ModPath.to_string mp)
         in
-        Feedback.msg_debug (Pp.str msg));
+        Pp.str msg));
      translate_mod prefix mp env md.mod_type acc
   | SFBmodtype mdtyp ->
      let mp = mdtyp.mod_mp in
-     (if !Flags.debug then
+     (debug_native_compiler (fun () ->
         let msg =
           Printf.sprintf "Compiling module type %s..." (ModPath.to_string mp)
         in
-        Feedback.msg_debug (Pp.str msg));
+        Pp.str msg));
      translate_mod prefix mp env mdtyp.mod_type acc
 
 let dump_library mp dp env mod_expr =
-  if !Flags.debug then Feedback.msg_debug (Pp.str "Compiling library...");
+  debug_native_compiler (fun () -> Pp.str "Compiling library...");
   match mod_expr with
   | NoFunctor struc ->
       let env = add_structure mp struc empty_delta_resolver env in