diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-14 22:29:38 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-16 03:34:28 +0200 |
| commit | ed91bf1fce168026675f986a0069ca596ad2b806 (patch) | |
| tree | 1cfe89a725489e617fab67b3c94db68929381bd7 /.travis.yml | |
| parent | cfed57b021b89018d1bb30c6aa0957299fe35d8d (diff) | |
[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.
Diffstat (limited to '.travis.yml')
| -rw-r--r-- | .travis.yml | 21 |
1 files changed, 0 insertions, 21 deletions
diff --git a/.travis.yml b/.travis.yml index 88eed5186..25acbf726 100644 --- a/.travis.yml +++ b/.travis.yml @@ -87,39 +87,24 @@ matrix: - TEST_TARGET="ci-equations" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-geocoq" - - if: NOT (type = pull_request) - env: - TEST_TARGET="ci-fcsl-pcm" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-fiat-crypto" - - if: NOT (type = pull_request) - env: - TEST_TARGET="ci-fiat-parsers" - if: NOT (type = pull_request) env: - TEST_TARGET="ci-flocq" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-formal-topology" - - if: NOT (type = pull_request) - env: - TEST_TARGET="ci-hott" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-iris-lambda-rust" - - if: NOT (type = pull_request) - env: - TEST_TARGET="ci-ltac2" - if: NOT (type = pull_request) env: - TEST_TARGET="ci-math-classes" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-math-comp" - - if: NOT (type = pull_request) - env: - TEST_TARGET="ci-mtac2" - if: NOT (type = pull_request) env: @@ -127,12 +112,6 @@ matrix: - if: NOT (type = pull_request) env: - TEST_TARGET="ci-sf" - - if: NOT (type = pull_request) - env: - - TEST_TARGET="ci-unimath" - - if: NOT (type = pull_request) - env: - - TEST_TARGET="ci-vst" - env: - TEST_TARGET="lint" |