From a0c84abf1f3078c1ba42df1b588acbac4bc2e4df Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 6 Jun 2017 14:20:52 -0400
Subject: Display timing data travis for various projects

HoTT, which builds it's own makefile, and supports timing data, makes
use of its own timing script.

Everything else goes through the coq-bundled timing scripts.
---
 dev/ci/ci-color.sh           | 2 +-
 dev/ci/ci-cpdt.sh            | 3 +--
 dev/ci/ci-fiat-crypto.sh     | 2 +-
 dev/ci/ci-fiat-parsers.sh    | 2 +-
 dev/ci/ci-formal-topology.sh | 6 +++---
 dev/ci/ci-geocoq.sh          | 2 +-
 dev/ci/ci-hott.sh            | 2 +-
 dev/ci/ci-iris-coq.sh        | 4 ++--
 dev/ci/ci-math-classes.sh    | 4 ++--
 dev/ci/ci-math-comp.sh       | 2 +-
 dev/ci/ci-metacoq.sh         | 4 ++--
 dev/ci/ci-tlc.sh             | 2 +-
 dev/ci/ci-unimath.sh         | 3 +--
 13 files changed, 18 insertions(+), 20 deletions(-)

(limited to 'dev')

diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index 309050057c..6e25652616 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 )
+( cd ${Color_CI_DIR} && make Makefile.coq && make pretty-timed )
diff --git a/dev/ci/ci-cpdt.sh b/dev/ci/ci-cpdt.sh
index 8b725f6fec..5e34a206ec 100755
--- a/dev/ci/ci-cpdt.sh
+++ b/dev/ci/ci-cpdt.sh
@@ -6,5 +6,4 @@ source ${ci_dir}/ci-common.sh
 wget http://adam.chlipala.net/cpdt/cpdt.tgz
 tar xvfz cpdt.tgz
 
-( cd cpdt && make clean && make )
-
+( cd cpdt && make clean && (make TIMED=1 2>&1 | tee time-of-build.log; exit ${PIPESTATUS[0]}) && make -f Makefile.coq print-pretty-timed )
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index 5ca3ac47fc..ed5cdd2862 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 lite )
+( cd ${fiat_crypto_CI_DIR} && make pretty-timed TGTS=lite )
diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh
index 292331b813..d7fde97383 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 parsers parsers-examples && make fiat-core )
+( cd ${fiat_parsers_CI_DIR} && make pretty-timed TGTS="parsers parsers-examples fiat-core" )
diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh
index 2556f84a55..347471164b 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 && make install )
+( cd ${math_classes_CI_DIR} && make pretty-timed TGTS="all" && make install )
 
 # Setup Corn
 
 git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR}
 
-( cd ${Corn_CI_DIR} && make && make install )
+( cd ${Corn_CI_DIR} && make pretty-timed TGTS="all" && 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 )
+( 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 )
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
index eadeb7c38c..9dfe2116dd 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 )
+  make pretty-timed TGTS=all )
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index 693135a4c9..aa2edff7aa 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -7,4 +7,4 @@ HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT
 
 git_checkout ${HoTT_CI_BRANCH} ${HoTT_CI_GITURL} ${HoTT_CI_DIR}
 
-( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make )
+( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && git submodule update --init --recursive && ./etc/coq-scripts/timing/make-pretty-timed-or-error.sh )
diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh
index 2d127ddc1b..7526fe9a43 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 && make install )
+( cd ${stdpp_CI_DIR} && make pretty-timed TGTS="all" && make install )
 
 # Build iris now
-( cd ${Iris_CI_DIR} && make )
+( cd ${Iris_CI_DIR} && make pretty-timed TGTS="all" )
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
index 2837dee963..264e24a821 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 && make install )
+( cd ${math_classes_CI_DIR} && make pretty-timed TGTS="all" && make install )
 
 # Setup Corn
 
 git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR}
 
-( cd ${Corn_CI_DIR} && make )
+( cd ${Corn_CI_DIR} && make pretty-timed TGTS="all" && make install )
diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh
index 701403f2cf..e49ee5b171 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 all )
+  make Makefile.coq && make -f Makefile.coq pretty-timed TGTS="all" )
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh
index c813b1fe99..9df1e82d94 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 && make install )
+( cd ${unicoq_CI_DIR} && coq_makefile -f Make -o Makefile && make pretty-timed TGTS="all" && 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 )
+( cd ${metacoq_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make pretty-timed TGTS="all" )
diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh
index 8ecd8c441d..44f9fcd0ae 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 )
+( cd ${tlc_CI_DIR} && (make TIMED=1 | tee time-of-build.log; exit ${PIPESTATUS[0]}) && make -C src -f Makefile.coq print-pretty-timed )
diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh
index 66b56add77..10fd56d11e 100755
--- a/dev/ci/ci-unimath.sh
+++ b/dev/ci/ci-unimath.sh
@@ -10,5 +10,4 @@ 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 )
-
+  make BUILD_COQ=no pretty-timed TGTS="all" )
-- 
cgit v1.2.3