aboutsummaryrefslogtreecommitdiffhomepage
path: root/.travis.yml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-04-29 02:12:16 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-05 18:00:53 +0200
commitdaa023eba8044404fbc708b7ae6172a918f1f18b (patch)
tree819769686947d7f4d7a179631864bac3085d96fb /.travis.yml
parent87c959542e1bed55b14d371f1be02cd60d89082c (diff)
[gitlab] [circleci] Use a Custom Docker Image as base CI setup.
We provide a custom `Dockerfile` for Coq's CI system, based on `ubuntu:bionic`. The image includes the required set of packages and OPAM switches. This greatly simplifies the Gitlab and Circle scripts, at the cost of having to push a Docker build for them to depend on. Travis is not included in this PR as it requires significant more refactoring due to lack of native Docker support. This is work in progress but ready, a build hook is used so the image is properly tagged in the Docker autobuilder. We need to improve the autobuilder setup but this last point requires some design on how to trigger it. Fixes #7383
Diffstat (limited to '.travis.yml')
-rw-r--r--.travis.yml6
1 files changed, 3 insertions, 3 deletions
diff --git a/.travis.yml b/.travis.yml
index fce19f9d9..eeb0b800e 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -39,11 +39,11 @@ env:
- NJOBS=2
# system is == 4.02.3
- COMPILER="system"
- - COMPILER_BE="4.06.0"
+ - COMPILER_BE="4.06.1"
- CAMLP5_VER=".6.14"
- CAMLP5_VER_BE=".7.03"
- FINDLIB_VER=".1.4.1"
- - FINDLIB_VER_BE=".1.7.3"
+ - FINDLIB_VER_BE=".1.8.0"
- LABLGTK="lablgtk.2.18.3 lablgtk-extras.1.6"
- LABLGTK_BE="lablgtk.2.18.6 lablgtk-extras.1.6"
- NATIVE_COMP="yes"
@@ -67,7 +67,7 @@ matrix:
- TEST_TARGET="ci-color"
- if: NOT (type = pull_request)
env:
- - TEST_TARGET="ci-compcert"
+ - TEST_TARGET="ci-compcert" EXTRA_OPAM="menhir"
- if: NOT (type = pull_request)
env:
- TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph"