Alternate way of doing timing on ci

This puts the boilerplate all in one place

13 files changed, 20 insertions, 19 deletions

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 )
+