NativeCompute Timing: Use real, not user time

User time is unreliable for `native_compute`.

Also output time spent in conversion to native code, just in case that
is ever slow.

Note that this also removes spurious newlines in the output.

Fixes #11962

4 files changed, 29 insertions, 19 deletions

diff --git a/doc/changelog/04-tactics/11023-nativecompute-timing.rst b/doc/changelog/04-tactics/11023-nativecompute-timing.rst
deleted file mode 100644
index e8cdfcca21..0000000000
--- a/doc/changelog/04-tactics/11023-nativecompute-timing.rst
+++ /dev/null
@@ -1,7 +0,0 @@
-- 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/changelog/04-tactics/11025-nativecompute-timing.rst b/doc/changelog/04-tactics/11025-nativecompute-timing.rst
new file mode 100644
index 0000000000..cb77457c31
--- /dev/null
+++ b/doc/changelog/04-tactics/11025-nativecompute-timing.rst
@@ -0,0 +1,11 @@
+- **Changed:** 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 conversion to
+  native code, 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
+  (`#11025 <https://github.com/coq/coq/pull/11025>`_, by Jason Gross).
+  Additionally, the timing information now uses real time rather than
+  user time (Fixes `#11962
+  <https://github.com/coq/coq/issues/11962>`_, `#11963
+  <https://github.com/coq/coq/pull/11963>`_, by Jason Gross)
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 6a280b74c2..7da453b7af 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3134,8 +3134,10 @@ the conversion in hypotheses :n:`{+ @ident}`.
    .. 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.
+      timing information for the conversion to native code,
+      compilation, execution, and reification phases of native
+      compilation.  Timing is printed in units of seconds of
+      wall-clock time.
 
    .. flag:: NativeCompute Profiling
 
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index c1ca40329a..34498458a4 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -498,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