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

diff --git a/Makefile b/Makefile
index a6a73d249..2e49c84b5 100644
--- a/Makefile
+++ b/Makefile
@@ -17,7 +17,7 @@
 # read
 #    http://miller.emu.id.au/pmiller/books/rmch/
 # before complaining.
-# 
+#
 # When you are working in a subdir, you can compile without moving to the
 # upper directory using "make -C ..", and the output is still understood
 # by Emacs' next-error.
@@ -168,7 +168,7 @@ Makefile $(wildcard Makefile.*) config/Makefile : ;
 # Cleaning
 ###########################################################################
 
-.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean devdocclean
+.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean timingclean devdocclean
 
 clean: objclean cruftclean depclean docclean devdocclean
 
@@ -239,16 +239,19 @@ cacheclean:
 cleanconfig:
 	rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-coq dev/camlp4.dbg config/Info-*.plist
 
-distclean: clean cleanconfig cacheclean
+distclean: clean cleanconfig cacheclean timingclean
 
 voclean:
 	find theories plugins test-suite \( -name '*.vo' -o -name '*.glob' -o -name "*.cmxs" -o -name "*.native" -o -name "*.cmx" -o -name "*.cmi" -o -name "*.o" \) -delete
 	find theories plugins test-suite -name .coq-native -empty -delete
 
+timingclean:
+	find theories plugins test-suite \( -name '*.v.timing' -o -name '*.v.before-timing' -o -name "*.v.after-timing" -o -name "*.v.timing.diff" -o -name "time-of-build.log" -o -name "time-of-build-before.log" -o -name "time-of-build-after.log" -o -name "time-of-build-pretty.log" -o -name "time-of-build-both.log" \) -delete
+
 devdocclean:
 	find . -name '*.dep.ps' -o -name '*.dot' | xargs rm -f
-	rm -f $(OCAMLDOCDIR)/*.log $(OCAMLDOCDIR)/*.aux $(OCAMLDOCDIR)/*.toc 
-	rm -f $(OCAMLDOCDIR)/ocamldoc.sty $(OCAMLDOCDIR)/coq.tex 
+	rm -f $(OCAMLDOCDIR)/*.log $(OCAMLDOCDIR)/*.aux $(OCAMLDOCDIR)/*.toc
+	rm -f $(OCAMLDOCDIR)/ocamldoc.sty $(OCAMLDOCDIR)/coq.tex
 	rm -f $(OCAMLDOCDIR)/html/*.html
 
 ###########################################################################
@@ -299,4 +302,3 @@ printenv:
 	@env | wc -L
 	@echo -n "Total (win32 limit is 32k) : "
 	@env | wc -m
-