[travis] [External CI] compcert HoTT math-comp

- Improve the setup to support external contribs.
  We use a more minimalistic Coq build, gaining a few extra minutes.
- [math-comp] workaround `make -j` bug to enable parallel building.

6 files changed, 124 insertions, 17 deletions

diff --git a/.travis.yml b/.travis.yml
index f9d496563..ab59cf6bf 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -12,31 +12,75 @@ 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
 env:
   global:
   - NJOBS=1
+  - COMPILER="4.02.3"
+  # Main test suites
   matrix:
-  - TEST_TARGET="validate"    TW="travis_wait"
-  - TEST_TARGET="test-suite"  TW=""
+  - TEST_TARGET="validate"           TW="travis_wait"
+  - TEST_TARGET="contrib-hott"
+  - TEST_TARGET="contrib-math-comp"
+  - TEST_TARGET="contrib-compcert"
+
+matrix:
+  # Extra is Full COQ build and test-suite with two compilers
+  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:
-- "[ -e .opam ] || opam init -j ${NJOBS} --compiler=4.02.3 -n -y"
+- "[ -e .opam ] || 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
+- ./configure -local -usecamlp5 -native-compiler yes ${EXTRA_CONF}
 - make -j ${NJOBS}
 - ${TW} make -j ${NJOBS} ${TEST_TARGET}
diff --git a/Makefile b/Makefile
index 0f9619c01..25a97f9bb 100644
--- a/Makefile
+++ b/Makefile
@@ -246,6 +246,11 @@ devdocclean:
 	rm -f $(OCAMLDOCDIR)/html/*.html
 
 ###########################################################################
+# Contrib tests
+###########################################################################
+include Makefile.contrib
+
+###########################################################################
 # Emacs tags
 ###########################################################################
 
diff --git a/Makefile.contrib b/Makefile.contrib
new file mode 100644
index 000000000..2e3ed94c5
--- /dev/null
+++ b/Makefile.contrib
@@ -0,0 +1,13 @@
+.PHONY: contrib-all contrib-hott contrib-math-comp
+
+contrib-all: contrib-hott contrib-math-comp
+
+# TODO Do generic rule
+contrib-hott:
+	./tools/ci/contrib-hott.sh
+
+contrib-math-comp:
+	./tools/ci/contrib-math-comp.sh
+
+contrib-compcert:
+	./tools/ci/contrib-compcert.sh
diff --git a/tools/ci/contrib-compcert.sh b/tools/ci/contrib-compcert.sh
new file mode 100755
index 000000000..416e28325
--- /dev/null
+++ b/tools/ci/contrib-compcert.sh
@@ -0,0 +1,17 @@
+#!/bin/bash
+
+# Proof of concept contrib build script.
+
+set -xe
+
+export PATH=`pwd`/bin:$PATH
+ls `pwd`/bin
+
+opam install -j ${NJOBS} -y menhir
+git clone --depth 3 -b coq-8.6 https://github.com/maximedenes/CompCert.git
+
+pushd CompCert
+# Patch to avoid the upper version limit
+sed -i.bak 's/8.6)/8.6|trunk)/' configure
+./configure x86_32-linux && make -j ${NJOBS}
+popd
diff --git a/tools/ci/contrib-hott.sh b/tools/ci/contrib-hott.sh
new file mode 100755
index 000000000..35af76ceb
--- /dev/null
+++ b/tools/ci/contrib-hott.sh
@@ -0,0 +1,13 @@
+#!/bin/bash
+
+# Proof of concept contrib build script.
+
+set -xe
+
+export PATH=`pwd`/bin:$PATH
+
+git clone --depth 3 -b mz-8.6 https://github.com/ejgallego/HoTT.git
+
+pushd HoTT
+./autogen.sh && ./configure && make -j ${NJOBS}
+popd
diff --git a/tools/ci/contrib-math-comp.sh b/tools/ci/contrib-math-comp.sh
new file mode 100755
index 000000000..39a92a2d8
--- /dev/null
+++ b/tools/ci/contrib-math-comp.sh
@@ -0,0 +1,15 @@
+#!/bin/bash
+
+# Proof of concept contrib build script.
+
+set -xe
+
+export PATH=`pwd`/bin:$PATH
+
+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 )