Add timing scripts

This commit adds timing scripts from
https://github.com/JasonGross/coq-scripts/tree/master/timing into the
tools folder, and integrates them into coq_makefile and Coq's makefile.
The main added makefile targets are:

- the `TIMING` variable - when non-empty, this creates for each built
  `.v` file a `.v.timing` variable (or `.v.before-timing` or
  `.v.after-timing` for `TIMING=before` and `TIMING=after`, respectively)
- `pretty-timed TGTS=...` - runs `make $(TGTS)` and prints a table of
  sorted timings at the end, saving it to `time-of-build-pretty.log`
- `make-pretty-timed-before TGTS=...`, `make-pretty-timed-after
  TGTS=...` - runs `make $(TGTS)`, and saves the timing data to the file
  `time-of-build-before.log` or `time-of-build-after.log`, respectively
- `print-pretty-timed-diff` - prints a table with the difference between
  the logs recorded by `make-pretty-timed-before` and
  `make-pretty-timed-after`, saving the table to
  `time-of-build-both.log`
- `print-pretty-single-time-diff BEFORE=... AFTER=...` - this prints a
  table with the differences between two `.v.timing` files, and saves
  the output to `time-of-build-pretty.log`
- `*.v.timing.diff` - this saves the result of
  `print-pretty-single-time-diff` for each target to the
  `.v.timing.diff` file
- `all.timing.diff` (`world.timing.diff` and `coq.timing.diff` in Coq's
  own Makefile) - makes all `*.v.timing.diff` targets

N.B. We need to make `make pretty-timed` fail if `make` fails.  To do
this, we need to get around the fact that pipes swallow exit codes.
There are a few solutions in
https://stackoverflow.com/questions/23079651/equivalent-of-pipefail-in-gnu-make;
we choose the temporary file rather than requiring the shell of the
makefile to be bash.

1 files changed, 85 insertions, 4 deletions

diff --git a/Makefile.build b/Makefile.build
index 3f870ed172..2179bafe3b 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -34,6 +34,12 @@ TIMED ?=
 # it could be set to "'/usr/bin/time -p'".
 TIMECMD ?=
 
+# When non-empty, -time is passed to coqc and the output is recorded
+# in a timing file for each .v file.  If set to "before" or "after",
+# the file name for foo.v is foo.v.$(TIMING)-timing; otherwise, it is
+# foo.v.timing
+TIMING ?=
+
 # Non-empty skips the update of all dependency .d files:
 NO_RECALC_DEPS ?=
 
@@ -43,6 +49,16 @@ VALIDATE ?=
 # Is "-xml" when building XML library:
 COQ_XML ?=
 
+# Output file names for timed builds
+TIME_OF_BUILD_FILE               ?= time-of-build.log
+TIME_OF_BUILD_BEFORE_FILE        ?= time-of-build-before.log
+TIME_OF_BUILD_AFTER_FILE         ?= time-of-build-after.log
+TIME_OF_PRETTY_BUILD_FILE        ?= time-of-build-pretty.log
+TIME_OF_PRETTY_BOTH_BUILD_FILE   ?= time-of-build-both.log
+TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line
+BEFORE ?=
+AFTER ?=
+
 ###########################################################################
 # Default starting rule
 ###########################################################################
@@ -53,6 +69,9 @@ world: coq coqide documentation revision
 
 coq: coqlib coqbinaries tools
 
+world.timing.diff: coq.timing.diff
+coq.timing.diff: coqlib.timing.diff
+
 # Note: 'world' does not build the bytecode binaries anymore.
 # For that, you can use the 'byte' rule. Native and byte compilations
 # shouldn't be done in a same make -j... run, otherwise both ocamlc and
@@ -60,7 +79,7 @@ coq: coqlib coqbinaries tools
 
 byte: coqbyte coqide-byte pluginsbyte printers
 
-.PHONY: world coq byte
+.PHONY: world coq byte world.timing.diff coq.timing.diff
 
 ###########################################################################
 # Includes
@@ -78,6 +97,53 @@ include Makefile.install
 include Makefile.dev      ## provides the 'printers' and 'revision' rules
 
 ###########################################################################
+# Timing targets
+###########################################################################
+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::
+	$(HIDE)rm -f pretty-timed-success.ok
+	$(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)
+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)
+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'
+	$(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'
+	$(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)
+endif
+endif
+pretty-timed:
+	$(HIDE)$(MAKE) --no-print-directory make-pretty-timed
+	$(HIDE)$(MAKE) --no-print-directory print-pretty-timed
+.PHONY: pretty-timed make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff
+
+ifneq (,$(TIMING))
+TIMING_ARG=-time
+ifeq (after,$(TIMING))
+TIMING_EXT=after-timing
+else
+ifeq (before,$(TIMING))
+TIMING_EXT=before-timing
+else
+TIMING_EXT=timing
+endif
+endif
+else
+TIMING_ARG=
+endif
+
+###########################################################################
 
 # This include below will lauch the build of all .d.
 # The - at front is for disabling warnings about currently missing ones.
@@ -616,18 +682,28 @@ OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack
 # since they are all mentioned in at least one Declare ML Module in some .v
 
 coqlib: theories plugins
+coqlib.timing.diff: theories.timing.diff plugins.timing.diff
 
 theories: $(THEORIESVO)
 plugins: $(PLUGINSVO)
 
-.PHONY: coqlib theories plugins
+theories.timing.diff: $(THEORIESVO:.vo=.v.timing.diff)
+plugins.timing.diff: $(PLUGINSVO:.vo=.v.timing.diff)
+
+.PHONY: coqlib theories plugins coqlib.timing.diff theories.timing.diff plugins.timing.diff
 
 # The .vo files in Init are built with the -noinit option
 
+ifneq (,$(TIMING))
+TIMING_EXTRA = > $<.$(TIMING_EXT)
+else
+TIMING_EXTRA =
+endif
+
 theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP)
 	$(SHOW)'COQC $(COQ_XML) -noinit $<'
 	$(HIDE)rm -f theories/Init/$*.glob
-	$(HIDE)$(BOOTCOQC) $< $(COQ_XML) -noinit -R theories Coq
+	$(HIDE)$(BOOTCOQC) $< $(COQ_XML) -noinit -R theories Coq $(TIMING_ARG) $(TIMING_EXTRA)
 
 # MExtraction.v generates the ml core file of the micromega tactic.
 # We check that this generated code is still in sync with the version
@@ -654,13 +730,18 @@ $(MICROMEGAV:.v=.vo) $(MICROMEGAV:.v=.glob) : $(MICROMEGAV) theories/Init/Prelud
 %.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP)
 	$(SHOW)'COQC      $<'
 	$(HIDE)rm -f $*.glob
-	$(HIDE)$(BOOTCOQC) $<
+	$(HIDE)$(BOOTCOQC) $< $(TIMING_ARG) $(TIMING_EXTRA)
 ifdef VALIDATE
 	$(SHOW)'COQCHK    $(call vo_to_mod,$@)'
 	$(HIDE)$(CHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \
 	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
 endif
 
+%.v.timing.diff: %.v.before-timing %.v.after-timing
+	$(SHOW)PYTHON TIMING-DIFF $<
+	$(HIDE)$(MAKE) --no-print-directory print-pretty-single-time-diff BEFORE=$*.v.before-timing AFTER=$*.v.after-timing TIME_OF_PRETTY_BUILD_FILE="$@"
+
+
 # Dependencies of .v files
 
 %.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT)