[ci] Add travis setup, docker-based.

Pretty straightforward; need to be enabled in the Travis console tho.

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'