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

2 files changed, 76 insertions, 3 deletions

diff --git a/doc/changelog/08-tools/11302-better-timing-scripts-options.rst b/doc/changelog/08-tools/11302-better-timing-scripts-options.rst
new file mode 100644
index 0000000000..3b20bbf75d
--- /dev/null
+++ b/doc/changelog/08-tools/11302-better-timing-scripts-options.rst
@@ -0,0 +1,35 @@
+- **Added:**
+  The ``make-both-single-timing-files.py`` script now accepts a
+  ``--fuzz=N`` parameter on the command line which determines how many
+  characters two lines may be offset in the "before" and "after"
+  timing logs while still being considered the same line.  When
+  invoking this script via the ``print-pretty-single-time-diff``
+  target in a ``Makefile`` made by ``coq_makefile``, you can set this
+  argument by passing ``TIMING_FUZZ=N`` to ``make`` (`#11302
+  <https://github.com/coq/coq/pull/11302>`_, by Jason Gross).
+
+- **Added:**
+  The ``make-one-time-file.py`` and ``make-both-time-files.py``
+  scripts now accept a ``--real`` parameter on the command line to
+  print real times rather than user times in the tables.  The
+  ``make-both-single-timing-files.py`` script accepts a ``--user``
+  parameter to use user times.  When invoking these scripts via the
+  ``print-pretty-timed`` or ``print-pretty-timed-diff`` or
+  ``print-pretty-single-time-diff`` targets in a ``Makefile`` made by
+  ``coq_makefile``, you can set this argument by passing
+  ``TIMING_REAL=1`` (to pass ``--real``) or ``TIMING_REAL=0`` (to pass
+  ``--user``) to ``make`` (`#11302
+  <https://github.com/coq/coq/pull/11302>`_, by Jason Gross).
+
+- **Added:**
+  Coq's build system now supports both ``TIMING_FUZZ``,
+  ``TIMING_SORT_BY``, and ``TIMING_REAL`` just like a ``Makefile``
+  made by ``coq_makefile`` (`#11302
+  <https://github.com/coq/coq/pull/11302>`_, by Jason Gross).
+
+- **Fixed:**
+  The various timing targets for Coq's standard library now correctly
+  display and label the "before" and "after" columns, rather than
+  mixing them up (`#11302 <https://github.com/coq/coq/pull/11302>`_
+  fixes `#11301 <https://github.com/coq/coq/issues/11301>`_, by Jason
+  Gross).
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: