Merge PR #745: Add timing scripts

1 files changed, 162 insertions, 3 deletions

diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index fee4de3364..768d0df763 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -60,7 +60,7 @@ subdirectory of the sources.
 
 The majority of \Coq\ projects are very similar: a collection of {\tt .v}
 files and eventually some {\tt .ml} ones (a \Coq\ plugin).  The main piece
-of metadata needed in order to build the project are the command 
+of metadata needed in order to build the project are the command
 line options to {\tt coqc} (e.g. {\tt -R, -I},
 \SeeAlso Section~\ref{coqoptions}). Collecting the list of files and
 options is the job of the {\tt \_CoqProject} file.
@@ -108,12 +108,171 @@ used in order to decide how to build them.  In particular:
 \end{itemize}
 
 The use of \texttt{.mlpack} files has to be preferred over \texttt{.mllib}
-files, since it results in a ``packed'' plugin: All auxiliary 
+files, since it results in a ``packed'' plugin: All auxiliary
 modules (as {\tt Baz} and {\tt Bazaux}) are hidden inside
 the plugin's ``name space'' ({\tt Qux\_plugin}).
 This reduces the chances of begin unable to load two distinct plugins
 because of a clash in their auxiliary module names.
 
+\paragraph{Timing targets and performance testing}
+The generated \texttt{Makefile} supports the generation of two kinds
+of timing data: per-file build-times, and per-line times for an
+individual file.
+
+The following targets and \texttt{Makefile} variables allow collection
+of per-file timing data:
+\begin{itemize}
+\item \texttt{TIMED=1} --- passing this variable will cause
+  \texttt{make} to emit a line describing the user-space build-time
+  and peak memory usage for each file built.
+
+  \texttt{Note}: On Mac OS, this works best if you've installed
+  \texttt{gnu-time}.
+
+  \texttt{Example}: For example, the output of \texttt{make TIMED=1}
+  may look like this:
+\begin{verbatim}
+COQDEP Fast.v
+COQDEP Slow.v
+COQC Slow.v
+Slow (user: 0.34 mem: 395448 ko)
+COQC Fast.v
+Fast (user: 0.01 mem: 45184 ko)
+\end{verbatim}
+\item \texttt{pretty-timed} --- this target stores the output of
+  \texttt{make TIMED=1} into \texttt{time-of-build.log}, and displays
+  a table of the times, sorted from slowest to fastest, which is also
+  stored in \texttt{time-of-build-pretty.log}.  If you want to
+  construct the log for targets other than the default one, you can
+  pass them via the variable \texttt{TGTS}, e.g., \texttt{make
+    pretty-timed TGTS="a.vo b.vo"}.
+
+  \texttt{Note}: This target requires \texttt{python} to build the table.
+
+  \texttt{Note}: This target will \emph{append} to the timing log; if
+  you want a fresh start, you must remove the file
+  \texttt{time-of-build.log} or run \texttt{make cleanall}.
+
+  \texttt{Example}: For example, the output of \texttt{make
+    pretty-timed} may look like this:
+\begin{verbatim}
+COQDEP Fast.v
+COQDEP Slow.v
+COQC Slow.v
+Slow (user: 0.36 mem: 393912 ko)
+COQC Fast.v
+Fast (user: 0.05 mem: 45992 ko)
+Time     | File Name
+--------------------
+0m00.41s | Total
+--------------------
+0m00.36s | Slow
+0m00.05s | Fast
+\end{verbatim}
+\item \texttt{print-pretty-timed-diff} --- this target builds a table
+  of timing changes between two compilations; run \texttt{make
+    make-pretty-timed-before} to build the log of the ``before''
+  times, and run \texttt{make make-pretty-timed-after} to build the
+  log of the ``after'' times.  The table is printed on the command
+  line, and stored in \texttt{time-of-build-both.log}.  This target is
+  most useful for profiling the difference between two commits to a
+  repo.
+
+  \texttt{Note}: This target requires \texttt{python} to build the table.
+
+  \texttt{Note}: The \texttt{make-pretty-timed-before} and
+  \texttt{make-pretty-timed-after} targets will \emph{append} to the
+  timing log; if you want a fresh start, you must remove the files
+  \texttt{time-of-build-before.log} and
+  \texttt{time-of-build-after.log} or run \texttt{make cleanall}
+  \emph{before} building either the ``before'' or ``after'' targets.
+
+  \texttt{Note}: The table will be sorted first by absolute time
+  differences rounded towards zero to a whole-number of seconds, then
+  by times in the ``after'' column, and finally lexicographically by
+  file name.  This will put the biggest changes in either direction
+  first, and will prefer sorting by build-time over subsecond changes
+  in build time (which are frequently noise); lexicographic sorting
+  forces an order on files which take effectively no time to compile.
+
+  \texttt{Example}: For example, the output table from \texttt{make
+    print-pretty-timed-diff} may look like this:
+\begin{verbatim}
+After    | File Name | Before   || Change    | % Change
+--------------------------------------------------------
+0m00.39s | Total     | 0m00.35s || +0m00.03s | +11.42%
+--------------------------------------------------------
+0m00.37s | Slow      | 0m00.01s || +0m00.36s | +3600.00%
+0m00.02s | Fast      | 0m00.34s || -0m00.32s | -94.11%
+\end{verbatim}
+\end{itemize}
+
+The following targets and \texttt{Makefile} variables allow collection
+of per-line timing data:
+\begin{itemize}
+\item \texttt{TIMING=1} --- passing this variable will cause
+  \texttt{make} to use \texttt{coqc -time} to write to a
+  \texttt{.v.timing} file for each \texttt{.v} file compiled, which
+  contains line-by-line timing information.
+
+  \texttt{Example}: For example, running \texttt{make all TIMING=1} may
+  result in a file like this:
+\begin{verbatim}
+Chars 0 - 26 [Require~Coq.ZArith.BinInt.] 0.157 secs (0.128u,0.028s)
+Chars 27 - 68 [Declare~Reduction~comp~:=~vm_c...] 0. secs (0.u,0.s)
+Chars 69 - 162 [Definition~foo0~:=~Eval~comp~i...] 0.153 secs (0.136u,0.019s)
+Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] 0.239 secs (0.236u,0.s)
+\end{verbatim}
+
+\item \texttt{print-pretty-single-time-diff
+  BEFORE=path/to/file.v.before-timing
+  AFTER=path/to/file.v.after-timing} --- this target will make a
+  sorted table of the per-line timing differences between the timing
+  logs in the \texttt{BEFORE} and \texttt{AFTER} files, display it,
+  and save it to the file specified by the
+  \texttt{TIME\_OF\_PRETTY\_BUILD\_FILE} variable, which defaults to
+  \texttt{time-of-build-pretty.log}.
+
+  To generate the \texttt{.v.before-timing} or
+  \texttt{.v.after-timing} files, you should pass
+  \texttt{TIMING=before} or \texttt{TIMING=after} rather than
+  \texttt{TIMING=1}.
+
+  \texttt{Note}: The sorting used here is the same as in the
+  \texttt{print-pretty-timed-diff} target.
+
+  \texttt{Note}: This target requires \texttt{python} to build the table.
+
+  \texttt{Example}: For example, running
+  \texttt{print-pretty-single-time-diff} might give a table like this:
+\begin{verbatim}
+After     | Code                                                | Before    || Change    | % Change
+---------------------------------------------------------------------------------------------------
+0m00.50s  | Total                                               | 0m04.17s  || -0m03.66s | -87.96%
+---------------------------------------------------------------------------------------------------
+0m00.145s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.192s || -0m00.04s | -24.47%
+0m00.126s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.]        | 0m00.143s || -0m00.01s | -11.88%
+   N/A    | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | 0m00.s    || +0m00.00s | N/A
+0m00.s    | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] |    N/A    || +0m00.00s | N/A
+0m00.231s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m03.836s || -0m03.60s | -93.97%
+\end{verbatim}
+
+\item \texttt{all.timing.diff}, \texttt{path/to/file.v.timing.diff}
+  --- The \texttt{path/to/file.v.timing.diff} target will make a
+  \texttt{.v.timing.diff} file for the corresponding \texttt{.v} file,
+  with a table as would be generated by the
+  \texttt{print-pretty-single-time-diff} target; it depends on having
+  already made the corresponding \texttt{.v.before-timing} and
+  \texttt{.v.after-timing} files, which can be made by passing
+  \texttt{TIMING=before} and \texttt{TIMING=after}.  The
+  \texttt{all.timing.diff} target will make such timing difference
+  files for all of the \texttt{.v} files that the \texttt{Makefile}
+  knows about.  It will fail if some \texttt{.v.before-timing} or
+  \texttt{.v.after-timing} files don't exist.
+
+  \texttt{Note}: This target requires \texttt{python} to build the table.
+\end{itemize}
+
 \paragraph{Notes about including the generated Makefile}
 
 This practice is discouraged. The contents of this file, including variable names
@@ -165,7 +324,7 @@ invoke-coqmakefile: CoqMakefile
 	or after the build (like invoking make on a subdirectory) one can
 	hook in {\tt pre-all} and {\tt post-all} extension points
 \item \texttt{-extra-phony} and \texttt{-extra} are deprecated.  To provide
-	additional target ({\tt .PHONY} or not) please use 
+	additional target ({\tt .PHONY} or not) please use
 	{\tt CoqMakefile.local}
 \end{itemize}