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-vst.sh | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'dev/ci/ci-vst.sh')

diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh
index 79001c547b..7a097eaab4 100755
--- 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 )
-- 
cgit v1.2.3