[travis] [External CI] C-Corn color coquelicot cpdt fiat-crypto floqc iris-coq math-classes sf

- [TLC] [metacoq] not ready for 8.6 yet

16 files changed, 179 insertions, 34 deletions

diff --git a/.travis.yml b/.travis.yml
index c85122ac96..1dc08fb3db 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -21,9 +21,20 @@ env:
   # Main test suites
   matrix:
   - TEST_TARGET="validate"           TW="travis_wait"
+  - TEST_TARGET="ci-color"
+  - TEST_TARGET="ci-compcert"
+  - TEST_TARGET="ci-coquelicot"
+  - TEST_TARGET="ci-cpdt"
+  - 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-compcert"
+  - TEST_TARGET="ci-sf"
+  # Not ready yet for 8.7
+  # - TEST_TARGET="ci-metacoq"
+  # - TEST_TARGET="ci-tlc"
 
 matrix:
 
diff --git a/Makefile.ci b/Makefile.ci
index ada698e0a6..d10ff3ad96 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -1,13 +1,10 @@
-.PHONY: ci-all ci-hott ci-math-comp ci-compcert
+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-all: ci-hott ci-math-comp ci-compcert
+.PHONY: $(CI_TARGETS)
 
-# TODO Do generic rule
-ci-hott:
-	./tools/ci/ci-hott.sh
+# Generic rule, we use make to easy travis integraton with mixed rules
+$(CI_TARGETS): ci-%:
+	./tools/ci/ci-$*.sh
 
-ci-math-comp:
-	./tools/ci/ci-math-comp.sh
-
-ci-compcert:
-	./tools/ci/ci-compcert.sh
diff --git a/tools/ci/ci-color.sh b/tools/ci/ci-color.sh
new file mode 100755
index 0000000000..78ae7f02f9
--- /dev/null
+++ b/tools/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/tools/ci/ci-common.sh b/tools/ci/ci-common.sh
new file mode 100644
index 0000000000..2a6601e045
--- /dev/null
+++ b/tools/ci/ci-common.sh
@@ -0,0 +1,6 @@
+#!/bin/bash
+
+set -xe
+
+export PATH=`pwd`/bin:$PATH
+ls `pwd`/bin
diff --git a/tools/ci/ci-compcert.sh b/tools/ci/ci-compcert.sh
index 416e283254..d4023c9165 100755
--- a/tools/ci/ci-compcert.sh
+++ b/tools/ci/ci-compcert.sh
@@ -1,17 +1,10 @@
 #!/bin/bash
 
-# Proof of concept contrib build script.
-
-set -xe
-
-export PATH=`pwd`/bin:$PATH
-ls `pwd`/bin
+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
 
-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
+( cd CompCert && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make -j ${NJOBS} )
diff --git a/tools/ci/ci-coquelicot.sh b/tools/ci/ci-coquelicot.sh
new file mode 100755
index 0000000000..4a23e51be6
--- /dev/null
+++ b/tools/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/tools/ci/ci-cpdt.sh b/tools/ci/ci-cpdt.sh
new file mode 100755
index 0000000000..18d7561804
--- /dev/null
+++ b/tools/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/tools/ci/ci-fiat-crypto.sh b/tools/ci/ci-fiat-crypto.sh
new file mode 100755
index 0000000000..c594f83603
--- /dev/null
+++ b/tools/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/tools/ci/ci-flocq.sh b/tools/ci/ci-flocq.sh
new file mode 100755
index 0000000000..b9cf649a1a
--- /dev/null
+++ b/tools/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/tools/ci/ci-hott.sh b/tools/ci/ci-hott.sh
index 35af76ceb7..8f82ba9f21 100755
--- a/tools/ci/ci-hott.sh
+++ b/tools/ci/ci-hott.sh
@@ -1,13 +1,8 @@
 #!/bin/bash
 
-# Proof of concept contrib build script.
-
-set -xe
-
-export PATH=`pwd`/bin:$PATH
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
 
 git clone --depth 3 -b mz-8.6 https://github.com/ejgallego/HoTT.git
 
-pushd HoTT
-./autogen.sh && ./configure && make -j ${NJOBS}
-popd
+( cd HoTT && ./autogen.sh && ./configure && make -j ${NJOBS} )
diff --git a/tools/ci/ci-iris-coq.sh b/tools/ci/ci-iris-coq.sh
new file mode 100755
index 0000000000..c1306e070d
--- /dev/null
+++ b/tools/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/tools/ci/ci-math-classes.sh b/tools/ci/ci-math-classes.sh
new file mode 100755
index 0000000000..9127c18951
--- /dev/null
+++ b/tools/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/tools/ci/ci-math-comp.sh b/tools/ci/ci-math-comp.sh
index 39a92a2d89..b833792419 100755
--- a/tools/ci/ci-math-comp.sh
+++ b/tools/ci/ci-math-comp.sh
@@ -1,10 +1,8 @@
 #!/bin/bash
 
-# Proof of concept contrib build script.
-
-set -xe
-
-export PATH=`pwd`/bin:$PATH
+# $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
 
diff --git a/tools/ci/ci-metacoq.sh b/tools/ci/ci-metacoq.sh
new file mode 100755
index 0000000000..9a9bd3648b
--- /dev/null
+++ b/tools/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/tools/ci/ci-sf.sh b/tools/ci/ci-sf.sh
new file mode 100755
index 0000000000..5e41211f1a
--- /dev/null
+++ b/tools/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/tools/ci/ci-tlc.sh b/tools/ci/ci-tlc.sh
new file mode 100755
index 0000000000..2161a11461
--- /dev/null
+++ b/tools/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} )