diff options
Diffstat (limited to '.travis.yml')
| -rw-r--r-- | .travis.yml | 88 |
1 files changed, 44 insertions, 44 deletions
diff --git a/.travis.yml b/.travis.yml index 41814e954..86a2aea66 100644 --- a/.travis.yml +++ b/.travis.yml @@ -39,35 +39,41 @@ env: - NJOBS=2 # system is == 4.02.3 - COMPILER="system" - - COMPILER_BE="4.06.0" + - COMPILER_BE="4.06.1" - CAMLP5_VER=".6.14" - - CAMLP5_VER_BE=".7.03" + - CAMLP5_VER_BE=".7.05" - FINDLIB_VER=".1.4.1" - - FINDLIB_VER_BE=".1.7.3" + - FINDLIB_VER_BE=".1.8.0" - LABLGTK="lablgtk.2.18.3 lablgtk-extras.1.6" - LABLGTK_BE="lablgtk.2.18.6 lablgtk-extras.1.6" - 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" EXTRA_OPAM="num" FINDLIB_VER="${FINDLIB_VER_BE}" matrix: include: - if: NOT (type = pull_request) env: + - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit" EXTRA_OPAM="ounit" + - 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: - TEST_TARGET="ci-color" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-compcert" + - TEST_TARGET="ci-compcert" EXTRA_OPAM="menhir" - if: NOT (type = pull_request) env: - TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph" @@ -76,18 +82,15 @@ matrix: - TEST_TARGET="ci-coquelicot" - if: NOT (type = pull_request) env: + - TEST_TARGET="ci-elpi" EXTRA_OPAM="elpi" # ppx_tools_versioned requires a specific version findlib - FINDLIB_VER="" - - TEST_TARGET="ci-elpi" EXTRA_OPAM="ppx_tools_versioned ppx_deriving ocaml-migrate-parsetree" - if: NOT (type = pull_request) env: - TEST_TARGET="ci-equations" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-geocoq" - - if: NOT (type = pull_request) - env: - - TEST_TARGET="ci-fiat-crypto" + - TEST_TARGET="ci-fcsl-pcm" - if: NOT (type = pull_request) env: - TEST_TARGET="ci-fiat-parsers" @@ -96,31 +99,22 @@ matrix: - 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" + - TEST_TARGET="ci-mtac2" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-sf" - - if: NOT (type = pull_request) - env: - - TEST_TARGET="ci-unimath" + - TEST_TARGET="ci-pidetop" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-vst" + - TEST_TARGET="ci-sf" - env: - TEST_TARGET="lint" @@ -134,10 +128,11 @@ 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="hevea ${LABLGTK}" + - EXTRA_OPAM="${LABLGTK} ounit" before_install: &sphinx-install - sudo pip3 install bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex addons: @@ -157,20 +152,19 @@ matrix: - texlive-fonts-extra - latex-xcolor - ghostscript - - transfig - - imagemagick - tipa - python3 - python3-pip - python3-setuptools - - env: + - if: NOT (type = pull_request) + env: - TEST_TARGET="test-suite" - COMPILER="${COMPILER_BE}" - FINDLIB_VER="${FINDLIB_VER_BE}" - CAMLP5_VER="${CAMLP5_VER_BE}" - EXTRA_CONF="-coqide opt -with-doc yes" - - EXTRA_OPAM="num hevea ${LABLGTK_BE}" + - EXTRA_OPAM="${LABLGTK_BE} ounit" before_install: *sphinx-install addons: apt: @@ -179,14 +173,15 @@ 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}" - CAMLP5_VER="${CAMLP5_VER_BE}" - NATIVE_COMP="no" - EXTRA_CONF="-coqide opt -with-doc yes -flambda-opts -O3" - - EXTRA_OPAM="num hevea ${LABLGTK_BE}" + - EXTRA_OPAM="${LABLGTK_BE} ounit" before_install: *sphinx-install addons: apt: @@ -195,12 +190,11 @@ 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="hevea ${LABLGTK}" - # dummy target - - BUILD_TARGET="clean" + - EXTRA_OPAM="${LABLGTK}" addons: apt: sources: @@ -211,15 +205,14 @@ 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}" - CAMLP5_VER="${CAMLP5_VER_BE}" - EXTRA_CONF="-byte-only -coqide byte -warn-error yes" - - EXTRA_OPAM="num hevea ${LABLGTK_BE}" - # dummy target - - BUILD_TARGET="clean" + - EXTRA_OPAM="${LABLGTK_BE}" addons: apt: sources: @@ -233,8 +226,10 @@ matrix: - CAMLP5_VER=".6.17" - NATIVE_COMP="no" - COQ_DEST="-local" + - EXTRA_OPAM="ounit" before_install: - brew update + - brew unlink python - brew install opam gnu-time - if: NOT (type = pull_request) @@ -274,14 +269,19 @@ install: - if [ "${TRAVIS_OS_NAME}" == "linux" ]; then travis_retry ./dev/tools/sudo-apt-get-update.sh -q; fi - if [ "${TRAVIS_OS_NAME}" == "linux" ]; then sudo apt-get install -y opam aspcud gcc-multilib; fi - opam init -j ${NJOBS} --compiler=${COMPILER} -n -y +- opam switch "$COMPILER" && opam update - eval $(opam config env) - opam config list -- opam install -j ${NJOBS} -y camlp5${CAMLP5_VER} ocamlfind${FINDLIB_VER} ${EXTRA_OPAM} +- opam install -j ${NJOBS} -y num ocamlfind${FINDLIB_VER} jbuilder camlp5${CAMLP5_VER} ${EXTRA_OPAM} - opam list script: - set -e +- echo 'Testing make clean...' && echo -en 'travis_fold:start:coq.clean\\r' +- make clean # ensure that `make clean` works on a fresh clone +- echo -en 'travis_fold:end:coq.clean\\r' + - echo 'Configuring Coq...' && echo -en 'travis_fold:start:coq.config\\r' - ./configure ${COQ_DEST} -native-compiler ${NATIVE_COMP} ${EXTRA_CONF} - echo -en 'travis_fold:end:coq.config\\r' |