From 27be8637d1f073c245c32aa7c336fb70e1b82c20 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 7 Feb 2017 08:17:52 +0100
Subject: [travis] Move ci files from `tools` to `dev`.

---
 Makefile.ci                 |  2 +-
 README.ci                   |  4 ++--
 dev/ci/ci-color.sh          |  8 ++++++++
 dev/ci/ci-common.sh         |  6 ++++++
 dev/ci/ci-compcert.sh       | 10 ++++++++++
 dev/ci/ci-coquelicot.sh     | 29 +++++++++++++++++++++++++++++
 dev/ci/ci-cpdt.sh           | 10 ++++++++++
 dev/ci/ci-fiat-crypto.sh    | 12 ++++++++++++
 dev/ci/ci-flocq.sh          |  9 +++++++++
 dev/ci/ci-hott.sh           |  8 ++++++++
 dev/ci/ci-iris-coq.sh       | 30 ++++++++++++++++++++++++++++++
 dev/ci/ci-math-classes.sh   | 12 ++++++++++++
 dev/ci/ci-math-comp.sh      | 13 +++++++++++++
 dev/ci/ci-metacoq.sh        | 16 ++++++++++++++++
 dev/ci/ci-sf.sh             | 11 +++++++++++
 dev/ci/ci-tlc.sh            |  8 ++++++++
 tools/ci/ci-color.sh        |  8 --------
 tools/ci/ci-common.sh       |  6 ------
 tools/ci/ci-compcert.sh     | 10 ----------
 tools/ci/ci-coquelicot.sh   | 29 -----------------------------
 tools/ci/ci-cpdt.sh         | 10 ----------
 tools/ci/ci-fiat-crypto.sh  | 12 ------------
 tools/ci/ci-flocq.sh        |  9 ---------
 tools/ci/ci-hott.sh         |  8 --------
 tools/ci/ci-iris-coq.sh     | 30 ------------------------------
 tools/ci/ci-math-classes.sh | 12 ------------
 tools/ci/ci-math-comp.sh    | 13 -------------
 tools/ci/ci-metacoq.sh      | 16 ----------------
 tools/ci/ci-sf.sh           | 11 -----------
 tools/ci/ci-tlc.sh          |  8 --------
 30 files changed, 185 insertions(+), 185 deletions(-)
 create mode 100755 dev/ci/ci-color.sh
 create mode 100644 dev/ci/ci-common.sh
 create mode 100755 dev/ci/ci-compcert.sh
 create mode 100755 dev/ci/ci-coquelicot.sh
 create mode 100755 dev/ci/ci-cpdt.sh
 create mode 100755 dev/ci/ci-fiat-crypto.sh
 create mode 100755 dev/ci/ci-flocq.sh
 create mode 100755 dev/ci/ci-hott.sh
 create mode 100755 dev/ci/ci-iris-coq.sh
 create mode 100755 dev/ci/ci-math-classes.sh
 create mode 100755 dev/ci/ci-math-comp.sh
 create mode 100755 dev/ci/ci-metacoq.sh
 create mode 100755 dev/ci/ci-sf.sh
 create mode 100755 dev/ci/ci-tlc.sh
 delete mode 100755 tools/ci/ci-color.sh
 delete mode 100644 tools/ci/ci-common.sh
 delete mode 100755 tools/ci/ci-compcert.sh
 delete mode 100755 tools/ci/ci-coquelicot.sh
 delete mode 100755 tools/ci/ci-cpdt.sh
 delete mode 100755 tools/ci/ci-fiat-crypto.sh
 delete mode 100755 tools/ci/ci-flocq.sh
 delete mode 100755 tools/ci/ci-hott.sh
 delete mode 100755 tools/ci/ci-iris-coq.sh
 delete mode 100755 tools/ci/ci-math-classes.sh
 delete mode 100755 tools/ci/ci-math-comp.sh
 delete mode 100755 tools/ci/ci-metacoq.sh
 delete mode 100755 tools/ci/ci-sf.sh
 delete mode 100755 tools/ci/ci-tlc.sh

diff --git a/Makefile.ci b/Makefile.ci
index d10ff3ad96..d69028ce13 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -6,5 +6,5 @@ CI_TARGETS=ci-all ci-hott ci-math-comp ci-compcert ci-sf ci-cpdt	\
 
 # Generic rule, we use make to easy travis integraton with mixed rules
 $(CI_TARGETS): ci-%:
-	./tools/ci/ci-$*.sh
+	./dev/ci/ci-$*.sh
 
diff --git a/README.ci b/README.ci
index ed2ba9126e..dcf93cf00e 100644
--- a/README.ci
+++ b/README.ci
@@ -40,7 +40,7 @@ Maintaining your contribution manually [current method]
 ======================================
 
 To add your contribution to the Coq Travis CI set, add a script for
-building your library to `tools/ci/`, update `.travis.yml` and
+building your library to `dev/ci/`, update `.travis.yml` and
 `Makefile.ci`. Then, submit a PR.
 
 Maintaining your contribution as an OPAM package [work in progress] [to be implemented]
@@ -67,7 +67,7 @@ repositories of some of the tests so they can provide fixed
 developments.
 
 The general idea is that the PR author will drop a file
-`tools/ci/overlays/$branch.overlay` where branch name is taken from
+`dev/ci/overlays/$branch.overlay` where branch name is taken from
 `${TRAVIS_PULL_REQUEST_BRANCH:-$TRAVIS_BRANCH}`
 that is to say, the name of the original branch for the PR.
 
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-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..c1306e070d
--- /dev/null
+++ b/dev/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/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} )
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} )
-- 
cgit v1.2.3