Merge PR#431

[travis] Add math-comp overlays, update CompCert to official version, add UniMath

15 files changed, 89 insertions, 61 deletions

diff --git a/.travis.yml b/.travis.yml
index 188e446007..de16f2d0b4 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -36,6 +36,7 @@ env:
   - 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"
diff --git a/Makefile.ci b/Makefile.ci
index 040144e6e8..e4b5832f60 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -1,6 +1,7 @@
-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_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)
 
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 2a6601e045..412da626fd 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -2,5 +2,51 @@
 
 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
index d4023c9165..ec09389f8e 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -3,8 +3,11 @@
 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 clone --depth 3 -b coq-8.6 https://github.com/maximedenes/CompCert.git
+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
index 4a23e51be6..94bd5e468f 100755
--- a/dev/ci/ci-coquelicot.sh
+++ b/dev/ci/ci-coquelicot.sh
@@ -4,26 +4,9 @@
 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
+install_ssreflect
 
 # Setup coquelicot
-git clone --depth 3 https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git
+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-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index c594f83603..c669195ddd 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -4,9 +4,6 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-git clone --depth 3 https://github.com/mit-plv/fiat-crypto.git
+git_checkout master https://github.com/mit-plv/fiat-crypto.git fiat-crypto
 
 ( 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
index b9cf649a1a..345924e40a 100755
--- a/dev/ci/ci-flocq.sh
+++ b/dev/ci/ci-flocq.sh
@@ -4,6 +4,6 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-git clone --depth 3 https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git
+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
index 589a826e02..ce870e52b5 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -7,7 +7,7 @@ source ${ci_dir}/ci-common.sh
 GeoCoq_CI_BRANCH=master
 GeoCoq_CI_GITURL=https://github.com/GeoCoq/GeoCoq.git
 
-git clone --depth 1 -b ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL}
+git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} GeoCoq
 
 ( cd GeoCoq                                               && \
   ./configure.sh                                          && \
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index 8f82ba9f21..aaffc9d484 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -3,6 +3,6 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-git clone --depth 3 -b mz-8.6 https://github.com/ejgallego/HoTT.git
+git_checkout mz-8.6 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
index e97e2c19e3..c21af976f4 100755
--- a/dev/ci/ci-iris-coq.sh
+++ b/dev/ci/ci-iris-coq.sh
@@ -4,32 +4,14 @@
 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
+install_ssreflect
 
 # Setup stdpp
-git clone --depth 1 https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git
+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 clone --depth 1 https://gitlab.mpi-sws.org/FP/iris-coq.git
+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
index 9127c18951..4450dc0710 100755
--- a/dev/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math-classes.sh
@@ -4,9 +4,9 @@
 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
+git_checkout v8.6 https://github.com/math-classes/math-classes.git math-classes
 ( cd math-classes && make -j ${NJOBS} && make install )
 
-git clone --depth 1 -b v8.6 https://github.com/c-corn/corn.git
+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
index b833792419..2eb150cb52 100755
--- a/dev/ci/ci-math-comp.sh
+++ b/dev/ci/ci-math-comp.sh
@@ -4,10 +4,10 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-git clone --depth 3 https://github.com/math-comp/math-comp.git
+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 )
+( 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
index 9a9bd3648b..91a33695b0 100755
--- a/dev/ci/ci-metacoq.sh
+++ b/dev/ci/ci-metacoq.sh
@@ -6,11 +6,11 @@ source ${ci_dir}/ci-common.sh
 
 # MetaCoq + UniCoq
 
-git clone --depth 1 https://github.com/unicoq/unicoq.git
+git_checkout master https://github.com/unicoq/unicoq.git unicoq
 
 ( cd unicoq && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install )
 
-git clone --depth 1 https://github.com/MetaCoq/MetaCoq.git
+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-tlc.sh b/dev/ci/ci-tlc.sh
index 2161a11461..b946324924 100755
--- a/dev/ci/ci-tlc.sh
+++ b/dev/ci/ci-tlc.sh
@@ -3,6 +3,6 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-git clone https://gforge.inria.fr/git/tlc/tlc.git
+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 0000000000..15e619acbb
--- /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 )
+