dist: trusty # Travis builds are slower using sudo: false (the container-based # infrastructure) as of March 2017; see # https://github.com/coq/coq/pull/467 for some discussion. sudo: required # Until Ocaml becomes a language, we set a known one. language: c cache: apt: true directories: - $HOME/.opam before_cache: - rm -rf ~/.opam/log/ addons: apt: sources: - avsm packages: - opam - aspcud - gcc-multilib env: global: - NJOBS=2 # system is == 4.02.3 - COMPILER="system" - COMPILER_BE="4.06.0" - CAMLP5_VER="6.14" - CAMLP5_VER_BE="7.03" - FINDLIB_VER="1.4.1" - FINDLIB_VER_BE="1.7.3" - LABLGTK="lablgtk.2.16.0 lablgtk-extras.1.5" - 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}" - TEST_TARGET="ci-bignums TIMED=1" - TEST_TARGET="ci-color TIMED=1" - TEST_TARGET="ci-compcert TIMED=1" - TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph" - TEST_TARGET="ci-coquelicot TIMED=1" - TEST_TARGET="ci-equations TIMED=1" - TEST_TARGET="ci-geocoq TIMED=1" - TEST_TARGET="ci-fiat-crypto TIMED=1" - TEST_TARGET="ci-fiat-parsers TIMED=1" - TEST_TARGET="ci-flocq TIMED=1" - TEST_TARGET="ci-formal-topology TIMED=1" - TEST_TARGET="ci-hott TIMED=1" - TEST_TARGET="ci-iris-lambda-rust TIMED=1" - TEST_TARGET="ci-ltac2 TIMED=1" - TEST_TARGET="ci-math-classes TIMED=1" - TEST_TARGET="ci-math-comp TIMED=1" - TEST_TARGET="ci-sf TIMED=1" - TEST_TARGET="ci-unimath TIMED=1" - TEST_TARGET="ci-vst TIMED=1" # Not ready yet for 8.7 # - TEST_TARGET="ci-cpdt TIMED=1" # - TEST_TARGET="ci-metacoq TIMED=1" # - TEST_TARGET="ci-tlc TIMED=1" matrix: include: - env: - TEST_TARGET="lint" install: [] before_script: [] addons: apt: sources: [] packages: [] script: - dev/lint-repository.sh # Full Coq test-suite with two compilers - env: - TEST_TARGET="test-suite" - EXTRA_CONF="-coqide opt -with-doc yes" - EXTRA_OPAM="hevea ${LABLGTK}" addons: apt: sources: - avsm packages: &extra-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 - tipa - 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}" addons: apt: sources: - avsm packages: *extra-packages # Full test-suite with flambda - 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}" addons: apt: sources: - avsm packages: *extra-packages # Ocaml warnings with two compilers - env: - MAIN_TARGET="coqocaml" - EXTRA_CONF="-byte-only -coqide byte -warn-error" - EXTRA_OPAM="hevea ${LABLGTK}" # dummy target - BUILD_TARGET="clean" addons: apt: sources: - avsm packages: &coqide-packages - opam - aspcud - libgtk2.0-dev - libgtksourceview2.0-dev - 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" - EXTRA_OPAM="num hevea ${LABLGTK_BE}" # dummy target - BUILD_TARGET="clean" addons: apt: sources: - avsm packages: *coqide-packages - os: osx env: - TEST_TARGET="test-suite" - COMPILER="4.02.3" - CAMLP5_VER="6.17" - NATIVE_COMP="no" - COQ_DEST="-local" before_install: - brew update - brew install opam gnu-time - if: NOT (type = pull_request) os: osx env: - TEST_TARGET="" - COMPILER="4.02.3" - CAMLP5_VER="6.17" - NATIVE_COMP="no" - COQ_DEST="-prefix ${PWD}/_install" - EXTRA_CONF="-coqide opt -warn-error" - EXTRA_OPAM="${LABLGTK}" before_install: - brew update - brew install opam gnu-time gtk+ expat gtksourceview libxml2 gdk-pixbuf python3 - pip3 install macpack before_deploy: - dev/build/osx/make-macos-dmg.sh deploy: - provider: bintray user: maximedenes file: .bintray.json key: secure: "gUvXWwWR0gicDqsKOnBfe45taToSFied6gN8tCa5IOtl6E6gFoHoPZ83ZWXQsZP50oMDFS5eji0VQAFGEbOsGrTZaD9Y9Jnu34NND78SWL1tsJ6nHO3aCAoMpB0N3+oRuF6S+9HStU6KXWqgj+GeU4vZ4TOlG01RGctJa6U3vII=" skip_cleanup: true on: all_branches: true before_install: - if [ "${TRAVIS_PULL_REQUEST}" != "false" ]; then echo "Tested commit (followed by parent commits):"; git log -1; for commit in `git log -1 --format="%P"`; do echo; git log -1 $commit; done; fi install: - opam init -j ${NJOBS} --compiler=${COMPILER} -n -y - eval $(opam config env) - opam config list - opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind.${FINDLIB_VER} ${EXTRA_OPAM} - opam list script: - set -e - 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' - echo 'Building Coq...' && echo -en 'travis_fold:start:coq.build\\r' - make -j ${NJOBS} ${MAIN_TARGET} - echo -en 'travis_fold:end:coq.build\\r' - echo 'Running tests...' && echo -en 'travis_fold:start:coq.test\\r' - if [ -n "${TEST_TARGET}" ]; then ${TW} make -j ${NJOBS} ${TEST_TARGET}; fi - echo -en 'travis_fold:end:coq.test\\r' - set +e # Testing Gitter webhook notifications: webhooks: urls: - https://webhooks.gitter.im/e/3cdabdec318214c7cd63 on_success: change # options: [always|never|change] default: always on_failure: always # options: [always|never|change] default: always on_start: never # options: [always|never|change] default: always