From 6799ad6240fa4d233f698c3cfa0bd5417f471bba Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 17 Dec 2019 15:14:24 -0500
Subject: 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
---
 dev/doc/INSTALL.make.md | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'dev/doc')

diff --git a/dev/doc/INSTALL.make.md b/dev/doc/INSTALL.make.md
index 3db5d0b14f..f81630c55d 100644
--- a/dev/doc/INSTALL.make.md
+++ b/dev/doc/INSTALL.make.md
@@ -102,6 +102,14 @@ Detailed Installation Procedure.
    it is recommended to compile in parallel, via make -jN where N is your number
    of cores.
 
+   If you wish to create timing logs for the standard library, you can
+   pass `TIMING=1` (for per-line timing files) or `TIMED=1` (for
+   per-file timing on stdout).  Further variables and targets are
+   available for more detailed timing analysis; see the section of the
+   reference manual on `coq_makefile`.  If there is any timing target
+   or variable supported by `coq_makefile`-made Makefiles which is not
+   supported by Coq's own Makefile, please report that as a bug.
+
 5. You can now install the Coq system. Executables, libraries, and
    manual pages are copied in some standard places of your system,
    defined at configuration time (step 3). Just do
-- 
cgit v1.2.3