aboutsummaryrefslogtreecommitdiffhomepage
path: root/.travis.yml
diff options
context:
space:
mode:
authorGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-05-19 19:36:22 +0200
committerGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-05-19 19:36:22 +0200
commit931cb1d5b337b0fda54133954c2e3025e1637beb (patch)
tree233e7d763e3e14efd2bf3dc8bb63ce397165f33a /.travis.yml
parent9f11adda4bff194a3c6a66d573ce7001d4399886 (diff)
Travis: do not cache opam logs (+prettier spacing)
Diffstat (limited to '.travis.yml')
-rw-r--r--.travis.yml15
1 files changed, 13 insertions, 2 deletions
diff --git a/.travis.yml b/.travis.yml
index aa2e0e63c..a959fbf96 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -1,14 +1,21 @@
dist: trusty
+
# Travis builds are slower using sudo: false (the container-based
# infrastructure) as of March 2017; see
# https://github.com/coq/coq/pull/467 for some discussion.
sudo: required
+
# Until Ocaml becomes a language, we set a known one.
language: c
+
cache:
apt: true
directories:
- $HOME/.opam
+
+before_cache:
+ - rm -rf ~/.opam/log/
+
addons:
apt:
sources:
@@ -17,6 +24,7 @@ addons:
- opam
- aspcud
- gcc-multilib
+
env:
global:
- NJOBS=2
@@ -55,9 +63,8 @@ matrix:
allow_failures:
- env: TEST_TARGET="ci-geocoq"
- # Full Coq test-suite with two compilers
- # [TODO: use yaml refs and avoid duplication for packages list]
include:
+ # Full Coq test-suite with two compilers
- env:
- TEST_TARGET="test-suite"
- EXTRA_CONF="-coqide opt -with-doc yes"
@@ -81,6 +88,7 @@ matrix:
- ghostscript
- transfig
- imagemagick
+
- env:
- TEST_TARGET="test-suite"
- COMPILER="4.04.1"
@@ -92,6 +100,8 @@ matrix:
sources:
- avsm
packages: *extra-packages
+
+ # Ocaml warnings with two compilers
- env:
- TEST_TARGET="coqocaml"
- EXTRA_CONF="-coqide opt -warn-error"
@@ -107,6 +117,7 @@ matrix:
- aspcud
- libgtk2.0-dev
- libgtksourceview2.0-dev
+
- env:
- TEST_TARGET="coqocaml"
- COMPILER="4.04.1"