diff options
| -rwxr-xr-x | dev/ci/ci-color.sh | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-cpdt.sh | 3 | ||||
| -rwxr-xr-x | dev/ci/ci-fiat-crypto.sh | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-fiat-parsers.sh | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-formal-topology.sh | 6 | ||||
| -rwxr-xr-x | dev/ci/ci-geocoq.sh | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-hott.sh | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-iris-coq.sh | 4 | ||||
| -rwxr-xr-x | dev/ci/ci-math-classes.sh | 4 | ||||
| -rwxr-xr-x | dev/ci/ci-math-comp.sh | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-metacoq.sh | 4 | ||||
| -rwxr-xr-x | dev/ci/ci-tlc.sh | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-unimath.sh | 3 |
13 files changed, 18 insertions, 20 deletions
diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index 309050057..6e2565261 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 8b725f6fe..5e34a206e 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 5ca3ac47f..ed5cdd286 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 292331b81..d7fde9738 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 2556f84a5..347471164 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 eadeb7c38..9dfe2116d 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 693135a4c..aa2edff7a 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 2d127ddc1..7526fe9a4 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 2837dee96..264e24a82 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 701403f2c..e49ee5b17 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 c813b1fe9..9df1e82d9 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 8ecd8c441..44f9fcd0a 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 66b56add7..10fd56d11 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" ) |