[travis] Move ci files from `tools` to `dev`.

14 files changed, 0 insertions, 182 deletions

diff --git a/tools/ci/ci-color.sh b/tools/ci/ci-color.sh
deleted file mode 100755
index 78ae7f02f9..0000000000
--- a/tools/ci/ci-color.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-#!/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
deleted file mode 100644
index 2a6601e045..0000000000
--- a/tools/ci/ci-common.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/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
deleted file mode 100755
index d4023c9165..0000000000
--- a/tools/ci/ci-compcert.sh
+++ /dev/null
@@ -1,10 +0,0 @@
-#!/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/tools/ci/ci-coquelicot.sh b/tools/ci/ci-coquelicot.sh
deleted file mode 100755
index 4a23e51be6..0000000000
--- a/tools/ci/ci-coquelicot.sh
+++ /dev/null
@@ -1,29 +0,0 @@
-#!/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
deleted file mode 100755
index 18d7561804..0000000000
--- a/tools/ci/ci-cpdt.sh
+++ /dev/null
@@ -1,10 +0,0 @@
-#!/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
deleted file mode 100755
index c594f83603..0000000000
--- a/tools/ci/ci-fiat-crypto.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/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
deleted file mode 100755
index b9cf649a1a..0000000000
--- a/tools/ci/ci-flocq.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-#!/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
deleted file mode 100755
index 8f82ba9f21..0000000000
--- a/tools/ci/ci-hott.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-#!/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/tools/ci/ci-iris-coq.sh b/tools/ci/ci-iris-coq.sh
deleted file mode 100755
index c1306e070d..0000000000
--- a/tools/ci/ci-iris-coq.sh
+++ /dev/null
@@ -1,30 +0,0 @@
-#!/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
deleted file mode 100755
index 9127c18951..0000000000
--- a/tools/ci/ci-math-classes.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/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
deleted file mode 100755
index b833792419..0000000000
--- a/tools/ci/ci-math-comp.sh
+++ /dev/null
@@ -1,13 +0,0 @@
-#!/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/tools/ci/ci-metacoq.sh b/tools/ci/ci-metacoq.sh
deleted file mode 100755
index 9a9bd3648b..0000000000
--- a/tools/ci/ci-metacoq.sh
+++ /dev/null
@@ -1,16 +0,0 @@
-#!/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
deleted file mode 100755
index 5e41211f1a..0000000000
--- a/tools/ci/ci-sf.sh
+++ /dev/null
@@ -1,11 +0,0 @@
-#!/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
deleted file mode 100755
index 2161a11461..0000000000
--- a/tools/ci/ci-tlc.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-#!/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} )