.travis.yml

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.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.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="ci-bignums"
    - if: NOT (type = pull_request)
      env:
      - TEST_TARGET="ci-color"
    - if: NOT (type = pull_request)
      env:
      - TEST_TARGET="ci-compcert"
    - 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-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"
    - 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-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"
      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
      osx_image: xcode7.3
      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:
- 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
- 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