[ci] Don't build lite versions of CI developments.

In the original Travis CI setup, the per-job time limit was an issue. However, Gitlab has much improved this problem due to a) Coq not being built for each contrib, b) user-configurable time limit. We thus disable the expensive builds from Travis: `fiat-crypto`, `formal-topology`, `geocoq`, `iris-lambda-rust`, `math-comp`, `unimath`, `vst` and instruct Gitlab to build [`geocoq`, `math-comp`, `unimath`, `vst`] in full. We also update the `math-comp` script as the `odd-order` theorem lives in a separate repository and it is a key CI case.
validsdp · May 16, 2018 · ed91bf1 · ed91bf1
1 parent cfed57b
commit ed91bf1
Show file tree

Hide file tree

Showing 8 changed files with 16 additions and 45 deletions.
diff --git a/.travis.yml b/.travis.yml
@@ -85,39 +85,24 @@ matrix:
     - if: NOT (type = pull_request)
       env:
       - TEST_TARGET="ci-equations"
-    - if: NOT (type = pull_request)
-      env:
-      - TEST_TARGET="ci-geocoq"
     - if: NOT (type = pull_request)
       env:
       - TEST_TARGET="ci-fcsl-pcm"
-    - if: NOT (type = pull_request)
-      env:
-      - TEST_TARGET="ci-fiat-crypto"
     - if: NOT (type = pull_request)
       env:
       - TEST_TARGET="ci-fiat-parsers"
     - if: NOT (type = pull_request)
       env:
       - TEST_TARGET="ci-flocq"
-    - if: NOT (type = pull_request)
-      env:
-      - TEST_TARGET="ci-formal-topology"
     - if: NOT (type = pull_request)
       env:
       - TEST_TARGET="ci-hott"
-    - if: NOT (type = pull_request)
-      env:
-      - TEST_TARGET="ci-iris-lambda-rust"
     - if: NOT (type = pull_request)
       env:
       - TEST_TARGET="ci-ltac2"
     - if: NOT (type = pull_request)
       env:
       - TEST_TARGET="ci-math-classes"
-    - if: NOT (type = pull_request)
-      env:
-      - TEST_TARGET="ci-math-comp"
     - if: NOT (type = pull_request)
       env:
       - TEST_TARGET="ci-mtac2"
@@ -127,12 +112,6 @@ matrix:
     - if: NOT (type = pull_request)
       env:
       - TEST_TARGET="ci-sf"
-    - if: NOT (type = pull_request)
-      env:
-      - TEST_TARGET="ci-unimath"
-    - if: NOT (type = pull_request)
-      env:
-      - TEST_TARGET="ci-vst"
 
     - env:
       - TEST_TARGET="lint"

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
@@ -11,6 +11,8 @@
 ########################################################################
 : "${mathcomp_CI_BRANCH:=master}"
 : "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp.git}"
+: "${oddorder_CI_BRANCH:=master}"
+: "${oddorder_CI_GITURL:=https://github.com/math-comp/odd-order.git}"
 
 ########################################################################
 # UniMath

diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
@@ -67,11 +67,6 @@ git_checkout()
     echo "${_DEST}: $(git log -1 --format='%s | %H | %cd | %aN')" )
 }
 
-checkout_mathcomp()
-{
-  git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${1}"
-}
-
 make()
 {
     # +x: add x only if defined
@@ -89,7 +84,8 @@ install_ssreflect()
 {
   echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r'
 
-  checkout_mathcomp "${mathcomp_CI_DIR}"
+  git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}"
+
   ( cd "${mathcomp_CI_DIR}/mathcomp" && \
     sed -i.bak '/ssrtest/d'     Make && \
     sed -i.bak '/odd_order/d'   Make && \

diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
@@ -6,6 +6,9 @@ ci_dir="$(dirname "$0")"
 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 lite-display )
+fiat_crypto_CI_TARGETS="lite lite-display"
+
+( cd "${fiat_crypto_CI_DIR}" && make ${fiat_crypto_CI_TARGETS} )
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
@@ -7,6 +7,4 @@ GeoCoq_CI_DIR="${CI_BUILD_DIR}/GeoCoq"
 
 git_checkout "${GeoCoq_CI_BRANCH}" "${GeoCoq_CI_GITURL}" "${GeoCoq_CI_DIR}"
 
-( cd "${GeoCoq_CI_DIR}"                                     && \
-  ./configure-ci.sh                                       && \
-  make )
+( cd "${GeoCoq_CI_DIR}" && ./configure.sh && make )
diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh
@@ -5,11 +5,10 @@ ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
 mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp"
+oddorder_CI_DIR="${CI_BUILD_DIR}/odd-order"
 
-checkout_mathcomp "${mathcomp_CI_DIR}"
+git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}"
+git_checkout "${oddorder_CI_BRANCH}" "${oddorder_CI_GITURL}" "${oddorder_CI_DIR}"
 
-# odd_order takes too much time for travis.
-( 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 )
+( cd "${mathcomp_CI_DIR}/mathcomp" && make && make install )
+( cd "${oddorder_CI_DIR}/" && make )
diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh
@@ -7,7 +7,4 @@ UniMath_CI_DIR="${CI_BUILD_DIR}/UniMath"
 
 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 )
+( cd "${UniMath_CI_DIR}" && make BUILD_COQ=no )
diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh
@@ -5,9 +5,6 @@ ci_dir="$(dirname "$0")"
 
 VST_CI_DIR="${CI_BUILD_DIR}/VST"
 
-# opam install -j ${NJOBS} -y menhir
 git_checkout "${VST_CI_BRANCH}" "${VST_CI_GITURL}" "${VST_CI_DIR}"
 
-# We have to omit progs as otherwise we timeout on Travis; on Gitlab
-# we will be able to just use `make`
-( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true -o progs )
+( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true )