diff options
| author | Maxime Dénès | 2017-10-25 10:06:14 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-25 10:06:14 +0200 |
| commit | cda35d8c660d32de0ba4e9a4f30aae2d04d78d20 (patch) | |
| tree | 80556659ca5dfc4c5623d80c14a089c8fd09249b | |
| parent | 0897d0f642c19419c513f9609782436bebf28f5b (diff) | |
| parent | 16681ac2e3669d1c9ca3f4bb86c88820d697427b (diff) | |
Merge PR #5971: [travis] Add flambda testing.
| -rw-r--r-- | .travis.yml | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/.travis.yml b/.travis.yml index 196f4b22ad..c818b95212 100644 --- a/.travis.yml +++ b/.travis.yml @@ -39,6 +39,7 @@ env: - 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="4.05.0+flambda" CAMLP5_VER="7.01" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" NATIVE_COMP="no" - TEST_TARGET="ci-bignums TIMED=1" - TEST_TARGET="ci-color TIMED=1" - TEST_TARGET="ci-compcert TIMED=1" @@ -103,6 +104,21 @@ matrix: - avsm packages: *extra-packages + # Full test-suite with flambda + - env: + - TEST_TARGET="test-suite" + - COMPILER="4.05.0+flambda" + - FINDLIB_VER="1.7.3" + - CAMLP5_VER="7.01" + - NATIVE_COMP="no" + - EXTRA_CONF="-coqide opt -with-doc yes -flambda-opts -O3" + - EXTRA_OPAM="lablgtk-extras hevea" + addons: + apt: + sources: + - avsm + packages: *extra-packages + # Ocaml warnings with two compilers - env: - TEST_TARGET="coqocaml" |