aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/nativecode.ml11
-rw-r--r--kernel/nativecode.mli4
-rw-r--r--kernel/nativeconv.ml4
-rw-r--r--kernel/nativelib.ml12
-rw-r--r--kernel/nativelibrary.ml18
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:59:21 +0000