From ed91bf1fce168026675f986a0069ca596ad2b806 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 14 May 2018 22:29:38 +0200
Subject: [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.
---
 dev/ci/ci-math-comp.sh | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

(limited to 'dev/ci/ci-math-comp.sh')

diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh
index 8c6b910bbb..20328baf2a 100755
--- 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 )
-- 
cgit v1.2.3