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, 25 insertions, 6 deletions

diff --git a/Makefile.build b/Makefile.build
index a8ae040f8e..51689d0287 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -50,6 +50,12 @@ VALIDATE ?=
 # When non-empty, passed as extra arguments to coqtop/coqc:
 COQUSERFLAGS ?=
 
+# Option for changing sorting of timing output file
+TIMING_SORT_BY ?= auto
+# Option for changing the fuzz parameter on the output file
+TIMING_FUZZ ?= 0
+# Option for changing whether to use real or user time for timing tables
+TIMING_REAL?=
 # Output file names for timed builds
 TIME_OF_BUILD_FILE               ?= time-of-build.log
 TIME_OF_BUILD_BEFORE_FILE        ?= time-of-build-before.log
@@ -104,6 +110,19 @@ include Makefile.dev      ## provides the 'printers' and 'revision' rules
 ###########################################################################
 # Timing targets
 ###########################################################################
+ifeq (0,$(TIMING_REAL))
+TIMING_REAL_ARG :=
+TIMING_USER_ARG := --user
+else
+ifeq (1,$(TIMING_REAL))
+TIMING_REAL_ARG := --real
+TIMING_USER_ARG :=
+else
+TIMING_REAL_ARG :=
+TIMING_USER_ARG :=
+endif
+endif
+
 make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE)
 make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE)
 make-pretty-timed make-pretty-timed-before make-pretty-timed-after::
@@ -111,21 +130,21 @@ make-pretty-timed make-pretty-timed-before make-pretty-timed-after::
 	$(HIDE)($(MAKE) --no-print-directory $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE)
 	$(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed
 print-pretty-timed::
-	$(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+	$(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
 print-pretty-timed-diff::
-	$(HIDE)$(COQMAKE_BOTH_TIME_FILES) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+	$(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
 ifeq (,$(BEFORE))
 print-pretty-single-time-diff::
-	@echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing'
+	@echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing'
 	$(HIDE)false
 else
 ifeq (,$(AFTER))
 print-pretty-single-time-diff::
-	@echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing'
+	@echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing'
 	$(HIDE)false
 else
 print-pretty-single-time-diff::
-	$(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) $(BEFORE) $(AFTER) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+	$(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --fuzz=$(TIMING_FUZZ) --sort-by=$(TIMING_SORT_BY) $(TIMING_USER_ARG) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
 endif
 endif
 pretty-timed:
@@ -859,7 +878,7 @@ endif
 	$(HIDE)$(BOOTCOQC) $< -vio -noglob
 
 %.v.timing.diff: %.v.before-timing %.v.after-timing
-	$(SHOW)PYTHON TIMING-DIFF $<
+	$(SHOW)'PYTHON TIMING-DIFF $*.v.{before,after}-timing'
 	$(HIDE)$(MAKE) --no-print-directory print-pretty-single-time-diff BEFORE=$*.v.before-timing AFTER=$*.v.after-timing TIME_OF_PRETTY_BUILD_FILE="$@"