From 51d4d83316f91abb25ea331bfdc1dcba17362dc8 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Tue, 15 Aug 2017 10:31:09 -0400
Subject: Add native compute profiling, BZ#5170

---
 doc/refman/RefMan-tac.tex | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index b3b0df5c8a..ba9b21bfd4 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
-- 
cgit v1.2.3


From 64b6b6075e461383719f6565aff2976dacc47569 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Thu, 17 Aug 2017 14:56:46 -0400
Subject: use OCaml temp_file, instead of our own version

---
 doc/refman/RefMan-tac.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index ba9b21bfd4..6e27357008 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3326,9 +3326,9 @@ evaluating purely computational expressions (i.e. with little dead code).
   \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
+  to specify the profile output; the default is {\tt native\_compute\_profile.data}. The actual filename used 
+  will contain extra characters to avoid overwriting an existing file; that filename is reported to the user. 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}
-- 
cgit v1.2.3