Add Set NativeCompute Timing

The command `Set NativeCompute Timing` causes calls to `native_compute`
(as well as kernel calls to the native compiler) to emit separate timing
information about compilation, execution, and reification.  This allows
more fine-grained timing of the native compiler without needing to set
the `-debug` flag.

5 files changed, 43 insertions, 5 deletions

diff --git a/doc/changelog/04-tactics/11023-nativecompute-timing.rst b/doc/changelog/04-tactics/11023-nativecompute-timing.rst
new file mode 100644
index 0000000000..2afa3990ac
--- /dev/null
+++ b/doc/changelog/04-tactics/11023-nativecompute-timing.rst
@@ -0,0 +1,7 @@
+- The :flag:`NativeCompute Timing` flag causes calls to
+  :tacn:`native_compute` (as well as kernel calls to the native
+  compiler) to emit separate timing information about compilation,
+  execution, and reification.  It replaces the timing information
+  previously emitted when the `-debug` flag was set, and allows more
+  fine-grained timing of the native compiler.  (`#11023
+  <https://github.com/coq/coq/pull/11023>`_, by Jason Gross).
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 53cfb973d4..36a5916868 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3113,6 +3113,12 @@ the conversion in hypotheses :n:`{+ @ident}`.
    compilation cost is higher, so it is worth using only for intensive
    computations.
 
+   .. flag:: NativeCompute Timing
+
+      This flag causes all calls to the native compiler to print
+      timing information for the compilation, execution, and
+      reification phases of native compilation.
+
    .. flag:: NativeCompute Profiling
 
       On Linux, if you have the ``perf`` profiler installed, this flag makes
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 2db674d397..97fffbd7c8 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -26,6 +26,10 @@ open Context.Rel.Declaration
 
 exception Find_at of int
 
+(* timing *)
+
+let timing_enabled = ref false
+
 (* profiling *)
 
 let profiling_enabled = ref false
@@ -79,6 +83,12 @@ let get_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
@@ -496,19 +506,23 @@ let native_norm env sigma c ty =
     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 fn = Nativelib.compile ml_filename code ~profile:profile in
-    if !Flags.debug then Feedback.msg_debug (Pp.str "Running norm ...");
+    let tc1 = Sys.time () 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
     Nativelib.call_linker ~fatal:true env ~prefix fn (Some upd);
     let t1 = Sys.time () in
     if profile then stop_profiler profiler_pid;
-    let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
-    if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
+    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 "Reification done in %.5f@." (t2 -. t1) in
-    if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
+    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
 
 let native_conv_generic pb sigma t =
diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli
index 02de034fcb..458fe70e2c 100644
--- a/pretyping/nativenorm.mli
+++ b/pretyping/nativenorm.mli
@@ -20,6 +20,9 @@ val set_profile_filename : string -> unit
 val get_profiling_enabled : unit -> bool
 val set_profiling_enabled : bool -> unit
 
+val get_timing_enabled : unit -> bool
+val set_timing_enabled : bool -> unit
+
 
 val native_norm : env -> evar_map -> constr -> types -> constr
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 99d74f16cc..4dc883725e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1448,6 +1448,14 @@ let () =
       optread  = Nativenorm.get_profiling_enabled;
       optwrite = Nativenorm.set_profiling_enabled }
 
+let () =
+  declare_bool_option
+    { optdepr  = false;
+      optname  = "enable native compute timing";
+      optkey   = ["NativeCompute"; "Timing"];
+      optread  = Nativenorm.get_timing_enabled;
+      optwrite = Nativenorm.set_timing_enabled }
+
 let _ =
   declare_bool_option
     { optdepr  = false;