Add test-suite tests for timing scripts

These work on precomputed build logs (in this case, from a recent
partial build of fiat-crypto).

They are meant to serve as human-readable sanity checks of output
format.

Separate out the sane bits of template/init.sh from the ones messing
with directory structure (which are fragile and make assumptions about
where the calling script is sourcing it from).

N.B. The test-suite removes all *.log files, so we use *.log.in.

N.B. We set COQLIB in precomputed-time-tests/run.sh, not the Makefile,
because coqc, on Windows, doesn't handle cygwin paths passed via
-coqlib, and `pwd` gives cygwin paths.

N.B. We have .gitattributes to satisfy the linter (as per
https://github.com/coq/coq/pull/6149#issuecomment-346410990)

2 files changed, 6 insertions, 5 deletions

diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh
index c4bd11c57..db34e9182 100755
--- a/test-suite/coq-makefile/template/init.sh
+++ b/test-suite/coq-makefile/template/init.sh
@@ -1,8 +1,4 @@
-set -e
-set -o pipefail
-
-export PATH=$COQBIN:$PATH
-export LC_ALL=C
+. ../template/path-init.sh
 
 rm -rf theories src Makefile Makefile.conf tmp
 git clean -dfx || true
diff --git a/test-suite/coq-makefile/template/path-init.sh b/test-suite/coq-makefile/template/path-init.sh
new file mode 100755
index 000000000..dd19ab2b1
--- /dev/null
+++ b/test-suite/coq-makefile/template/path-init.sh
@@ -0,0 +1,5 @@
+set -e
+set -o pipefail
+
+export PATH="$COQBIN:$PATH"
+export LC_ALL=C