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.

2 files changed, 13 insertions, 0 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