Merge branch 'v8.7'

5 files changed, 171 insertions, 7 deletions

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 5966ac468c..7e07868a38 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -486,15 +486,17 @@ where there is a hole in that place.
 
 \subsection{\tt Set Typeclasses Legacy Resolution}
 \optindex{Typeclasses Legacy Resolution}
+\emph{Deprecated since 8.7}
 
 This option (off by default) uses the 8.5 implementation of resolution.
 Use for compatibility purposes only (porting and debugging).
 
 \subsection{\tt Set Typeclasses Module Eta}
 \optindex{Typeclasses Modulo Eta}
+\emph{Deprecated since 8.7}
 
 This option allows eta-conversion for functions and records during
-unification of type-classes. This option is now unsupported in 8.6 with
+unification of type-classes. This option is unsupported since 8.6 with
 {\tt Typeclasses Filtered Unification} set, but still affects the
 default unification strategy, and the one used in {\tt Legacy
   Resolution} mode. It is \emph{unset} by default. If {\tt Typeclasses
@@ -505,7 +507,7 @@ pattern-matching is not up-to eta.
 \subsection{\tt Set Typeclasses Limit Intros}
 \optindex{Typeclasses Limit Intros}
 
-This option (on by default in Coq 8.6 and below) controls the ability to
+This option (on by default) controls the ability to
 apply hints while avoiding (functional) eta-expansions in the generated
 proof term. It does so by allowing hints that conclude in a product to
 apply to a goal with a matching product directly, avoiding an
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 2fc1c8764a..f60908da6c 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -278,7 +278,8 @@ tactic is replaced by the default one if not specified.
   as implicit arguments of the special constant
   \texttt{Program.Tactics.obligation}.
 \item {\tt Set Shrink Obligations}\optindex{Shrink Obligations}
-  Control whether obligations should have their
+\emph{Deprecated since 8.7}
+  This option (on by default) controls whether obligations should have their
   context minimized to the set of variables used in the proof of the
   obligation, to avoid unnecessary dependencies.
 \end{itemize}
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index f3bc2dd05e..3ce1d4ecd8 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1131,8 +1131,9 @@ on. This can be obtained thanks to the option below.
 \optindex{Shrink Abstract}
 {\tt Set Shrink Abstract}
 \end{quote}
+\emph{Deprecated since 8.7}
 
-When set, all lemmas generated through \texttt{abstract {\tacexpr}}
+When set (default), all lemmas generated through \texttt{abstract {\tacexpr}}
 and \texttt{transparent\_abstract {\tacexpr}} are quantified only over the
 variables that appear in the term constructed by \texttt{\tacexpr}.
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index ecb89b5fb8..a23c432322 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3485,6 +3485,7 @@ reduced to \texttt{S t}.
 \optindex{Refolding Reduction}
 {\tt Refolding Reduction}
 \end{quote}
+\emph{Deprecated since 8.7}
 
 This option (off by default) controls the use of the refolding strategy
 of {\tt cbn} while doing reductions in unification, type inference and
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}