.travis.yml

language: generic

sudo: false

addons:
  apt:
    sources:
    - avsm
    packages:
    - opam
    - ocaml
    - texlive-latex-base
    - texlive-latex-extra
    - pgf
    - texlive-pictures
    - libc6-dev-i386
    - gcc-multilib
    - linux-libc-dev:i386
    - python3

env:
  global:
  - INSTALL_DIR: $HOME/.local
  - ISABELLE_VERSION: Isabelle2016
  - ISABELLE_TARBALL: ${ISABELLE_VERSION}_app.tar.gz
  - ISABELLE_URL: http://isabelle.in.tum.de/dist/${ISABELLE_TARBALL}
  - ISABELLE_DIR: ${INSTALL_DIR}/${ISABELLE_VERSION}
  - ISABELLE: ${ISABELLE_DIR}/bin/isabelle
  - ISABELLE_USER_SETTINGS: ${HOME}/.isabelle/${ISABELLE_VERSION}/etc/settings
  - AFP_BRANCH: afp-2016
  - AFP_REPO: https://bitbucket.org/isa-afp/${AFP_BRANCH}
  - AFP_DIR: ${INSTALL_DIR}/${AFP_BRANCH}
  - OPAM_DIR: ${HOME}/.opam
  - OPAM_INIT: ${OPAM_DIR}/opam-init/init.sh

cache:
  directories:
  - ${HOME}/.isabelle
  - ${OPAM_DIR}
  - ${TRAVIS_BUILD_DIR}/compcertSSA

before_install:
  - test -e ${OPAM_INIT} || opam init -y
  - . ${OPAM_INIT}
  - which coqc || travis_wait opam install -y coq.8.4.5
  - test -d ${INSTALL_DIR} || mkdir -p ${INSTALL_DIR}
  - test -e $ISABELLE || { wget ${ISABELLE_URL} && tar -C ${INSTALL_DIR}/ -xzf ${ISABELLE_TARBALL}; }
  - test -d ${AFP_DIR} || (cd ${INSTALL_DIR}; hg clone ${AFP_REPO})
  - (cd ${AFP_DIR}; hg pull -u)

install:
  - test -e ${ISABELLE_USER_SETTINGS} || { mkdir -p $(dirname ${ISABELLE_USER_SETTINGS}) && touch ${ISABELLE_USER_SETTINGS}; }
  - grep init_component ${ISABELLE_USER_SETTINGS} || echo 'init_component "${AFP_DIR}"' >> ${ISABELLE_USER_SETTINGS}
  - grep ISABELLE_BUILD_OPTIONS ${ISABELLE_USER_SETTINGS} || echo 'ISABELLE_BUILD_OPTIONS="threads=1"' >> ${ISABELLE_USER_SETTINGS}
  - grep ML_OPTIONS ${ISABELLE_USER_SETTINGS} || echo 'ML_OPTIONS="-H 500"' >> ${ISABELLE_USER_SETTINGS}

script:
  - make ccomp ISABELLE=${ISABELLE}
  - (set -o pipefail; make -C compcertSSA/test/spass ssa | ./measure.py)

before_cache:
  - rm -f `$ISABELLE getenv -b ISABELLE_HOME_USER`/heaps/`$ISABELLE getenv -b ML_IDENTIFIER`/FormalSSA*
  - rm -f `$ISABELLE getenv -b ISABELLE_HOME_USER`/heaps/`$ISABELLE getenv -b ML_IDENTIFIER`/log/FormalSSA*
  - rm -f `$ISABELLE getenv -b ISABELLE_HOME_USER`/heaps/`$ISABELLE getenv -b ML_IDENTIFIER`/log/compcertSSA.gz
  - find ${TRAVIS_BUILD_DIR}/compcertSSA -name "*.vo" > /tmp/cccf
  - find ${TRAVIS_BUILD_DIR}/compcertSSA -name "*.vp" | sed -e "s/\.vp/\.v/g" >> /tmp/cccf
  - find ${TRAVIS_BUILD_DIR}/compcertSSA -name "ndfun*" >> /tmp/cccf
  - sort /tmp/cccf > /tmp/cccf.sorted
  - find ${TRAVIS_BUILD_DIR}/compcertSSA -type f -o -type l | sort > /tmp/cc.all
  - comm -23 /tmp/cc.all /tmp/cccf.sorted | xargs rm
  - rm -r `find ${TRAVIS_BUILD_DIR}/compcertSSA -type d -empty`