diff options
Diffstat (limited to '.travis.yml')
| -rw-r--r-- | .travis.yml | 54 |
1 files changed, 22 insertions, 32 deletions
diff --git a/.travis.yml b/.travis.yml index 88eed5186..23b6f7f60 100644 --- a/.travis.yml +++ b/.travis.yml @@ -49,18 +49,24 @@ env: - NATIVE_COMP="yes" - COQ_DEST="-local" - MAIN_TARGET="world" - # 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="validate" COMPILER="${COMPILER_BE}+flambda" CAMLP5_VER="${CAMLP5_VER_BE}" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" FINDLIB_VER="${FINDLIB_VER_BE}" matrix: include: - if: NOT (type = pull_request) env: + - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="validate" TW="travis_wait" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="validate" COMPILER="4.02.3+32bit" TW="travis_wait" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="validate" COMPILER="${COMPILER_BE}+flambda" CAMLP5_VER="${CAMLP5_VER_BE}" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" FINDLIB_VER="${FINDLIB_VER_BE}" + - if: NOT (type = pull_request) + env: - TEST_TARGET="ci-bignums" - if: NOT (type = pull_request) env: @@ -87,39 +93,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 +118,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" @@ -146,7 +131,8 @@ matrix: - dev/lint-repository.sh # Full Coq test-suite with two compilers - - env: + - if: NOT (type = pull_request) + env: - TEST_TARGET="test-suite" - EXTRA_CONF="-coqide opt -with-doc yes" - EXTRA_OPAM="${LABLGTK}" @@ -174,7 +160,8 @@ matrix: - python3-pip - python3-setuptools - - env: + - if: NOT (type = pull_request) + env: - TEST_TARGET="test-suite" - COMPILER="${COMPILER_BE}" - FINDLIB_VER="${FINDLIB_VER_BE}" @@ -189,7 +176,8 @@ matrix: packages: *extra-packages # Full test-suite with flambda - - env: + - if: NOT (type = pull_request) + env: - TEST_TARGET="test-suite" - COMPILER="${COMPILER_BE}+flambda" - FINDLIB_VER="${FINDLIB_VER_BE}" @@ -205,7 +193,8 @@ matrix: packages: *extra-packages # Ocaml warnings with two compilers - - env: + - if: NOT (type = pull_request) + env: - MAIN_TARGET="coqocaml" - EXTRA_CONF="-byte-only -coqide byte -warn-error yes" - EXTRA_OPAM="${LABLGTK}" @@ -219,7 +208,8 @@ matrix: - libgtk2.0-dev - libgtksourceview2.0-dev - - env: + - if: NOT (type = pull_request) + env: - MAIN_TARGET="coqocaml" - COMPILER="${COMPILER_BE}" - FINDLIB_VER="${FINDLIB_VER_BE}" |