1 files changed, 89 insertions, 9 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 12dea9a30..ffcb37134 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -78,7 +78,7 @@ For instance
 {\tt try repeat \tac$_1$ ||
   \tac$_2$;\tac$_3$;[\tac$_{31}$|\dots|\tac$_{3n}$];\tac$_4$.}
 \end{quote}
-is understood as 
+is understood as
 \begin{quote}
 {\tt (try (repeat (\tac$_1$ || \tac$_2$)));} \\
 {\tt ((\tac$_3$;[\tac$_{31}$|\dots|\tac$_{3n}$]);\tac$_4$).}
@@ -174,7 +174,7 @@ is understood as
 \\
 {\messagetoken}\!\!\!\!\!\! & ::= & {\qstring} ~|~ {\ident} ~|~ {\integer} \\
 \\
-\tacarg & ::= & 
+\tacarg & ::= &
         {\qualid}\\
 & $|$ & {\tt ()} \\
 & $|$ & {\tt ltac :} {\atom}\\
@@ -344,7 +344,7 @@ for $=1,...,n$. It fails if the number of focused goals is not exactly $n$.
     expects multiple goals, such as {\tt swap}, would act as if a single
     goal is focused.
 
-  \item {\tacexpr} {\tt ; [ } {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]} 
+  \item {\tacexpr} {\tt ; [ } {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}
 
     This variant of local tactic application is paired with a
     sequence.  In this variant, $n$ must be the number of goals
@@ -782,7 +782,7 @@ setting option {\tt Printing All}, see Section~\ref{SetPrintingAll}).
 \begin{coq_example}
 Ltac f x :=
   match x with
-    context f [S ?X] => 
+    context f [S ?X] =>
     idtac X;                    (* To display the evaluation order *)
     assert (p := eq_refl 1 : X=1);    (* To filter the case X=1 *)
     let x:= context f[O] in assert (x=O) (* To observe the context *)
@@ -1026,7 +1026,7 @@ Reset Initial.
 \index{Tacticals!abstract@{\tt abstract}}}
 
 From the outside ``\texttt{abstract \tacexpr}'' is the same as
-{\tt solve \tacexpr}. Internally it saves an auxiliary lemma called 
+{\tt solve \tacexpr}. Internally it saves an auxiliary lemma called
 {\ident}\texttt{\_subproof}\textit{n} where {\ident} is the name of the
 current goal and \textit{n} is chosen so that this is a fresh name.
 Such auxiliary lemma is inlined in the final proof term
@@ -1196,6 +1196,86 @@ s: & continue current evaluation without stopping\\
 r $n$: & advance $n$ steps further\\
 r {\qstring}: & advance up to the next call to ``{\tt idtac} {\qstring}''\\
 \end{tabular}
+
+\subsection[Profiling {\ltac} tactics]{Profiling {\ltac} tactics\optindex{Ltac Profiling}\comindex{Show Ltac Profile}\comindex{Reset Ltac Profile}}
+
+It is possible to measure the time spent in invocations of primitive tactics as well as tactics defined in {\ltac} and their inner invocations. The primary use is the development of complex tactics, which can sometimes be so slow as to impede interactive usage. The reasons for the performence degradation can be intricate, like a slowly performing {\ltac} match or a sub-tactic whose performance only degrades in certain situations. The profiler generates a call tree and indicates the time spent in a tactic depending its calling context. Thus it allows to locate the part of a tactic definition that contains the performance bug.
+
+\begin{quote}
+{\tt Set Ltac Profiling}.
+\end{quote}
+Enables the profiler
+
+\begin{quote}
+{\tt Unset Ltac Profiling}.
+\end{quote}
+Disables the profiler
+
+\begin{quote}
+{\tt Show Ltac Profile}.
+\end{quote}
+Prints the profile
+
+\begin{quote}
+{\tt Show Ltac Profile} {\qstring}.
+\end{quote}
+Prints a profile for all tactics that start with {\qstring}. Append a period (.) to the string if you only want exactly that name.
+
+\begin{quote}
+{\tt Reset Profile}.
+\end{quote}
+Resets the profile, that is, deletes all accumulated information
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+\begin{coq_example*}
+Require Import Coq.omega.Omega.
+
+Ltac mytauto := tauto.
+Ltac tac := intros; repeat split; omega || mytauto.
+
+Notation max x y := (x + (y - x)) (only parsing).
+\end{coq_example*}
+\begin{coq_example*}
+Goal forall x y z A B C D E F G H I J K L M N O P Q R S T U V W X Y Z,
+    max x (max y z) = max (max x y) z /\ max x (max y z) = max (max x y) z
+    /\ (A /\ B /\ C /\ D /\ E /\ F /\ G /\ H /\ I /\ J /\ K /\ L /\ M /\ N /\ O /\ P /\ Q /\ R /\ S /\ T /\ U /\ V /\ W /\ X /\ Y /\ Z
+        -> Z /\ Y /\ X /\ W /\ V /\ U /\ T /\ S /\ R /\ Q /\ P /\ O /\ N /\ M /\ L /\ K /\ J /\ I /\ H /\ G /\ F /\ E /\ D /\ C /\ B /\ A).
+Proof.
+\end{coq_example*}
+\begin{coq_example}
+  Set Ltac Profiling.
+  tac.
+\end{coq_example}
+{\let\textit\texttt% use tt mode for the output of ltacprof
+\begin{coq_example}
+  Show Ltac Profile.
+\end{coq_example}
+\begin{coq_example}
+  Show Ltac Profile "omega".
+\end{coq_example}
+}
+\begin{coq_example*}
+Abort.
+Unset Ltac Profiling.
+\end{coq_example*}
+
+\tacindex{start ltac profiling}\tacindex{stop ltac profiling}
+The following two tactics behave like {\tt idtac} but enable and disable the profiling. They allow you to exclude parts of a proof script from profiling.
+
+\begin{quote}
+{\tt start ltac profiling}.
+\end{quote}
+
+\begin{quote}
+{\tt stop ltac profiling}.
+\end{quote}
+
+You can also pass the {\tt -profile-ltac} command line option to {\tt coqc}, which performs a {\tt Set Ltac Profiling} at the beginning of each document, and a {\tt Show Ltac Profile} at the end.
+
+Note that the profiler currently does not handle backtracking into multi-success tactics, and issues a warning to this effect in many cases when such backtracking occurs.
+
 \endinput
 
 \subsection{Permutation on closed lists}
@@ -1229,7 +1309,7 @@ Another more complex example is the problem of permutation on closed
 lists. The aim is to show that a closed list is a permutation of
 another one.  First, we define the permutation predicate as shown on
 Figure~\ref{permutpred}.
- 
+
 \begin{figure}[p]
 \begin{center}
 \fbox{\begin{minipage}{0.95\textwidth}
@@ -1555,7 +1635,7 @@ Figure~\ref{isoslem} gives examples of what can be solved by {\tt IsoProve}.
 \begin{center}
 \fbox{\begin{minipage}{0.95\textwidth}
 \begin{coq_example*}
-Lemma isos_ex1 : 
+Lemma isos_ex1 :
   forall A B:Set, A * unit * B = B * (unit * A).
 Proof.
 intros; IsoProve.
@@ -1575,7 +1655,7 @@ Qed.
 \label{isoslem}
 \end{figure}
 
-%%% Local Variables: 
+%%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
-%%% End: 
+%%% End: