diff options
Diffstat (limited to 'pretyping/nativenorm.ml')
| -rw-r--r-- | pretyping/nativenorm.ml | 59 |
1 files changed, 29 insertions, 30 deletions
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index c950854d8f..d672ddc906 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -28,16 +28,22 @@ exception Find_at of int (* timing *) -let timing_enabled = ref false +let get_timing_enabled = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["NativeCompute"; "Timing"] + ~value:false (* profiling *) -let profiling_enabled = ref false +let get_profiling_enabled = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["NativeCompute"; "Profiling"] + ~value:false (* for supported platforms, filename for profiler results *) -let profile_filename = ref "native_compute_profile.data" - let profiler_platform () = match [@warning "-8"] Sys.os_type with | "Unix" -> @@ -48,10 +54,11 @@ let profiler_platform () = | "Win32" -> "Windows (Win32)" | "Cygwin" -> "Windows (Cygwin)" -let get_profile_filename () = !profile_filename - -let set_profile_filename fn = - profile_filename := fn +let get_profile_filename = + Goptions.declare_string_option_and_ref + ~depr:false + ~key:["NativeCompute"; "Profile"; "Filename"] + ~value:"native_compute_profile.data" (* find unused profile filename *) let get_available_profile_filename () = @@ -77,18 +84,6 @@ let get_available_profile_filename () = let _ = Feedback.msg_info (Pp.str msg) in assert false -let get_profiling_enabled () = - !profiling_enabled - -let set_profiling_enabled b = - profiling_enabled := b - -let get_timing_enabled () = - !timing_enabled - -let set_timing_enabled b = - timing_enabled := b - let invert_tag cst tag reloc_tbl = try for j = 0 to Array.length reloc_tbl - 1 do @@ -503,25 +498,29 @@ let native_norm env sigma c ty = Format.eprintf "Numbers of free variables (named): %i\n" (List.length vl1); Format.eprintf "Numbers of free variables (rel): %i\n" (List.length vl2); *) - let ml_filename, prefix = Nativelib.get_ml_filename () in - let code, upd = mk_norm_code env (evars_of_evar_map sigma) prefix c in let profile = get_profiling_enabled () in let print_timing = get_timing_enabled () in - let tc0 = Sys.time () in + let ml_filename, prefix = Nativelib.get_ml_filename () in + let tnc0 = Unix.gettimeofday () in + let code, upd = mk_norm_code env (evars_of_evar_map sigma) prefix c in + let tnc1 = Unix.gettimeofday () in + let time_info = Format.sprintf "native_compute: Conversion to native code done in %.5f" (tnc1 -. tnc0) in + if print_timing then Feedback.msg_info (Pp.str time_info); + let tc0 = Unix.gettimeofday () in let fn = Nativelib.compile ml_filename code ~profile:profile in - let tc1 = Sys.time () in - let time_info = Format.sprintf "native_compute: Compilation done in %.5f@." (tc1 -. tc0) in + let tc1 = Unix.gettimeofday () in + let time_info = Format.sprintf "native_compute: Compilation done in %.5f" (tc1 -. tc0) in if print_timing then Feedback.msg_info (Pp.str time_info); let profiler_pid = if profile then start_profiler () else None in - let t0 = Sys.time () in + let t0 = Unix.gettimeofday () in Nativelib.call_linker ~fatal:true env ~prefix fn (Some upd); - let t1 = Sys.time () in + let t1 = Unix.gettimeofday () in if profile then stop_profiler profiler_pid; - let time_info = Format.sprintf "native_compute: Evaluation done in %.5f@." (t1 -. t0) in + let time_info = Format.sprintf "native_compute: Evaluation done in %.5f" (t1 -. t0) in if print_timing then Feedback.msg_info (Pp.str time_info); let res = nf_val env sigma !Nativelib.rt1 ty in - let t2 = Sys.time () in - let time_info = Format.sprintf "native_compute: Reification done in %.5f@." (t2 -. t1) in + let t2 = Unix.gettimeofday () in + let time_info = Format.sprintf "native_compute: Reification done in %.5f" (t2 -. t1) in if print_timing then Feedback.msg_info (Pp.str time_info); EConstr.of_constr res |