Merge PR#453: [travis] Backport trunk's travis support.

19 files changed, 364 insertions, 0 deletions

diff --git a/.travis.yml b/.travis.yml
new file mode 100644
index 000000000..de16f2d0b
--- /dev/null
+++ b/.travis.yml
@@ -0,0 +1,119 @@
+dist: trusty
+sudo: required
+# Until Ocaml becomes a language, we set a known one.
+language: c
+cache:
+  apt: true
+  directories:
+  - $HOME/.opam
+addons:
+  apt:
+    sources:
+    - avsm
+    packages:
+    - opam
+    - aspcud
+    - 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"
+  - TEST_TARGET="ci-unimath"
+  # 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:
+- opam init -j ${NJOBS} --compiler=${COMPILER} -n -y
+- eval $(opam config env)
+- opam config var root
+- opam install -j ${NJOBS} -y camlp5 ocamlfind ${EXTRA_OPAM}
+- opam list
+
+script:
+
+- 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}
+- 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 1dd4efca2..e84d5e377 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 000000000..e4b5832f6
--- /dev/null
+++ b/Makefile.ci
@@ -0,0 +1,11 @@
+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 \
+           ci-unimath
+
+.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/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
new file mode 100755
index 000000000..78ae7f02f
--- /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 000000000..412da626f
--- /dev/null
+++ b/dev/ci/ci-common.sh
@@ -0,0 +1,52 @@
+#!/bin/bash
+
+set -xe
+
+# Coq's tools need an ending slash :S, we should fix them.
+export COQBIN=`pwd`/bin/
+export PATH=`pwd`/bin:$PATH
+
+ls `pwd`/bin
+
+# Maybe we should just use Ruby...
+mathcomp_CI_BRANCH=master
+mathcomp_CI_GITURL=https://github.com/math-comp/math-comp.git
+
+# git_checkout branch
+git_checkout()
+{
+  local _BRANCH=${1}
+  local _URL=${2}
+  local _DEST=${3}
+
+  echo "Checking out ${_DEST}"
+  git clone --depth 1 -b ${_BRANCH} ${_URL} ${_DEST}
+  ( cd ${3} && echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" )
+}
+
+checkout_mathcomp()
+{
+  git_checkout ${mathcomp_CI_BRANCH} ${mathcomp_CI_GITURL} ${1}
+}
+
+# this installs just the ssreflect library of math-comp
+install_ssreflect()
+{
+  echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r'
+
+  checkout_mathcomp math-comp
+  ( 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 Makefile.coq && make -f Makefile.coq -j ${NJOBS} all && make install )
+
+  echo -en 'travis_fold:end:ssr.install\\r'
+
+}
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
new file mode 100755
index 000000000..ec09389f8
--- /dev/null
+++ b/dev/ci/ci-compcert.sh
@@ -0,0 +1,13 @@
+#!/bin/bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+CompCert_CI_BRANCH=master
+CompCert_CI_GITURL=https://github.com/AbsInt/CompCert.git
+
+opam install -j ${NJOBS} -y menhir
+git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} CompCert
+
+# 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 000000000..94bd5e468
--- /dev/null
+++ b/dev/ci/ci-coquelicot.sh
@@ -0,0 +1,12 @@
+#!/bin/bash
+
+# $0 is not the safest way, but...
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+install_ssreflect
+
+# Setup coquelicot
+git_checkout master https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git coquelicot
+
+( 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 000000000..18d756180
--- /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 000000000..c669195dd
--- /dev/null
+++ b/dev/ci/ci-fiat-crypto.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_checkout master https://github.com/mit-plv/fiat-crypto.git fiat-crypto
+
+( cd fiat-crypto && make -j ${NJOBS} )
diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh
new file mode 100755
index 000000000..345924e40
--- /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_checkout master https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git flocq
+
+( 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 000000000..ce870e52b
--- /dev/null
+++ b/dev/ci/ci-geocoq.sh
@@ -0,0 +1,16 @@
+#!/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_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} GeoCoq
+
+( cd GeoCoq                                               && \
+  ./configure.sh                                          && \
+  sed -i.bak '/Ch16_coordinates_with_functions\.v/d' Make && \
+  coq_makefile -f Make -o Makefile                        && \
+  make -j ${NJOBS} )
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
new file mode 100755
index 000000000..0c07564c0
--- /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_checkout mz-8.7 https://github.com/ejgallego/HoTT.git HoTT
+
+( 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 000000000..c21af976f
--- /dev/null
+++ b/dev/ci/ci-iris-coq.sh
@@ -0,0 +1,17 @@
+#!/bin/bash
+
+# $0 is not the safest way, but...
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+install_ssreflect
+
+# Setup stdpp
+git_checkout master https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git coq-stdpp
+
+( cd coq-stdpp && make -j ${NJOBS} && make install )
+
+# Setup Iris
+git_checkout master https://gitlab.mpi-sws.org/FP/iris-coq.git iris-coq
+
+( 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 000000000..4450dc071
--- /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_checkout v8.6 https://github.com/math-classes/math-classes.git math-classes
+( cd math-classes && make -j ${NJOBS} && make install )
+
+git_checkout v8.6 https://github.com/c-corn/corn.git corn
+( 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 000000000..2eb150cb5
--- /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
+
+checkout_mathcomp math-comp
+
+# 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 000000000..91a33695b
--- /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_checkout master https://github.com/unicoq/unicoq.git unicoq
+
+( cd unicoq && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install )
+
+git_checkout master https://github.com/MetaCoq/MetaCoq.git MetaCoq
+
+( 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 000000000..5e41211f1
--- /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 000000000..b94632492
--- /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_checkout master https://gforge.inria.fr/git/tlc/tlc.git tlc
+
+( cd tlc && make -j ${NJOBS} )
diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh
new file mode 100755
index 000000000..15e619acb
--- /dev/null
+++ b/dev/ci/ci-unimath.sh
@@ -0,0 +1,15 @@
+#!/bin/bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+UniMath_CI_BRANCH=master
+UniMath_CI_GITURL=https://github.com/UniMath/UniMath.git
+
+git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} UniMath
+
+( cd UniMath                                  && \
+  sed -i.bak '/Folds/d'              Makefile && \
+  sed -i.bak '/HomologicalAlgebra/d' Makefile && \
+  make -j ${NJOBS} BUILD_COQ=no )
+