Merge PR#421: [travis] Perform parallel testing

19 files changed, 385 insertions, 19 deletions

diff --git a/.travis.yml b/.travis.yml
index 3e71a71570..188e446007 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -1,6 +1,7 @@
 dist: trusty
 sudo: required
-language: ocaml
+# Until Ocaml becomes a language, we set a known one.
+language: c
 cache:
   apt: true
   directories:
@@ -12,27 +13,106 @@ addons:
     packages:
     - opam
     - aspcud
-    - libgtk2.0-dev
-    - libgtksourceview2.0-dev
-    - texlive-latex-base
-    - texlive-latex-recommended
-    - texlive-latex-extra
-    - texlive-math-extra
-    - texlive-fonts-recommended
-    - texlive-fonts-extra
-    - latex-xcolor
-    - ghostscript
-    - transfig
-    - imagemagick
+    - gcc-multilib
+env:
+  global:
+  - NJOBS=2
+  # system is == 4.02.3
+  - COMPILER="system"
+  # Main test suites
+  matrix:
+  - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit"
+  - TEST_TARGET="validate"                           TW="travis_wait"
+  - TEST_TARGET="validate"   COMPILER="4.02.3+32bit" TW="travis_wait"
+  - TEST_TARGET="ci-color"
+  - TEST_TARGET="ci-compcert"
+  - TEST_TARGET="ci-coquelicot"
+  - TEST_TARGET="ci-cpdt"
+  - TEST_TARGET="ci-geocoq"
+  - TEST_TARGET="ci-fiat-crypto"
+  - TEST_TARGET="ci-flocq"
+  - TEST_TARGET="ci-hott"
+  - TEST_TARGET="ci-iris-coq"
+  - TEST_TARGET="ci-math-classes"
+  - TEST_TARGET="ci-math-comp"
+  - TEST_TARGET="ci-sf"
+  # Not ready yet for 8.7
+  # - TEST_TARGET="ci-metacoq"
+  # - TEST_TARGET="ci-tlc"
+
+matrix:
+
+  allow_failures:
+  - env: TEST_TARGET="ci-cpdt"
+
+  # Full Coq test-suite with two compilers
+  # [TODO: use yaml refs and avoid duplication for packages list]
+  include:
+    - env:
+      - TEST_TARGET="test-suite"
+      - EXTRA_CONF="-coqide opt -with-doc yes"
+      - EXTRA_OPAM="lablgtk-extras hevea"
+      addons:
+        apt:
+          sources:
+          - avsm
+          packages:
+          - opam
+          - aspcud
+          - libgtk2.0-dev
+          - libgtksourceview2.0-dev
+          - texlive-latex-base
+          - texlive-latex-recommended
+          - texlive-latex-extra
+          - texlive-math-extra
+          - texlive-fonts-recommended
+          - texlive-fonts-extra
+          - latex-xcolor
+          - ghostscript
+          - transfig
+          - imagemagick
+    - env:
+      - TEST_TARGET="test-suite"
+      - COMPILER="4.04.0"
+      - EXTRA_CONF="-coqide opt -with-doc yes"
+      - EXTRA_OPAM="lablgtk-extras hevea"
+      addons:
+        apt:
+          sources:
+          - avsm
+          packages:
+          - opam
+          - aspcud
+          - libgtk2.0-dev
+          - libgtksourceview2.0-dev
+          - texlive-latex-base
+          - texlive-latex-recommended
+          - texlive-latex-extra
+          - texlive-math-extra
+          - texlive-fonts-recommended
+          - texlive-fonts-extra
+          - latex-xcolor
+          - ghostscript
+          - transfig
+          - imagemagick
+
 install:
-- ": ${NJOBS:=1}"
-- "[ -e .opam ] || opam init -j ${NJOBS} --compiler=4.02.3 -n -y"
+- opam init -j ${NJOBS} --compiler=${COMPILER} -n -y
 - eval $(opam config env)
 - opam config var root
-- opam install -j ${NJOBS} -y camlp5 ocamlfind lablgtk-extras hevea
+- opam install -j ${NJOBS} -y camlp5 ocamlfind ${EXTRA_OPAM}
 - opam list
+
 script:
-- ./configure -local -usecamlp5 -native-compiler yes -coqide opt -with-doc yes
+
+- echo 'Configuring Coq...' && echo -en 'travis_fold:start:coq.config\\r'
+- ./configure -local -usecamlp5 -native-compiler yes ${EXTRA_CONF}
+- echo -en 'travis_fold:end:coq.config\\r'
+
+- echo 'Building Coq...' && echo -en 'travis_fold:start:coq.build\\r'
 - make -j ${NJOBS}
-- travis_wait make -j ${NJOBS} validate
-- travis_wait make -j ${NJOBS} test-suite
+- echo -en 'travis_fold:end:coq.build\\r'
+
+- echo 'Running tests...' && echo -en 'travis_fold:start:coq.test\\r'
+- ${TW} make -j ${NJOBS} ${TEST_TARGET}
+- echo -en 'travis_fold:end:coq.test\\r'
diff --git a/Makefile b/Makefile
index 0f9619c01b..e1d6e8e1d2 100644
--- a/Makefile
+++ b/Makefile
@@ -246,6 +246,11 @@ devdocclean:
 	rm -f $(OCAMLDOCDIR)/html/*.html
 
 ###########################################################################
+# Continuous Intregration Tests
+###########################################################################
+include Makefile.ci
+
+###########################################################################
 # Emacs tags
 ###########################################################################
 
diff --git a/Makefile.ci b/Makefile.ci
new file mode 100644
index 0000000000..040144e6e8
--- /dev/null
+++ b/Makefile.ci
@@ -0,0 +1,10 @@
+CI_TARGETS=ci-all ci-hott ci-math-comp ci-compcert ci-sf ci-cpdt	\
+           ci-color ci-math-classes ci-tlc ci-fiat-crypto		\
+           ci-coquelicot ci-flocq ci-iris-coq ci-metacoq ci-geocoq
+
+.PHONY: $(CI_TARGETS)
+
+# Generic rule, we use make to easy travis integraton with mixed rules
+$(CI_TARGETS): ci-%:
+	./dev/ci/ci-$*.sh
+
diff --git a/README.ci b/README.ci
new file mode 100644
index 0000000000..dcf93cf00e
--- /dev/null
+++ b/README.ci
@@ -0,0 +1,77 @@
+**WARNING:** This document is a work in progress and intended as a RFC.
+If you are not a Coq Developer, don't follow this instructions yet.
+
+Introduction
+============
+
+The Coq Travis CI infrastructure is meant to provide lightweight
+automatics testing of pull requests.
+
+More comprehensive testing is the responsability of Coq's [Jenkins CI
+server](https://ci.inria.fr/coq/) see, [XXX: add document] for
+instructions on how to add your development to Jenkins.
+
+How to submit your development for Coq Travis CI
+================================================
+
+Travis CI provides a convenient way to perform testing of Coq changes
+versus a set of curated libraries.
+
+Are you an author of a Coq library who would be interested in having
+the latest Coq changes validated against your development?
+
+If so, keep reading! Getting Coq changes tested against your library
+is easy, all that you need to do is:
+
+1.- Put you development in a public repository tracking coq trunk.
+2.- Make sure that your development builds in less than 35 minutes.
+3.- Submit a PR adding you development.
+4.- ?
+5.- Profit! Your library is now part of Coq's continous integration!
+
+Note that by partipating in this program, you assume a reasonable
+compromise to discuss and eventually integrate compatibility changes
+upstream.
+
+Get in touch with us to discuss any special need your development may
+have.
+
+Maintaining your contribution manually [current method]
+======================================
+
+To add your contribution to the Coq Travis CI set, add a script for
+building your library to `dev/ci/`, update `.travis.yml` and
+`Makefile.ci`. Then, submit a PR.
+
+Maintaining your contribution as an OPAM package [work in progress] [to be implemented]
+================================================
+
+You can also provide an opam package for your contribution XXX at
+https://github.com/coq/opam-coq-archive
+
+Then, add a `ci-opam-XXX` target to the `.travis.yml` file, the
+package XXX.dev will be tested against each Coq commit and pull
+request.
+
+- TODO: The main question here is what to do with `.opam` caching. We
+  could disable it altogether, however this will have an impact. We
+  could install a dummy Coq package, but `coq-*` dependencies will be
+  botched too. Need to think more.
+
+PR Overlays [work in progress] [to be implemented]
+===========
+
+It is common for PR to break some of the external tests. To this
+purpose, we provide a method for particular PR to overlay the
+repositories of some of the tests so they can provide fixed
+developments.
+
+The general idea is that the PR author will drop a file
+`dev/ci/overlays/$branch.overlay` where branch name is taken from
+`${TRAVIS_PULL_REQUEST_BRANCH:-$TRAVIS_BRANCH}`
+that is to say, the name of the original branch for the PR.
+
+The `.overlay` file will contain a set of variables that will be used
+to do the corresponding `opam pin` or to overload the corresponding
+git repositories, etc...
+
diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
new file mode 100755
index 0000000000..78ae7f02f9
--- /dev/null
+++ b/dev/ci/ci-color.sh
@@ -0,0 +1,8 @@
+#!/bin/bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+svn checkout https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color color
+
+( cd color && make -j ${NJOBS} )
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
new file mode 100644
index 0000000000..2a6601e045
--- /dev/null
+++ b/dev/ci/ci-common.sh
@@ -0,0 +1,6 @@
+#!/bin/bash
+
+set -xe
+
+export PATH=`pwd`/bin:$PATH
+ls `pwd`/bin
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
new file mode 100755
index 0000000000..d4023c9165
--- /dev/null
+++ b/dev/ci/ci-compcert.sh
@@ -0,0 +1,10 @@
+#!/bin/bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+opam install -j ${NJOBS} -y menhir
+git clone --depth 3 -b coq-8.6 https://github.com/maximedenes/CompCert.git
+
+# Patch to avoid the upper version limit
+( cd CompCert && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make -j ${NJOBS} )
diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh
new file mode 100755
index 0000000000..4a23e51be6
--- /dev/null
+++ b/dev/ci/ci-coquelicot.sh
@@ -0,0 +1,29 @@
+#!/bin/bash
+
+# $0 is not the safest way, but...
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+git clone --depth 3 https://github.com/math-comp/math-comp.git
+
+# coquelicot just needs mathcomp
+( cd math-comp/mathcomp && \
+  sed -i.bak '/ssrtest/d'   Make && \
+  sed -i.bak '/odd_order/d'   Make && \
+  sed -i.bak '/all\/all.v/d'  Make && \
+  sed -i.bak '/character/d'   Make && \
+  sed -i.bak '/real_closed/d' Make && \
+  sed -i.bak '/solvable/d'    Make && \
+  sed -i.bak '/field/d'       Make && \
+  sed -i.bak '/fingroup/d'    Make && \
+  sed -i.bak '/algebra/d'     Make && \
+  make -j ${NJOBS} && make install )
+
+# Setup ssr
+# echo "Add ML Path \"`pwd`/math-comp/mathcomp/\"." > ${HOME}/.coqrc
+# echo "Add LoadPath \"`pwd`/math-comp/mathcomp/\" as mathcomp." >> ${HOME}/.coqrc
+
+# Setup coquelicot
+git clone --depth 3 https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git
+
+( cd coquelicot && ./autogen.sh && ./configure && ./remake -j${NJOBS} )
diff --git a/dev/ci/ci-cpdt.sh b/dev/ci/ci-cpdt.sh
new file mode 100755
index 0000000000..18d7561804
--- /dev/null
+++ b/dev/ci/ci-cpdt.sh
@@ -0,0 +1,10 @@
+#!/bin/bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+wget http://adam.chlipala.net/cpdt/cpdt.tgz
+tar xvfz cpdt.tgz
+
+( cd cpdt && make clean && make -j ${NJOBS} )
+
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
new file mode 100755
index 0000000000..c594f83603
--- /dev/null
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -0,0 +1,12 @@
+#!/bin/bash
+
+# $0 is not the safest way, but...
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+git clone --depth 3 https://github.com/mit-plv/fiat-crypto.git
+
+( cd fiat-crypto && make -j ${NJOBS} )
+
+# ( cd corn && make -j ${NJOBS} )
+
diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh
new file mode 100755
index 0000000000..b9cf649a1a
--- /dev/null
+++ b/dev/ci/ci-flocq.sh
@@ -0,0 +1,9 @@
+#!/bin/bash
+
+# $0 is not the safest way, but...
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+git clone --depth 3 https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git
+
+( cd flocq && ./autogen.sh && ./configure && ./remake -j${NJOBS} )
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
new file mode 100755
index 0000000000..7b5811dc4a
--- /dev/null
+++ b/dev/ci/ci-geocoq.sh
@@ -0,0 +1,12 @@
+#!/bin/bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+# XXX: replace by generic template
+GeoCoq_CI_BRANCH=master
+GeoCoq_CI_GITURL=https://github.com/GeoCoq/GeoCoq.git
+
+git clone --depth 1 -b ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL}
+
+( cd GeoCoq && ./configure.sh && make -j ${NJOBS} )
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
new file mode 100755
index 0000000000..8f82ba9f21
--- /dev/null
+++ b/dev/ci/ci-hott.sh
@@ -0,0 +1,8 @@
+#!/bin/bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+git clone --depth 3 -b mz-8.6 https://github.com/ejgallego/HoTT.git
+
+( cd HoTT && ./autogen.sh && ./configure && make -j ${NJOBS} )
diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh
new file mode 100755
index 0000000000..c1306e070d
--- /dev/null
+++ b/dev/ci/ci-iris-coq.sh
@@ -0,0 +1,30 @@
+#!/bin/bash
+
+# $0 is not the safest way, but...
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+# XXX: Refactor into install-ssreflect
+git clone --depth 1 https://github.com/math-comp/math-comp.git
+
+# coquelicot just needs mathcomp
+( cd math-comp/mathcomp && \
+  sed -i.bak '/ssrtest/d'     Make && \
+  sed -i.bak '/odd_order/d'   Make && \
+  sed -i.bak '/all\/all.v/d'  Make && \
+  sed -i.bak '/character/d'   Make && \
+  sed -i.bak '/real_closed/d' Make && \
+  sed -i.bak '/solvable/d'    Make && \
+  sed -i.bak '/field/d'       Make && \
+  sed -i.bak '/fingroup/d'    Make && \
+  sed -i.bak '/algebra/d'     Make && \
+  make -j ${NJOBS} && make install )
+
+# Setup ssr = This doesn't work as coq_makefile will pass -q to coqc :S :S
+# echo "Add ML Path \"`pwd`/math-comp/mathcomp/\"." > ${HOME}/.coqrc
+# echo "Add LoadPath \"`pwd`/math-comp/mathcomp/\" as mathcomp." >> ${HOME}/.coqrc
+
+# Setup Iris
+git clone --depth 1 https://gitlab.mpi-sws.org/FP/iris-coq.git
+
+( cd iris-coq && make -j ${NJOBS} )
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
new file mode 100755
index 0000000000..9127c18951
--- /dev/null
+++ b/dev/ci/ci-math-classes.sh
@@ -0,0 +1,12 @@
+#!/bin/bash
+
+# $0 is not the safest way, but...
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+git clone --depth 1 -b v8.6 https://github.com/math-classes/math-classes.git
+( cd math-classes && make -j ${NJOBS} && make install )
+
+git clone --depth 1 -b v8.6 https://github.com/c-corn/corn.git
+( cd corn         && make -j ${NJOBS} )
+
diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh
new file mode 100755
index 0000000000..b833792419
--- /dev/null
+++ b/dev/ci/ci-math-comp.sh
@@ -0,0 +1,13 @@
+#!/bin/bash
+
+# $0 is not the safest way, but...
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+git clone --depth 3 https://github.com/math-comp/math-comp.git
+
+# odd_order takes too much time for travis.
+( cd math-comp/mathcomp                              && \
+     sed -i.bak '/PFsection/d'                  Make && \
+     sed -i.bak '/stripped_odd_order_theorem/d' Make && \
+     make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all )
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh
new file mode 100755
index 0000000000..9a9bd3648b
--- /dev/null
+++ b/dev/ci/ci-metacoq.sh
@@ -0,0 +1,16 @@
+#!/bin/bash
+
+# $0 is not the safest way, but...
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+# MetaCoq + UniCoq
+
+git clone --depth 1 https://github.com/unicoq/unicoq.git
+
+( cd unicoq && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install )
+
+git clone --depth 1 https://github.com/MetaCoq/MetaCoq.git
+
+( cd MetaCoq && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} )
+
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
new file mode 100755
index 0000000000..5e41211f1a
--- /dev/null
+++ b/dev/ci/ci-sf.sh
@@ -0,0 +1,11 @@
+#!/bin/bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+wget https://www.cis.upenn.edu/~bcpierce/sf/current/sf.tgz
+tar xvfz sf.tgz
+
+( cd sf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make -j ${NJOBS} )
+
+
diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh
new file mode 100755
index 0000000000..2161a11461
--- /dev/null
+++ b/dev/ci/ci-tlc.sh
@@ -0,0 +1,8 @@
+#!/bin/bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+git clone https://gforge.inria.fr/git/tlc/tlc.git
+
+( cd tlc && make -j ${NJOBS} )