diff options
| author | Maxime Dénès | 2020-10-15 15:31:51 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2021-02-24 15:09:15 +0100 |
| commit | 068031ff7da092c1e2d35db27d713b9606960c42 (patch) | |
| tree | 2a3e2ae6a82e60a76ef31659ff305d70a4b2ea39 /kernel/nativecode.ml | |
| parent | 264aba2484312a2172cd36dd9b89ed66e4f38864 (diff) | |
Infrastructure for fine-grained debug flags
Diffstat (limited to 'kernel/nativecode.ml')
| -rw-r--r-- | kernel/nativecode.ml | 11 |
1 files changed, 8 insertions, 3 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 |