.travis.yml

# This is the simple Travis configuration, which is intended for use
# on applications which do not require cross-platform and
# multiple-GHC-version support. For more information and other
# options, see:
#
# https://docs.haskellstack.org/en/stable/travis_ci/
#
# Copy these contents into the root directory of your Github project in a file
# named .travis.yml

# Use new container infrastructure to enable caching
sudo: false

# Do not choose a language; we provide our own build tools.
language: generic

# Travis slack notification
notifications:
  slack:
    on_success: change
    on_failure: always
    template:
     - "Commit (<%{compare_url}|%{commit}>) on %{branch} by %{author} <%{build_url}|%{result}>"
     - "%{commit_subject}"
    rooms:
     - secure: B38DsPEJPcxRoTwDS4JHks2bi+ViZkTwI6sB/5R+xKXSz4ZEU9chrQ15mXS/NVwdEaQZLNjuIKdxj1LgKAr9gelXZMDLS9lv/bzajx6SRq8x6MZxlYcd7e5ej+xZSmo8R+2ivMLB23iSBtZDi98aTulplbmXb2Qdh5WznShrGRftdtyO7Aqf5xZOy3Q3+0ji7qAXQpWB4sDLJr4Iu2Fjkvj5fBkq9dLHmkK08AR1xyo3kswNx4pssPbfiAiuk3zJY9h+iPGOCj8F3rfVlGdVOGXnF6Qa12rmEVmxCoQ66JNf97ESAp92+lqB84bpNuxLdfn+XZZLQOLZCIRZxm/noJYlQgYs9LPUA5RZ014ryR2B+ThiX/Cgod6toNDVN/vl/lg9QqyQoo+jZbloy/Ot3Z74eFNaVY8vDUkuPpkdSo7bkKDdzQcojmjLXKCT47hnIImD5AclzAv5WnYJd+387XEf2nD3F2RBwi++m2smE+CI66GZ0rizRZKMHIzWUJoEunQY2xRnFqo0XU+jYz50guIdu7h6X5sw2TfilbWLPigaWM03JYwbp4hrB4hqbkEeYaDA4ygqnyePo7oMQMmv57fwwcpvYN2yO6kgun0npSmBg0sWYFkrwQsxT3sI9mTljbhgXtuk0SRDOdXrOvlK1/fRqiq76o6RZ16cE8JN7eQ=

# Caching so the next build will be fast too
cache:
  directories:
  - $HOME/.stack
  - $HOME/ghc
  - $HOME/.opam
  - $HOME/unitb/hs-to-coq/lean/_target

# Ensure necessary system libraries are present
addons:
   apt:
    sources:
      - avsm
    packages:
      - opam
      - libgmp-dev
      - xutils-dev

before_install:
 # Download and unpack the stack executable
 - mkdir -p ~/.local/bin
 - export PATH=$HOME/.local/bin:$PATH
 - travis_retry curl -L https://www.stackage.org/stack/linux-x86_64 | tar xz --wildcards --strip-components=1 -C ~/.local/bin '*/stack'
 # Skip this for now, I can't seem to get this to work with the caching
 # Get GHC
 # - mkdir -p ~/ghc
 # - '[[ -n $(find ~/ghc -prune -empty) ]] && (cd ~/ghc; travis_retry curl https://codeload.github.com/ghc/ghc/tar.gz/ghc-8.0.2-release | tar xz --strip-components 1)'
 # Install COQ
 - opam config env
 - if ! [ -e $HOME/.opam/config ]; then opam init -j 2 --compiler=system -n -y; fi
 - $HOME/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true
 - opam repo add coq-released http://coq.inria.fr/opam/released || true
 - opam list -i coq.8.7.2 || { opam update && opam unpin coq && opam install -v -y -j 1  coq.8.7.2 ocamlfind.1.7.3-1 ; }

install:
 # Build dependencies
 - stack --no-terminal --install-ghc test --only-dependencies
 # dependencies of the containers code that we translate
 - stack --no-terminal --install-ghc install QuickCheck HUnit test-framework test-framework-hunit test-framework-quickcheck2
 -  wget -c https://github.com/leanprover/lean-nightly/releases/download/nightly-2018-04-02/lean-3.3.1-nightly-2018-04-02-linux.tar.gz -O - | tar xz -C $HOME
 - export PATH=$HOME/lean-3.3.1-nightly-2018-04-02-linux/bin:$PATH

jobs:
  include:
    - stage: setup ghc
      script: True
    - stage: setup Lean
      script:
      - cd lean
      - leanpkg configure
      - lean --make _target/deps/mathlib

    - stage: setup Coq
      script:
        - opam list -i coq-mathcomp-ssreflect || opam install -y coq-mathcomp-ssreflect
        - eval $(opam config env)
    - stage: test
      script:
        - stack --no-terminal --install-ghc install
        # Run test suite
        - make -C examples/tests
        # Build Coq’ified base (generated sources are in the repo)
        - make -C base
        # Build base theory
        - make -C base-thy
        # Run examples that use base:
        - make -C examples/base-tests
        - make -C examples/successors
        - make -C examples/compiler
        - make -C examples/rle
        - make -C examples/bag
        - make -C examples/quicksort
        - make -C examples/dlist
        - make -C examples/intervals
        - make -C examples/containers clean
        - make -C examples/containers
        - make -C examples/containers/theories
        - make -C examples/transformers
        - make -C examples/coinduction

        # Test extraction
        - make -C examples/containers/extraction/src
        - ( cd examples/containers/extraction ; stack --no-terminal --install-ghc test)
        - ( cd examples/containers/extraction ; stack --no-terminal --install-ghc bench)

        # disabled 2018-07-24 due to too big of a fall-out, and the
        # focus is somewhere on containers right now
        #- make -C examples/ghc/lib

        # This requires a configured check-out of GHC, so lets not do that on travis
        # - make -C examples/ghc