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.

1 files changed, 8 insertions, 0 deletions

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;