Merge branch 'master'.

15 files changed, 203 insertions, 0 deletions

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..589a826e02
--- /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 clone --depth 1 -b ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL}
+
+( 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 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..e97e2c19e3
--- /dev/null
+++ b/dev/ci/ci-iris-coq.sh
@@ -0,0 +1,35 @@
+#!/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 stdpp
+git clone --depth 1 https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git
+
+( cd coq-stdpp && make -j ${NJOBS} && make install )
+
+# 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} )