diff options
Diffstat (limited to '.travis.yml')
| -rw-r--r-- | .travis.yml | 235 |
1 files changed, 235 insertions, 0 deletions
diff --git a/.travis.yml b/.travis.yml new file mode 100644 index 00000000..f20599ed --- /dev/null +++ b/.travis.yml @@ -0,0 +1,235 @@ +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 +## Due to issues like +## https://github.com/travis-ci/travis-ci/issues/8507 , +## https://github.com/travis-ci/travis-ci/issues/9000 , +## https://github.com/travis-ci/travis-ci/issues/9081 , and +## https://github.com/travis-ci/travis-ci/issues/9126 , we get frequent +## failures with using `packages`. Therefore, for most targets, we +## instead invoke `apt-get update` manually with `travis_retry` before +## invoking `apt-get install`, manually, below in the `install:` +## target. +# packages: +# - opam +# - aspcud +# - gcc-multilib + +env: + global: + - NJOBS=2 + # system is == 4.02.3 + - COMPILER="system" + - COMPILER_BE="4.07.0" + - DUNE_VER=".1.0.0" + - CAMLP5_VER=".6.14" + - CAMLP5_VER_BE=".7.06" + - FINDLIB_VER=".1.4.1" + - FINDLIB_VER_BE=".1.8.0" + - LABLGTK="lablgtk.2.18.3 conf-gtksourceview.2" + - LABLGTK_BE="lablgtk.2.18.6 conf-gtksourceview.2" + - NATIVE_COMP="yes" + - COQ_DEST="-local" + - MAIN_TARGET="world" + +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}" EXTRA_CONF="-flambda-opts -O3" FINDLIB_VER="${FINDLIB_VER_BE}" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="ci-coquelicot" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="ci-equations" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="ci-flocq" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="ci-hott" + - if: NOT (type = pull_request) + env: + - TEST_TARGET="ci-ltac2" + + - env: + - TEST_TARGET="lint" + install: [] + before_script: [] + addons: + apt: + sources: [] + packages: [] + script: + - dev/lint-repository.sh + + # Full Coq test-suite with two compilers + - if: NOT (type = pull_request) + env: + - TEST_TARGET="sphinx test-suite" + - EXTRA_CONF="-coqide opt" + - EXTRA_OPAM="hevea ${LABLGTK}" + before_install: &sphinx-install + - sudo pip3 install bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex + addons: + apt: + sources: + - avsm + packages: &extra-packages + - opam + - aspcud + - libgtk2.0-dev + - libgtksourceview2.0-dev + - python3 + - python3-pip + - python3-setuptools + + - if: NOT (type = pull_request) + env: + - TEST_TARGET="sphinx test-suite" + - COMPILER="${COMPILER_BE}" + - FINDLIB_VER="${FINDLIB_VER_BE}" + - CAMLP5_VER="${CAMLP5_VER_BE}" + - EXTRA_CONF="-coqide opt" + - EXTRA_OPAM="hevea ${LABLGTK_BE}" + before_install: *sphinx-install + addons: + apt: + sources: + - avsm + packages: *extra-packages + + # Full test-suite with flambda + - if: NOT (type = pull_request) + env: + - TEST_TARGET="sphinx test-suite" + - COMPILER="${COMPILER_BE}+flambda" + - FINDLIB_VER="${FINDLIB_VER_BE}" + - CAMLP5_VER="${CAMLP5_VER_BE}" + - EXTRA_CONF="-coqide opt -flambda-opts -O3" + - EXTRA_OPAM="hevea ${LABLGTK_BE}" + before_install: *sphinx-install + addons: + apt: + sources: + - avsm + packages: *extra-packages + + - os: osx + env: + - TEST_TARGET="test-suite" + - COMPILER="${COMPILER_BE}" + - FINDLIB_VER="${FINDLIB_VER_BE}" + - CAMLP5_VER="${CAMLP5_VER_BE}" + - NATIVE_COMP="no" + - COQ_DEST="-local" + before_install: + - brew update + - brew unlink python + - brew install gnu-time + # only way to continue using OPAM 1.2 + - brew install https://raw.githubusercontent.com/Homebrew/homebrew-core/d156edeeed7291f4bc1e08620b331bbd05d52b78/Formula/opam.rb + + - if: NOT (type = pull_request) + os: osx + osx_image: xcode7.3 + env: + - TEST_TARGET="" + - COMPILER="${COMPILER_BE}" + - FINDLIB_VER="${FINDLIB_VER_BE}" + - CAMLP5_VER="${CAMLP5_VER_BE}" + - NATIVE_COMP="no" + - COQ_DEST="-prefix ${PWD}/_install" + - EXTRA_CONF="-coqide opt -warn-error yes" + - EXTRA_OPAM="${LABLGTK_BE}" + before_install: + - brew update + - brew unlink python + - brew install gnu-time gtk+ expat gtksourceview gdk-pixbuf + # only way to continue using OPAM 1.2 + - brew install https://raw.githubusercontent.com/Homebrew/homebrew-core/d156edeeed7291f4bc1e08620b331bbd05d52b78/Formula/opam.rb + - brew unlink python@2 + - brew install 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: +- 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 --allow-unauthenticated; 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 num ocamlfind${FINDLIB_VER} camlp5${CAMLP5_VER} ${EXTRA_OPAM} +- opam list + +script: + +- set -e +- echo 'Configuring Coq...' && echo -en 'travis_fold:start:coq.config\\r' +- ./configure ${COQ_DEST} -warn-error yes -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 |