Add native compute profiling, BZ#5170

1 files changed, 15 insertions, 1 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index b3b0df5c8..ba9b21bfd 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3269,7 +3269,7 @@ The call-by-value strategy is the one used in ML languages: the
 arguments of a function call are systematically weakly evaluated
 first. Despite the lazy strategy always performs fewer reductions than
 the call-by-value strategy, the latter is generally more efficient for
-evaluating purely computational expressions (i.e. with few dead code).
+evaluating purely computational expressions (i.e. with little dead code).
 
 \begin{Variants}
 \item {\tt compute} \tacindex{compute}\\
@@ -3317,6 +3317,20 @@ evaluating purely computational expressions (i.e. with few dead code).
   compilation cost is higher, so it is worth using only for intensive
   computations.
 
+  On Linux, if you have the {\tt perf} profiler installed, you can profile {\tt native\_compute} evaluations. 
+  The command
+  \begin{quote}
+    {\tt Set Native Compute Profiling}
+  \end{quote}
+  enables profiling. Use the command
+  \begin{quote}
+    {\tt Set NativeCompute Profile Filename \str}
+  \end{quote}
+  to specify the profile output; the default is {\tt native\_compute\_profile.data}. If there's an existing file with
+  the specified name, \Coq{} will append a number to it to avoid name collisions. That means you can
+  individually profile multiple uses of {\tt native\_compute} in a script. From the Linux command line, run {\tt perf report} on
+  the profile file to see the results. Consult the {\tt perf} documentation for more details.
+
 \end{Variants}
 
 % Obsolete? Anyway not very important message