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.

20 files changed, 148 insertions, 0 deletions

diff --git a/test-suite/coq-makefile/timing/after/Fast.v b/test-suite/coq-makefile/timing/after/Fast.v
new file mode 100644
index 0000000000..54d3cfc3eb
--- /dev/null
+++ b/test-suite/coq-makefile/timing/after/Fast.v
@@ -0,0 +1,4 @@
+Require Coq.ZArith.BinInt.
+Definition foo0 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl.
+Definition foo1 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl.
+Definition foo2 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl.
diff --git a/test-suite/coq-makefile/timing/after/Slow.v b/test-suite/coq-makefile/timing/after/Slow.v
new file mode 100644
index 0000000000..8b13789179
--- /dev/null
+++ b/test-suite/coq-makefile/timing/after/Slow.v
@@ -0,0 +1 @@
+
diff --git a/test-suite/coq-makefile/timing/after/_CoqProject b/test-suite/coq-makefile/timing/after/_CoqProject
new file mode 100644
index 0000000000..36c3a18c2b
--- /dev/null
+++ b/test-suite/coq-makefile/timing/after/_CoqProject
@@ -0,0 +1,2 @@
+Slow.v
+Fast.v
diff --git a/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired
new file mode 100644
index 0000000000..729de2f366
--- /dev/null
+++ b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired
@@ -0,0 +1,16 @@
+Makefile:69: warning: undefined variable '*'
+Makefile:204: warning: undefined variable 'DSTROOT'
+COQDEP Fast.v
+COQDEP Slow.v
+Makefile:69: warning: undefined variable '*'
+Makefile:204: warning: undefined variable 'DSTROOT'
+Makefile:69: warning: undefined variable '*'
+Makefile:204: warning: undefined variable 'DSTROOT'
+Makefile:69: warning: undefined variable '*'
+Makefile:204: warning: undefined variable 'DSTROOT'
+COQC Slow.v
+Slow (real: 0.04, user: 0.02, sys: 0.01, mem: 45512 ko)
+COQC Fast.v
+Fast (real: 0.41, user: 0.37, sys: 0.04, mem: 395200 ko)
+Makefile:69: warning: undefined variable '*'
+Makefile:204: warning: undefined variable 'DSTROOT'
diff --git a/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired
new file mode 100644
index 0000000000..b25bc3683c
--- /dev/null
+++ b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired
@@ -0,0 +1,16 @@
+Makefile:69: warning: undefined variable '*'
+Makefile:204: warning: undefined variable 'DSTROOT'
+COQDEP Fast.v
+COQDEP Slow.v
+Makefile:69: warning: undefined variable '*'
+Makefile:204: warning: undefined variable 'DSTROOT'
+Makefile:69: warning: undefined variable '*'
+Makefile:204: warning: undefined variable 'DSTROOT'
+Makefile:69: warning: undefined variable '*'
+Makefile:204: warning: undefined variable 'DSTROOT'
+COQC Slow.v
+Slow (real: 0.40, user: 0.35, sys: 0.04, mem: 394968 ko)
+COQC Fast.v
+Fast (real: 0.04, user: 0.03, sys: 0.00, mem: 46564 ko)
+Makefile:69: warning: undefined variable '*'
+Makefile:204: warning: undefined variable 'DSTROOT'
diff --git a/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired
new file mode 100644
index 0000000000..56815d241e
--- /dev/null
+++ b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired
@@ -0,0 +1,6 @@
+After    | File Name | Before   || Change    | % Change 
+--------------------------------------------------------
+0m00.38s | Total     | 0m00.39s || -0m00.01s | -2.56%   
+--------------------------------------------------------
+0m00.35s | Slow      | 0m00.02s || +0m00.32s | +1649.99%
+0m00.03s | Fast      | 0m00.37s || -0m00.34s | -91.89%  
\ No newline at end of file
diff --git a/test-suite/coq-makefile/timing/aggregate/Fast.v b/test-suite/coq-makefile/timing/aggregate/Fast.v
new file mode 100644
index 0000000000..8b13789179
--- /dev/null
+++ b/test-suite/coq-makefile/timing/aggregate/Fast.v
@@ -0,0 +1 @@
+
diff --git a/test-suite/coq-makefile/timing/aggregate/Slow.v b/test-suite/coq-makefile/timing/aggregate/Slow.v
new file mode 100644
index 0000000000..54d3cfc3eb
--- /dev/null
+++ b/test-suite/coq-makefile/timing/aggregate/Slow.v
@@ -0,0 +1,4 @@
+Require Coq.ZArith.BinInt.
+Definition foo0 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl.
+Definition foo1 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl.
+Definition foo2 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl.
diff --git a/test-suite/coq-makefile/timing/aggregate/_CoqProject b/test-suite/coq-makefile/timing/aggregate/_CoqProject
new file mode 100644
index 0000000000..36c3a18c2b
--- /dev/null
+++ b/test-suite/coq-makefile/timing/aggregate/_CoqProject
@@ -0,0 +1,2 @@
+Slow.v
+Fast.v
diff --git a/test-suite/coq-makefile/timing/before/Fast.v b/test-suite/coq-makefile/timing/before/Fast.v
new file mode 100644
index 0000000000..8b13789179
--- /dev/null
+++ b/test-suite/coq-makefile/timing/before/Fast.v
@@ -0,0 +1 @@
+
diff --git a/test-suite/coq-makefile/timing/before/Slow.v b/test-suite/coq-makefile/timing/before/Slow.v
new file mode 100644
index 0000000000..54d3cfc3eb
--- /dev/null
+++ b/test-suite/coq-makefile/timing/before/Slow.v
@@ -0,0 +1,4 @@
+Require Coq.ZArith.BinInt.
+Definition foo0 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl.
+Definition foo1 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl.
+Definition foo2 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl.
diff --git a/test-suite/coq-makefile/timing/before/_CoqProject b/test-suite/coq-makefile/timing/before/_CoqProject
new file mode 100644
index 0000000000..36c3a18c2b
--- /dev/null
+++ b/test-suite/coq-makefile/timing/before/_CoqProject
@@ -0,0 +1,2 @@
+Slow.v
+Fast.v
diff --git a/test-suite/coq-makefile/timing/error/A.v b/test-suite/coq-makefile/timing/error/A.v
new file mode 100644
index 0000000000..932363a122
--- /dev/null
+++ b/test-suite/coq-makefile/timing/error/A.v
@@ -0,0 +1 @@
+Check I : I.
diff --git a/test-suite/coq-makefile/timing/error/_CoqProject b/test-suite/coq-makefile/timing/error/_CoqProject
new file mode 100644
index 0000000000..790e057133
--- /dev/null
+++ b/test-suite/coq-makefile/timing/error/_CoqProject
@@ -0,0 +1 @@
+A.v
diff --git a/test-suite/coq-makefile/timing/per-file-after/A.v b/test-suite/coq-makefile/timing/per-file-after/A.v
new file mode 100644
index 0000000000..851e2b9738
--- /dev/null
+++ b/test-suite/coq-makefile/timing/per-file-after/A.v
@@ -0,0 +1,4 @@
+Require Coq.ZArith.BinInt.
+Declare Reduction comp := native_compute.
+Definition foo0 := Eval comp in (Coq.ZArith.BinInt.Z.div_eucl, Coq.ZArith.BinInt.Z.div_eucl).
+Definition foo1 := Eval comp in (foo0, foo0).
diff --git a/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired b/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired
new file mode 100644
index 0000000000..18f0f34b28
--- /dev/null
+++ b/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired
@@ -0,0 +1,9 @@
+After     | Code                                                | Before    || Change    | % Change
+---------------------------------------------------------------------------------------------------
+0m00.50s  | Total                                               | 0m04.17s  || -0m03.66s | -87.96% 
+---------------------------------------------------------------------------------------------------
+0m00.145s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.192s || -0m00.04s | -24.47% 
+0m00.126s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.]        | 0m00.143s || -0m00.01s | -11.88% 
+   N/A    | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | 0m00.s    || +0m00.00s | N/A     
+0m00.s    | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] |    N/A    || +0m00.00s | N/A     
+0m00.231s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m03.836s || -0m03.60s | -93.97% 
\ No newline at end of file
diff --git a/test-suite/coq-makefile/timing/per-file-after/_CoqProject b/test-suite/coq-makefile/timing/per-file-after/_CoqProject
new file mode 100644
index 0000000000..790e057133
--- /dev/null
+++ b/test-suite/coq-makefile/timing/per-file-after/_CoqProject
@@ -0,0 +1 @@
+A.v
diff --git a/test-suite/coq-makefile/timing/per-file-before/A.v b/test-suite/coq-makefile/timing/per-file-before/A.v
new file mode 100644
index 0000000000..115c1f95bd
--- /dev/null
+++ b/test-suite/coq-makefile/timing/per-file-before/A.v
@@ -0,0 +1,4 @@
+Require Coq.ZArith.BinInt.
+Declare Reduction comp :=     vm_compute.
+Definition foo0 := Eval comp in (Coq.ZArith.BinInt.Z.div_eucl, Coq.ZArith.BinInt.Z.div_eucl).
+Definition foo1 := Eval comp in (foo0, foo0).
diff --git a/test-suite/coq-makefile/timing/per-file-before/_CoqProject b/test-suite/coq-makefile/timing/per-file-before/_CoqProject
new file mode 100644
index 0000000000..790e057133
--- /dev/null
+++ b/test-suite/coq-makefile/timing/per-file-before/_CoqProject
@@ -0,0 +1 @@
+A.v
diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh
new file mode 100755
index 0000000000..9786af10a8
--- /dev/null
+++ b/test-suite/coq-makefile/timing/run.sh
@@ -0,0 +1,68 @@
+#!/usr/bin/env bash
+
+#set -x
+set -e
+
+. ../template/init.sh
+
+cd error
+coq_makefile -f _CoqProject -o Makefile
+make cleanall
+if make pretty-timed TGTS="all" -j1; then
+    echo "Error: make pretty-timed should have failed"
+    exit 1
+fi
+
+cd ../aggregate
+coq_makefile -f _CoqProject -o Makefile
+make cleanall
+make pretty-timed TGTS="all" -j1 || exit $?
+
+cd ../before
+coq_makefile -f _CoqProject -o Makefile
+make cleanall
+make make-pretty-timed-before TGTS="all" -j1 || exit $?
+
+cd ../after
+coq_makefile -f _CoqProject -o Makefile
+make cleanall
+make make-pretty-timed-after TGTS="all" -j1 || exit $?
+rm -f time-of-build-before.log
+make print-pretty-timed-diff TIME_OF_BUILD_BEFORE_FILE=../before/time-of-build-before.log
+cp ../before/time-of-build-before.log ./
+make print-pretty-timed-diff || exit $?
+
+for ext in "" .desired; do
+    for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do
+	cat ${file}${ext} | grep -v 'warning: undefined variable' | sed s'/[0-9]//g' | sed s'/ *$//g' | sed s'/^-*$/------/g' | sed s'/  */ /g' | sed s'/\(Total.*\)-\(.*\)-/\1+\2+/g' > ${file}${ext}.processed
+    done
+done
+for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do
+    diff -u $file.desired.processed $file.processed || exit $?
+done
+
+cd ../per-file-before
+coq_makefile -f _CoqProject -o Makefile
+make cleanall
+make all TIMING=before -j2 || exit $?
+
+cd ../per-file-after
+coq_makefile -f _CoqProject -o Makefile
+make cleanall
+make all TIMING=after -j2 || exit $?
+
+find ../per-file-before/ -name "*.before-timing" -exec 'cp' '{}' './' ';'
+make all.timing.diff -j2 || exit $?
+cat A.v.timing.diff
+echo
+
+for ext in "" .desired; do
+    for file in A.v.timing.diff; do
+	cat ${file}${ext} | sed s'/[0-9]*\.[0-9]*//g' | sed s'/0//g' | sed s'/  */ /g' | sed s'/+/-/g' | sort > ${file}${ext}.processed
+    done
+done
+for file in A.v.timing.diff; do
+    diff -u $file.desired.processed $file.processed || exit $?
+done
+
+exit 0