Add --fuzz, --real, --user to timing scripts

- Add a `--fuzz` option to `make-both-single-timing-files.py`

  Passing `--fuzz=N` allows differences in character locations of up to
  `N` characters when matching lines in per-line timing diffs.

  The corresponding variable for `coq_makefile` is `TIMING_FUZZ=N`.

  See also the discussion at
  https://github.com/coq/coq/pull/11076#pullrequestreview-324791139

- Allow passing `--real` to per-file timing scripts and `--user` to
  per-line timing script.

  This allows easily comparing real times instead of user ones (or vice
  versa).

- Support `TIMING_SORT_BY` and `TIMING_FUZZ` in Coq's own build

- We also now use argparse rather than a hand-rolled argument parser;
  there were getting to be too many combinations of options.

- Fix the ordering of columns in Coq's build system; this is the
  equivalent of #8167 for Coq's build system.

Fixes #11301
Supersedes / closes #11022
Supersedes / closes #11230

1 files changed, 41 insertions, 3 deletions

diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index e5edd08995..64a4716188 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -255,14 +255,20 @@ file timing data:
     one, you can pass them via the variable ``TGTS``, e.g., ``make pretty-timed
     TGTS="a.vo b.vo"``.
 
-    .. ::
+    .. note::
        This target requires ``python`` to build the table.
 
     .. note::
        This target will *append* to the timing log; if you want a
-       fresh start, you must remove the ``filetime-of-build.log`` or
+       fresh start, you must remove the file ``time-of-build.log`` or
        ``run make cleanall``.
 
+    .. note::
+       By default the table picks up user times.  If the build log
+       contains real times (which it does by default), passing
+       ``TIMING_REAL=1`` to ``make pretty-timed`` will use real times
+       rather than user times in the table.
+
     .. example::
 
       For example, the output of ``make pretty-timed`` may look like this:
@@ -310,6 +316,16 @@ file timing data:
        (which are frequently noise); lexicographic sorting forces an order on
        files which take effectively no time to compile.
 
+       If you prefer a different sorting order, you can pass
+       ``TIMING_SORT_BY=absolute`` to sort by the total time taken, or
+       ``TIMING_SORT_BY=diff`` to sort by the signed difference in
+       time.
+
+    .. note::
+       Just like ``pretty-timed``, this table defaults to using user
+       times and supports ``TIMING_REAL=1`` to specify that real times
+       rather than user times should be used.
+
     .. example::
 
         For example, the output table from
@@ -349,7 +365,7 @@ line timing data:
 
     ::
 
-       print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing
+       print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing
 
     this target will make a sorted table of the per-line timing differences
     between the timing logs in the ``BEFORE`` and ``AFTER`` files, display it, and
@@ -364,6 +380,28 @@ line timing data:
     .. note::
        This target requires python to build the table.
 
+    .. note::
+       This target follows the same sorting order as the
+       ``print-pretty-timed-diff`` target, and supports the same
+       options for the ``TIMING_SORT_BY`` variable.
+
+    .. note::
+       By default, two lines are only considered the same if the
+       character offsets and initial code strings match.  Passing
+       ``TIMING_FUZZ=N`` relaxes this constraint by allowing the
+       character offsets to differ by up to ``N`` characters, as long
+       as the total number of characters and initial code strings
+       continue to match.  This is useful when there are small changes
+       to a file, and you want to match later lines that have not
+       changed even though the character offsets have changed.
+
+    .. note::
+       By default the table picks up real times, under the assumption
+       that when comparing line-by-line, the real time is a more
+       accurate representation as it includes disk time and time spent
+       in the native compiler.  Passing ``TIMING_REAL=0`` to ``make``
+       will use user times rather than real times in the table.
+
     .. example::
 
        For example, running  ``print-pretty-single-time-diff`` might give a table like this: