aboutsummaryrefslogtreecommitdiffhomepage
path: root/.travis.yml
blob: 678b4af7f425b92bf70b82b6a6cda3083c723f0b (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
dist: trusty
sudo: required
# Until Ocaml becomes a language, we set a known one.
language: c
cache:
  apt: true
  directories:
  - $HOME/.opam
addons:
  apt:
    sources:
    - avsm
    packages:
    - opam
    - aspcud
    - gcc-multilib
env:
  global:
  - NJOBS=2
  # system is == 4.02.3
  - COMPILER="system"
  # Main test suites
  matrix:
  - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit"
  - TEST_TARGET="validate"                           TW="travis_wait"
  - TEST_TARGET="validate"   COMPILER="4.02.3+32bit" TW="travis_wait"
  - TEST_TARGET="ci-color"
  - TEST_TARGET="ci-compcert"
  - TEST_TARGET="ci-coquelicot"
  - TEST_TARGET="ci-geocoq"
  - TEST_TARGET="ci-fiat-crypto"
  - TEST_TARGET="ci-fiat-parsers"
  - TEST_TARGET="ci-flocq"
  - TEST_TARGET="ci-hott"
  - TEST_TARGET="ci-iris-coq"
  - TEST_TARGET="ci-math-classes"
  - TEST_TARGET="ci-math-comp"
  - TEST_TARGET="ci-sf"
  - TEST_TARGET="ci-unimath"
  # Not ready yet for 8.7
  # - TEST_TARGET="ci-cpdt"
  # - TEST_TARGET="ci-metacoq"
  # - TEST_TARGET="ci-tlc"

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:
    - env:
      - TEST_TARGET="test-suite"
      - EXTRA_CONF="-coqide opt -with-doc yes"
      - EXTRA_OPAM="lablgtk-extras hevea"
      addons:
        apt:
          sources:
          - avsm
          packages:
          - opam
          - aspcud
          - libgtk2.0-dev
          - libgtksourceview2.0-dev
          - texlive-latex-base
          - texlive-latex-recommended
          - texlive-latex-extra
          - texlive-math-extra
          - texlive-fonts-recommended
          - texlive-fonts-extra
          - latex-xcolor
          - ghostscript
          - transfig
          - imagemagick
    - env:
      - TEST_TARGET="test-suite"
      - COMPILER="4.04.0"
      - EXTRA_CONF="-coqide opt -with-doc yes"
      - EXTRA_OPAM="lablgtk-extras hevea"
      addons:
        apt:
          sources:
          - avsm
          packages:
          - opam
          - aspcud
          - libgtk2.0-dev
          - libgtksourceview2.0-dev
          - texlive-latex-base
          - texlive-latex-recommended
          - texlive-latex-extra
          - texlive-math-extra
          - texlive-fonts-recommended
          - texlive-fonts-extra
          - latex-xcolor
          - ghostscript
          - transfig
          - imagemagick

install:
- opam init -j ${NJOBS} --compiler=${COMPILER} -n -y
- eval $(opam config env)
- opam config var root
- opam install -j ${NJOBS} -y camlp5 ocamlfind ${EXTRA_OPAM}
- opam list

script:

- echo 'Configuring Coq...' && echo -en 'travis_fold:start:coq.config\\r'
- ./configure -local -usecamlp5 -native-compiler yes ${EXTRA_CONF}
- echo -en 'travis_fold:end:coq.config\\r'

- echo 'Building Coq...' && echo -en 'travis_fold:start:coq.build\\r'
- make -j ${NJOBS}
- echo -en 'travis_fold:end:coq.build\\r'

- echo 'Running tests...' && echo -en 'travis_fold:start:coq.test\\r'
- ${TW} make -j ${NJOBS} ${TEST_TARGET}
- echo -en 'travis_fold:end:coq.test\\r'