Alternate way of doing timing on ci

This puts the boilerplate all in one place

15 files changed, 47 insertions, 41 deletions

diff --git a/.travis.yml b/.travis.yml
index 3cd7fdf5e3..e0cca34cc2 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -37,34 +37,34 @@ env:
   - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit"
   - TEST_TARGET="validate"                           TW="travis_wait"
   - TEST_TARGET="validate"   COMPILER="4.02.3+32bit" TW="travis_wait"
-  - TEST_TARGET="ci-bignums"
-  - TEST_TARGET="ci-color"
-  - TEST_TARGET="ci-compcert"
+  - TEST_TARGET="ci-bignums TIMED=1"
+  - TEST_TARGET="ci-color TIMED=1"
+  - TEST_TARGET="ci-compcert TIMED=1"
   - TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph"
-  - TEST_TARGET="ci-coquelicot"
-  - TEST_TARGET="ci-geocoq"
-  - TEST_TARGET="ci-fiat-crypto"
-  - TEST_TARGET="ci-fiat-parsers"
-  - TEST_TARGET="ci-flocq"
-  - TEST_TARGET="ci-formal-topology"
-  - TEST_TARGET="ci-hott"
-  - TEST_TARGET="ci-iris-coq"
-  - TEST_TARGET="ci-math-classes"
-  - TEST_TARGET="ci-math-comp"
-  - TEST_TARGET="ci-sf"
-  - TEST_TARGET="ci-unimath"
-  - TEST_TARGET="ci-vst"
+  - TEST_TARGET="ci-coquelicot TIMED=1"
+  - TEST_TARGET="ci-geocoq TIMED=1"
+  - TEST_TARGET="ci-fiat-crypto TIMED=1"
+  - TEST_TARGET="ci-fiat-parsers TIMED=1"
+  - TEST_TARGET="ci-flocq TIMED=1"
+  - TEST_TARGET="ci-formal-topology TIMED=1"
+  - TEST_TARGET="ci-hott TIMED=1"
+  - TEST_TARGET="ci-iris-coq TIMED=1"
+  - TEST_TARGET="ci-math-classes TIMED=1"
+  - TEST_TARGET="ci-math-comp TIMED=1"
+  - TEST_TARGET="ci-sf TIMED=1"
+  - TEST_TARGET="ci-unimath TIMED=1"
+  - TEST_TARGET="ci-vst TIMED=1"
   # Not ready yet for 8.7
-  # - TEST_TARGET="ci-cpdt"
-  # - TEST_TARGET="ci-metacoq"
-  # - TEST_TARGET="ci-tlc"
+  # - TEST_TARGET="ci-cpdt TIMED=1"
+  # - TEST_TARGET="ci-metacoq TIMED=1"
+  # - TEST_TARGET="ci-tlc TIMED=1"
 
 matrix:
 
   allow_failures:
   - env: TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph"
-  - env: TEST_TARGET="ci-geocoq"
-  - env: TEST_TARGET="ci-fiat-parsers"
+  - env: TEST_TARGET="ci-geocoq TIMED=1"
+  - env: TEST_TARGET="ci-fiat-parsers TIMED=1"
 
   include:
     # Full Coq test-suite with two compilers
diff --git a/Makefile.ci b/Makefile.ci
index c8bc09fdc4..1b09905cc7 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -24,4 +24,9 @@ CI_TARGETS=ci-all \
 
 # Generic rule, we use make to easy travis integraton with mixed rules
 $(CI_TARGETS): ci-%:
-	+./dev/ci/ci-$*.sh
+	rm -f ci-$*.ok
+	+(./dev/ci/ci-$*.sh 2>&1 && touch ci-$*.ok) | tee time-of-build.log
+	echo 'Aggregating timing log...' && echo -en 'travis_fold:start:coq.test.timing\\r'
+	python ./tools/make-one-time-file.py time-of-build.log
+	echo -en 'travis_fold:end:coq.test.timing\\r'
+	rm ci-$*.ok # must not be -f; we're checking to see that it exists
diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index 6e25652616..309050057c 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -32,4 +32,4 @@ sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/List/ListUt
 sed -i -e "17i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Multiset/MultisetOrder.v
 sed -i -e "13i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Set/SetUtil.v
 
-( cd ${Color_CI_DIR} && make Makefile.coq && make pretty-timed )
+( cd ${Color_CI_DIR} && make )
diff --git a/dev/ci/ci-cpdt.sh b/dev/ci/ci-cpdt.sh
index 5e34a206ec..8b725f6fec 100755
--- a/dev/ci/ci-cpdt.sh
+++ b/dev/ci/ci-cpdt.sh
@@ -6,4 +6,5 @@ source ${ci_dir}/ci-common.sh
 wget http://adam.chlipala.net/cpdt/cpdt.tgz
 tar xvfz cpdt.tgz
 
-( cd cpdt && make clean && (make TIMED=1 2>&1 | tee time-of-build.log; exit ${PIPESTATUS[0]}) && make -f Makefile.coq print-pretty-timed )
+( cd cpdt && make clean && make )
+
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index ed5cdd2862..5ca3ac47fc 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -8,4 +8,4 @@ fiat_crypto_CI_DIR=${CI_BUILD_DIR}/fiat-crypto
 git_checkout ${fiat_crypto_CI_BRANCH} ${fiat_crypto_CI_GITURL} ${fiat_crypto_CI_DIR}
 ( cd ${fiat_crypto_CI_DIR} && git submodule update --init --recursive )
 
-( cd ${fiat_crypto_CI_DIR} && make pretty-timed TGTS=lite )
+( cd ${fiat_crypto_CI_DIR} && make lite )
diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh
index d7fde97383..292331b813 100755
--- a/dev/ci/ci-fiat-parsers.sh
+++ b/dev/ci/ci-fiat-parsers.sh
@@ -7,4 +7,4 @@ fiat_parsers_CI_DIR=${CI_BUILD_DIR}/fiat
 
 git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} ${fiat_parsers_CI_DIR}
 
-( cd ${fiat_parsers_CI_DIR} && make pretty-timed TGTS="parsers parsers-examples fiat-core" )
+( cd ${fiat_parsers_CI_DIR} && make parsers parsers-examples && make fiat-core )
diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh
index 347471164b..2556f84a55 100755
--- a/dev/ci/ci-formal-topology.sh
+++ b/dev/ci/ci-formal-topology.sh
@@ -17,16 +17,16 @@ source ${ci_dir}/ci-bignums.sh
 
 git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR}
 
-( cd ${math_classes_CI_DIR} && make pretty-timed TGTS="all" && make install )
+( cd ${math_classes_CI_DIR} && make && make install )
 
 # Setup Corn
 
 git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR}
 
-( cd ${Corn_CI_DIR} && make pretty-timed TGTS="all" && make install )
+( cd ${Corn_CI_DIR} && make && make install )
 
 # Setup formal-topology
 
 git_checkout ${formal_topology_CI_BRANCH} ${formal_topology_CI_GITURL} ${formal_topology_CI_DIR}
 
-( cd ${formal_topology_CI_DIR} && (make TIMED=1 2>&1 | tee time-of-build.log; exit ${PIPESTATUS[0]}) && make -f Makefile.coq print-pretty-timed )
+( cd ${formal_topology_CI_DIR} && make )
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
index 9dfe2116dd..eadeb7c38c 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -13,4 +13,4 @@ git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} ${GeoCoq_CI_DIR}
   sed -i.bak '/Elements\/Book_1\.v/d'                Make && \
   sed -i.bak '/Elements\/Book_3\.v/d'                Make && \
   coq_makefile -f Make -o Makefile                        && \
-  make pretty-timed TGTS=all )
+  make )
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index c905558532..1bf6e9a872 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -6,6 +6,5 @@ source ${ci_dir}/ci-common.sh
 HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT
 
 git_checkout ${HoTT_CI_BRANCH} ${HoTT_CI_GITURL} ${HoTT_CI_DIR}
-( cd ${HoTT_CI_DIR} && git submodule update --init --recursive )
 
-( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && (make TIMED=1 | tee time-of-build.log; exit ${PIPESTATUS[0]}) && python ./etc/coq-scripts/timing/make-one-time-file.py time-of-build.log time-of-build-pretty.log && cat time-of-build-pretty.log )
+( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make -j ${NJOBS} )
diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh
index 7526fe9a43..2d127ddc1b 100755
--- a/dev/ci/ci-iris-coq.sh
+++ b/dev/ci/ci-iris-coq.sh
@@ -20,7 +20,7 @@ stdpp_CI_COMMIT=${IRIS_DEP[2]}
 
 git_checkout ${stdpp_CI_BRANCH} ${stdpp_CI_GITURL} ${stdpp_CI_DIR} ${stdpp_CI_COMMIT}
 
-( cd ${stdpp_CI_DIR} && make pretty-timed TGTS="all" && make install )
+( cd ${stdpp_CI_DIR} && make && make install )
 
 # Build iris now
-( cd ${Iris_CI_DIR} && make pretty-timed TGTS="all" )
+( cd ${Iris_CI_DIR} && make )
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
index 264e24a821..2837dee963 100755
--- a/dev/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math-classes.sh
@@ -15,10 +15,10 @@ source ${ci_dir}/ci-bignums.sh
 
 git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR}
 
-( cd ${math_classes_CI_DIR} && make pretty-timed TGTS="all" && make install )
+( cd ${math_classes_CI_DIR} && make && make install )
 
 # Setup Corn
 
 git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR}
 
-( cd ${Corn_CI_DIR} && make pretty-timed TGTS="all" && make install )
+( cd ${Corn_CI_DIR} && make )
diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh
index e49ee5b171..701403f2cf 100755
--- a/dev/ci/ci-math-comp.sh
+++ b/dev/ci/ci-math-comp.sh
@@ -12,4 +12,4 @@ checkout_mathcomp ${mathcomp_CI_DIR}
 ( cd ${mathcomp_CI_DIR}/mathcomp                  && \
   sed -i.bak '/PFsection/d'                  Make && \
   sed -i.bak '/stripped_odd_order_theorem/d' Make && \
-  make Makefile.coq && make -f Makefile.coq pretty-timed TGTS="all" )
+  make Makefile.coq && make -f Makefile.coq all )
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh
index 9df1e82d94..c813b1fe99 100755
--- a/dev/ci/ci-metacoq.sh
+++ b/dev/ci/ci-metacoq.sh
@@ -10,10 +10,10 @@ metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq
 
 git_checkout ${unicoq_CI_BRANCH} ${unicoq_CI_GITURL} ${unicoq_CI_DIR}
 
-( cd ${unicoq_CI_DIR} && coq_makefile -f Make -o Makefile && make pretty-timed TGTS="all" && make install )
+( cd ${unicoq_CI_DIR} && coq_makefile -f Make -o Makefile && make && make install )
 
 # Setup MetaCoq
 
 git_checkout ${metacoq_CI_BRANCH} ${metacoq_CI_GITURL} ${metacoq_CI_DIR}
 
-( cd ${metacoq_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make pretty-timed TGTS="all" )
+( cd ${metacoq_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make )
diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh
index 44f9fcd0ae..8ecd8c441d 100755
--- a/dev/ci/ci-tlc.sh
+++ b/dev/ci/ci-tlc.sh
@@ -7,4 +7,4 @@ tlc_CI_DIR=${CI_BUILD_DIR}/tlc
 
 git_checkout ${tlc_CI_BRANCH} ${tlc_CI_GITURL} ${tlc_CI_DIR}
 
-( cd ${tlc_CI_DIR} && (make TIMED=1 | tee time-of-build.log; exit ${PIPESTATUS[0]}) && make -C src -f Makefile.coq print-pretty-timed )
+( cd ${tlc_CI_DIR} && make )
diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh
index 10fd56d11e..66b56add77 100755
--- a/dev/ci/ci-unimath.sh
+++ b/dev/ci/ci-unimath.sh
@@ -10,4 +10,5 @@ git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} ${UniMath_CI_DIR}
 ( cd ${UniMath_CI_DIR}                        && \
   sed -i.bak '/Folds/d'              Makefile && \
   sed -i.bak '/HomologicalAlgebra/d' Makefile && \
-  make BUILD_COQ=no pretty-timed TGTS="all" )
+  make BUILD_COQ=no )
+