.travis.yml

# IF YOU MODIFY THIS FILE to add or remove "make" targets,
# please also modify the travis: target in the Makefile.
# They're not automatically coordinated, the reason being that
# we want to split the Travis build into multiple jobs.

dist: trusty
sudo: required
language: ocaml
cache:
  apt: true
  directories:
  - $HOME/.opam
  - build/compcert
  - build/sepcomp
  - build/msl
  - build/veric
  - build/floyd
  - build_beta/compcert
  - build_beta/sepcomp
  - build_beta/msl
  - build_beta/veric
  - build_beta/floyd
addons:
  apt:
    sources:
    - avsm
    packages:
    - opam
    - aspcud
env:
  global:
  - NJOBS=2
  - COMPILER="4.07.1"
  - COQ_VERSION="8.12.2"
  - NEXT_VERSION="8.12.2"
  - COMPCERT_VERSION="3.8"

branches:
  only:
  - master
notifications:
  email:
    recipients:
    - vst-push@lists.cs.princeton.edu
git:
  depth: 3
  submodules: false
  
# Use sed to replace the SSH URL with the public URL, then initialize submodules
before_install:
    - sed -i 's/git@github.com:/https:\/\/github.com\//' .gitmodules
    - git submodule update --init --recursive

install:
- opam --version
- "[ -e .opam ] || opam init -j ${NJOBS} -n -y --compiler=${COMPILER}"
- opam switch list
- eval $(opam config env)
- opam config list
- opam config var root
- opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev || true
- opam repo add coq-released https://coq.inria.fr/opam/released
- opam repo add --yes prerelease file://$(pwd)/opam-prerelease
- opam update
- opam update prerelease
- opam repo list
- opam show coq
- opam show coq-compcert
- opam show coq-compcert-32
- travis_wait 15 opam install -j ${NJOBS} -y coq=${COQ_VERSION} ${EXTRA_OPAM}
- opam install -j ${NJOBS} -y coq=${COQ_VERSION} coq-ext-lib coq-flocq
- travis_wait 15 opam install -j ${NJOBS} -y coq-compcert=${COMPCERT_VERSION}
- travis_wait 15 opam install -j ${NJOBS} -y coq-compcert-32=${COMPCERT_VERSION}
- opam list
- file `which coqc`
# - WC=`which coqc`
# - ls -l `dirname ${WC}`

stages:
  - setup
  - test

script: echo "No script"

jobs:
 include:
  - stage: setup
    name: "Floyd 32-bit"
    script: ./.travis-script floyd
    env: BITSIZE=32
  - stage: setup
    name: "Floyd 64-bit"
    script: ./.travis-script floyd
    env: BITSIZE=64
  - stage: test
    name: "Progs 32-bit"
    script: ./.travis-script progs
    env: BITSIZE=32
  - stage: test
    name: "Progs 64-bit"
    script: ./.travis-script progs64
    env: BITSIZE=64
  - stage: test
    name: "SHA-HMAC 32-bit"
    script: ./.travis-script sha-hmac
    env: BITSIZE=32
  - stage: test
    name: "Mailbox 32-bit"
    script: ./.travis-script mailbox
    env: BITSIZE=32
  - stage: test
    name: "VSUpile 32-bit"
    script: ./.travis-script VSUpile
    env: BITSIZE=32
#    script:
#    - echo 'Building VST (Coq beta)...' && echo -en 'travis_fold:start:VST.build_beta\\r'
#    - opam switch create coq_beta ocaml-base-compiler.4.07.1 || true
#    - opam switch coq_beta
#    - eval $(opam config env)
#    - opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev || true
#    - opam update
#    - opam install -j ${NJOBS} -y coq=${NEXT_VERSION} ${EXTRA_OPAM}
#    - git show --format='COMMIT %H %ci' -s; coqc -v
#    - mkdir -p build_beta
#    - for i in `ls -a | grep -Ev '^(build_beta|\.\.?)$'`; do rsync -rc $i build_beta; done
#    - cd build_beta; make -j ${NJOBS} TIMINGS=simple IGNORECOQVERSION=true floyd calibrate
#    - echo -en 'travis_fold:end:VST.build_beta\\r'
#    env: BITSIZE=32