diff options
| -rw-r--r-- | .travis.yml | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/.travis.yml b/.travis.yml new file mode 100644 index 0000000000..d52b3ebd25 --- /dev/null +++ b/.travis.yml @@ -0,0 +1,39 @@ +dist: trusty +sudo: required +language: generic + +services: + - docker + +env: + global: + - NJOBS="2" + - CONTRIB_NAME="ltac2" + matrix: + - COQ_IMAGE="coqorg/coq:dev" + +install: | + # Prepare the COQ container + docker run -d -i --init --name=COQ -v ${TRAVIS_BUILD_DIR}:/home/coq/${CONTRIB_NAME} -w /home/coq/${CONTRIB_NAME} ${COQ_IMAGE} + docker exec COQ /bin/bash --login -c " + # This bash script is double-quoted to interpolate Travis CI env vars: + echo \"Build triggered by ${TRAVIS_EVENT_TYPE}\" + export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m ' + set -ex # -e = exit on failure; -x = trace for debug + # opam update -y + # opam install -y -j ${NJOBS} coq-mathcomp-ssreflect + opam config list + opam repo list + opam list + " +script: +- echo -e "${ANSI_YELLOW}Building ${CONTRIB_NAME}...${ANSI_RESET}" && echo -en 'travis_fold:start:script\\r' +- | + docker exec COQ /bin/bash --login -c " + export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m ' + set -ex + sudo chown -R coq:coq /home/coq/${CONTRIB_NAME} + make + " +- docker stop COQ # optional +- echo -en 'travis_fold:end:script\\r' |