From 1255a033434fd299048e68d0d8f700b49e2e58f9 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 8 Jan 2020 13:27:52 -0500
Subject: 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.
---
 doc/sphinx/proof-engine/tactics.rst | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'doc/sphinx/proof-engine')

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
-- 
cgit v1.2.3