From 62b8d99f1430a8a477d36be86d91aba8807659db Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Wed, 7 Jun 2017 13:33:42 -0400
Subject: 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.
---
 Makefile.common | 16 +++++++++++-----
 1 file changed, 11 insertions(+), 5 deletions(-)

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index 100698321..85ecb1a08 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -12,7 +12,7 @@
 # Executables
 ###########################################################################
 
-COQMKTOP:=bin/coqmktop$(EXE) 
+COQMKTOP:=bin/coqmktop$(EXE)
 
 COQTOPBYTE:=bin/coqtop.byte$(EXE)
 COQTOPEXE:=bin/coqtop$(EXE)
@@ -25,9 +25,15 @@ COQWC:=bin/coqwc$(EXE)
 COQDOC:=bin/coqdoc$(EXE)
 COQC:=bin/coqc$(EXE)
 COQWORKMGR:=bin/coqworkmgr$(EXE)
+COQMAKE_ONE_TIME_FILE:=tools/make-one-time-file.py
+COQTIME_FILE_MAKER:=tools/TimeFileMaker.py
+COQMAKE_BOTH_TIME_FILES:=tools/make-both-time-files.py
+COQMAKE_BOTH_SINGLE_TIMING_FILES:=tools/make-both-single-timing-files.py
 
 TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\
 	$(COQWORKMGR)
+TOOLS_HELPERS:=tools/CoqMakefile.in $(COQMAKE_ONE_TIME_FILE) $(COQTIME_FILE_MAKER)\
+	$(COQMAKE_BOTH_TIME_FILES) $(COQMAKE_BOTH_SINGLE_TIMING_FILES)
 
 COQDEPBOOT:=bin/coqdep_boot$(EXE)
 OCAMLLIBDEP:=bin/ocamllibdep$(EXE)
@@ -64,7 +70,7 @@ DYNLIB:=.cma
 endif
 
 INSTALLBIN:=install
-INSTALLLIB:=install -m 644 
+INSTALLLIB:=install -m 644
 INSTALLSH:=./install.sh
 MKDIR:=install -d
 
@@ -191,7 +197,7 @@ LIBFILES:=$(ALLVO) $(call vo_to_cm,$(ALLVO)) \
 	    $(call vo_to_obj,$(ALLVO)) \
 	    $(VFILES) $(GLOBFILES)
 
-# For emacs: 
-# Local Variables: 
-# mode: makefile 
+# For emacs:
+# Local Variables:
+# mode: makefile
 # End:
-- 
cgit v1.2.3