Merge PR #745: Add timing scripts

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 000000000..54d3cfc3e
--- /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 000000000..8b1378917
--- /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 000000000..36c3a18c2
--- /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 000000000..729de2f36
--- /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 000000000..b25bc3683
--- /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 000000000..56815d241
--- /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 000000000..8b1378917
--- /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 000000000..54d3cfc3e
--- /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 000000000..36c3a18c2
--- /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 000000000..8b1378917
--- /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 000000000..54d3cfc3e
--- /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 000000000..36c3a18c2
--- /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 000000000..932363a12
--- /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 000000000..790e05713
--- /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 000000000..851e2b973
--- /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 000000000..18f0f34b2
--- /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 000000000..790e05713
--- /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 000000000..115c1f95b
--- /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 000000000..790e05713
--- /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 000000000..9786af10a
--- /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