From 348160a1c59da5c448a56a2e2802865f94a40ddc Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 4 Feb 2017 21:18:54 +0100
Subject: [travis] Run tests using a parallel matrix.

We also optimize `travis_wait` use.
---
 .travis.yml | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index 3e71a71570..f9d4965638 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -24,8 +24,13 @@ addons:
     - ghostscript
     - transfig
     - imagemagick
+env:
+  global:
+  - NJOBS=1
+  matrix:
+  - TEST_TARGET="validate"    TW="travis_wait"
+  - TEST_TARGET="test-suite"  TW=""
 install:
-- ": ${NJOBS:=1}"
 - "[ -e .opam ] || opam init -j ${NJOBS} --compiler=4.02.3 -n -y"
 - eval $(opam config env)
 - opam config var root
@@ -34,5 +39,4 @@ install:
 script:
 - ./configure -local -usecamlp5 -native-compiler yes -coqide opt -with-doc yes
 - make -j ${NJOBS}
-- travis_wait make -j ${NJOBS} validate
-- travis_wait make -j ${NJOBS} test-suite
+- ${TW} make -j ${NJOBS} ${TEST_TARGET}
-- 
cgit v1.2.3


From 3e07baa69f1e7de02670dd20dd7577d70c2f2653 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 4 Feb 2017 21:25:14 +0100
Subject: [travis] [External CI] compcert HoTT math-comp

- Improve the setup to support external contribs.
  We use a more minimalistic Coq build, gaining a few extra minutes.
- [math-comp] workaround `make -j` bug to enable parallel building.
---
 .travis.yml                   | 78 +++++++++++++++++++++++++++++++++----------
 Makefile                      |  5 +++
 Makefile.contrib              | 13 ++++++++
 tools/ci/contrib-compcert.sh  | 17 ++++++++++
 tools/ci/contrib-hott.sh      | 13 ++++++++
 tools/ci/contrib-math-comp.sh | 15 +++++++++
 6 files changed, 124 insertions(+), 17 deletions(-)
 create mode 100644 Makefile.contrib
 create mode 100755 tools/ci/contrib-compcert.sh
 create mode 100755 tools/ci/contrib-hott.sh
 create mode 100755 tools/ci/contrib-math-comp.sh

diff --git a/.travis.yml b/.travis.yml
index f9d4965638..ab59cf6bf7 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -12,31 +12,75 @@ addons:
     packages:
     - opam
     - aspcud
-    - libgtk2.0-dev
-    - libgtksourceview2.0-dev
-    - texlive-latex-base
-    - texlive-latex-recommended
-    - texlive-latex-extra
-    - texlive-math-extra
-    - texlive-fonts-recommended
-    - texlive-fonts-extra
-    - latex-xcolor
-    - ghostscript
-    - transfig
-    - imagemagick
 env:
   global:
   - NJOBS=1
+  - COMPILER="4.02.3"
+  # Main test suites
   matrix:
-  - TEST_TARGET="validate"    TW="travis_wait"
-  - TEST_TARGET="test-suite"  TW=""
+  - TEST_TARGET="validate"           TW="travis_wait"
+  - TEST_TARGET="contrib-hott"
+  - TEST_TARGET="contrib-math-comp"
+  - TEST_TARGET="contrib-compcert"
+
+matrix:
+  # Extra is Full COQ build and test-suite with two compilers
+  include:
+    - env:
+      - TEST_TARGET="test-suite"
+      - EXTRA_CONF="-coqide opt -with-doc yes"
+      - EXTRA_OPAM="lablgtk-extras hevea"
+      addons:
+        apt:
+          sources:
+          - avsm
+          packages:
+          - opam
+          - aspcud
+          - libgtk2.0-dev
+          - libgtksourceview2.0-dev
+          - texlive-latex-base
+          - texlive-latex-recommended
+          - texlive-latex-extra
+          - texlive-math-extra
+          - texlive-fonts-recommended
+          - texlive-fonts-extra
+          - latex-xcolor
+          - ghostscript
+          - transfig
+          - imagemagick
+    - env:
+      - TEST_TARGET="test-suite"
+      - COMPILER="4.04.0"
+      - EXTRA_CONF="-coqide opt -with-doc yes"
+      - EXTRA_OPAM="lablgtk-extras hevea"
+      addons:
+        apt:
+          sources:
+          - avsm
+          packages:
+          - opam
+          - aspcud
+          - libgtk2.0-dev
+          - libgtksourceview2.0-dev
+          - texlive-latex-base
+          - texlive-latex-recommended
+          - texlive-latex-extra
+          - texlive-math-extra
+          - texlive-fonts-recommended
+          - texlive-fonts-extra
+          - latex-xcolor
+          - ghostscript
+          - transfig
+          - imagemagick
+
 install:
-- "[ -e .opam ] || opam init -j ${NJOBS} --compiler=4.02.3 -n -y"
+- "[ -e .opam ] || opam init -j ${NJOBS} --compiler=${COMPILER} -n -y"
 - eval $(opam config env)
 - opam config var root
-- opam install -j ${NJOBS} -y camlp5 ocamlfind lablgtk-extras hevea
+- opam install -j ${NJOBS} -y camlp5 ocamlfind ${EXTRA_OPAM}
 - opam list
 script:
-- ./configure -local -usecamlp5 -native-compiler yes -coqide opt -with-doc yes
+- ./configure -local -usecamlp5 -native-compiler yes ${EXTRA_CONF}
 - make -j ${NJOBS}
 - ${TW} make -j ${NJOBS} ${TEST_TARGET}
diff --git a/Makefile b/Makefile
index 0f9619c01b..25a97f9bb1 100644
--- a/Makefile
+++ b/Makefile
@@ -245,6 +245,11 @@ devdocclean:
 	rm -f $(OCAMLDOCDIR)/ocamldoc.sty $(OCAMLDOCDIR)/coq.tex 
 	rm -f $(OCAMLDOCDIR)/html/*.html
 
+###########################################################################
+# Contrib tests
+###########################################################################
+include Makefile.contrib
+
 ###########################################################################
 # Emacs tags
 ###########################################################################
diff --git a/Makefile.contrib b/Makefile.contrib
new file mode 100644
index 0000000000..2e3ed94c53
--- /dev/null
+++ b/Makefile.contrib
@@ -0,0 +1,13 @@
+.PHONY: contrib-all contrib-hott contrib-math-comp
+
+contrib-all: contrib-hott contrib-math-comp
+
+# TODO Do generic rule
+contrib-hott:
+	./tools/ci/contrib-hott.sh
+
+contrib-math-comp:
+	./tools/ci/contrib-math-comp.sh
+
+contrib-compcert:
+	./tools/ci/contrib-compcert.sh
diff --git a/tools/ci/contrib-compcert.sh b/tools/ci/contrib-compcert.sh
new file mode 100755
index 0000000000..416e283254
--- /dev/null
+++ b/tools/ci/contrib-compcert.sh
@@ -0,0 +1,17 @@
+#!/bin/bash
+
+# Proof of concept contrib build script.
+
+set -xe
+
+export PATH=`pwd`/bin:$PATH
+ls `pwd`/bin
+
+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
diff --git a/tools/ci/contrib-hott.sh b/tools/ci/contrib-hott.sh
new file mode 100755
index 0000000000..35af76ceb7
--- /dev/null
+++ b/tools/ci/contrib-hott.sh
@@ -0,0 +1,13 @@
+#!/bin/bash
+
+# Proof of concept contrib build script.
+
+set -xe
+
+export PATH=`pwd`/bin:$PATH
+
+git clone --depth 3 -b mz-8.6 https://github.com/ejgallego/HoTT.git
+
+pushd HoTT
+./autogen.sh && ./configure && make -j ${NJOBS}
+popd
diff --git a/tools/ci/contrib-math-comp.sh b/tools/ci/contrib-math-comp.sh
new file mode 100755
index 0000000000..39a92a2d89
--- /dev/null
+++ b/tools/ci/contrib-math-comp.sh
@@ -0,0 +1,15 @@
+#!/bin/bash
+
+# Proof of concept contrib build script.
+
+set -xe
+
+export PATH=`pwd`/bin:$PATH
+
+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 )
-- 
cgit v1.2.3


From 3a66f149a34613ef0ed04046fed3947e8e720cd6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 4 Feb 2017 22:32:49 +0100
Subject: [travis] Improvements to main script

- Add README.ci
  Suggestions and comments welcome.
- Use the system compiler to get some boot speedup.
- Build log folding.
- Set NJOBS=2 (very moderate speedup)
- Set language to a defined value.
  OPAM itself recommends C, so we follow suit.
- Remove spurious `.opam`test

  No harm in testing we are in the right opam setting even if the
  cache did exist.

  Anyways, it seems that the previous was spurious, as it was testing
  if ~/coq/.opam did exists. I think the correct command would have
  been:

```shell
[ -e ${HOME}/.opam ] || opam init ...
```

  See the log at https://travis-ci.org/coq/coq/builds/198948812 for an
  example.
---
 .travis.yml | 27 ++++++++++++++++++----
 README.ci   | 77 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 99 insertions(+), 5 deletions(-)
 create mode 100644 README.ci

diff --git a/.travis.yml b/.travis.yml
index ab59cf6bf7..14573e2952 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -1,6 +1,7 @@
 dist: trusty
 sudo: required
-language: ocaml
+# Until Ocaml becomes a language, we set a known one.
+language: c
 cache:
   apt: true
   directories:
@@ -14,8 +15,9 @@ addons:
     - aspcud
 env:
   global:
-  - NJOBS=1
-  - COMPILER="4.02.3"
+  - NJOBS=2
+  # system is == 4.02.3
+  - COMPILER="system"
   # Main test suites
   matrix:
   - TEST_TARGET="validate"           TW="travis_wait"
@@ -24,7 +26,12 @@ env:
   - TEST_TARGET="contrib-compcert"
 
 matrix:
-  # Extra is Full COQ build and test-suite with two compilers
+
+  allow_failures:
+  - env: TEST_TARGET="ci-cpdt"
+
+  # Full Coq test-suite with two compilers
+  # [TODO: use yaml refs and avoid duplication for packages list]
   include:
     - env:
       - TEST_TARGET="test-suite"
@@ -75,12 +82,22 @@ matrix:
           - imagemagick
 
 install:
-- "[ -e .opam ] || opam init -j ${NJOBS} --compiler=${COMPILER} -n -y"
+- opam init -j ${NJOBS} --compiler=${COMPILER} -n -y
 - eval $(opam config env)
 - opam config var root
 - opam install -j ${NJOBS} -y camlp5 ocamlfind ${EXTRA_OPAM}
 - opam list
+
 script:
+
+- echo 'Configuring Coq...' && echo -en 'travis_fold:start:coq.config\\r'
 - ./configure -local -usecamlp5 -native-compiler yes ${EXTRA_CONF}
+- echo -en 'travis_fold:end:coq.config\\r'
+
+- echo 'Building Coq...' && echo -en 'travis_fold:start:coq.build\\r'
 - make -j ${NJOBS}
+- echo -en 'travis_fold:end:coq.build\\r'
+
+- echo 'Running tests...' && echo -en 'travis_fold:start:coq.test\\r'
 - ${TW} make -j ${NJOBS} ${TEST_TARGET}
+- echo -en 'travis_fold:end:coq.test\\r'
diff --git a/README.ci b/README.ci
new file mode 100644
index 0000000000..ed2ba9126e
--- /dev/null
+++ b/README.ci
@@ -0,0 +1,77 @@
+**WARNING:** This document is a work in progress and intended as a RFC.
+If you are not a Coq Developer, don't follow this instructions yet.
+
+Introduction
+============
+
+The Coq Travis CI infrastructure is meant to provide lightweight
+automatics testing of pull requests.
+
+More comprehensive testing is the responsability of Coq's [Jenkins CI
+server](https://ci.inria.fr/coq/) see, [XXX: add document] for
+instructions on how to add your development to Jenkins.
+
+How to submit your development for Coq Travis CI
+================================================
+
+Travis CI provides a convenient way to perform testing of Coq changes
+versus a set of curated libraries.
+
+Are you an author of a Coq library who would be interested in having
+the latest Coq changes validated against your development?
+
+If so, keep reading! Getting Coq changes tested against your library
+is easy, all that you need to do is:
+
+1.- Put you development in a public repository tracking coq trunk.
+2.- Make sure that your development builds in less than 35 minutes.
+3.- Submit a PR adding you development.
+4.- ?
+5.- Profit! Your library is now part of Coq's continous integration!
+
+Note that by partipating in this program, you assume a reasonable
+compromise to discuss and eventually integrate compatibility changes
+upstream.
+
+Get in touch with us to discuss any special need your development may
+have.
+
+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
+`Makefile.ci`. Then, submit a PR.
+
+Maintaining your contribution as an OPAM package [work in progress] [to be implemented]
+================================================
+
+You can also provide an opam package for your contribution XXX at
+https://github.com/coq/opam-coq-archive
+
+Then, add a `ci-opam-XXX` target to the `.travis.yml` file, the
+package XXX.dev will be tested against each Coq commit and pull
+request.
+
+- TODO: The main question here is what to do with `.opam` caching. We
+  could disable it altogether, however this will have an impact. We
+  could install a dummy Coq package, but `coq-*` dependencies will be
+  botched too. Need to think more.
+
+PR Overlays [work in progress] [to be implemented]
+===========
+
+It is common for PR to break some of the external tests. To this
+purpose, we provide a method for particular PR to overlay the
+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
+`${TRAVIS_PULL_REQUEST_BRANCH:-$TRAVIS_BRANCH}`
+that is to say, the name of the original branch for the PR.
+
+The `.overlay` file will contain a set of variables that will be used
+to do the corresponding `opam pin` or to overload the corresponding
+git repositories, etc...
+
-- 
cgit v1.2.3


From 138a4da7f0133d7b4ea06cfbc938d23ddb88c97d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 4 Feb 2017 23:55:24 +0100
Subject: [travis] [External CI] Script renaming.

---
 .travis.yml                   |  6 +++---
 Makefile                      |  4 ++--
 Makefile.ci                   | 13 +++++++++++++
 Makefile.contrib              | 13 -------------
 tools/ci/ci-compcert.sh       | 17 +++++++++++++++++
 tools/ci/ci-hott.sh           | 13 +++++++++++++
 tools/ci/ci-math-comp.sh      | 15 +++++++++++++++
 tools/ci/contrib-compcert.sh  | 17 -----------------
 tools/ci/contrib-hott.sh      | 13 -------------
 tools/ci/contrib-math-comp.sh | 15 ---------------
 10 files changed, 63 insertions(+), 63 deletions(-)
 create mode 100644 Makefile.ci
 delete mode 100644 Makefile.contrib
 create mode 100755 tools/ci/ci-compcert.sh
 create mode 100755 tools/ci/ci-hott.sh
 create mode 100755 tools/ci/ci-math-comp.sh
 delete mode 100755 tools/ci/contrib-compcert.sh
 delete mode 100755 tools/ci/contrib-hott.sh
 delete mode 100755 tools/ci/contrib-math-comp.sh

diff --git a/.travis.yml b/.travis.yml
index 14573e2952..c85122ac96 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -21,9 +21,9 @@ env:
   # Main test suites
   matrix:
   - TEST_TARGET="validate"           TW="travis_wait"
-  - TEST_TARGET="contrib-hott"
-  - TEST_TARGET="contrib-math-comp"
-  - TEST_TARGET="contrib-compcert"
+  - TEST_TARGET="ci-hott"
+  - TEST_TARGET="ci-math-comp"
+  - TEST_TARGET="ci-compcert"
 
 matrix:
 
diff --git a/Makefile b/Makefile
index 25a97f9bb1..e1d6e8e1d2 100644
--- a/Makefile
+++ b/Makefile
@@ -246,9 +246,9 @@ devdocclean:
 	rm -f $(OCAMLDOCDIR)/html/*.html
 
 ###########################################################################
-# Contrib tests
+# Continuous Intregration Tests
 ###########################################################################
-include Makefile.contrib
+include Makefile.ci
 
 ###########################################################################
 # Emacs tags
diff --git a/Makefile.ci b/Makefile.ci
new file mode 100644
index 0000000000..ada698e0a6
--- /dev/null
+++ b/Makefile.ci
@@ -0,0 +1,13 @@
+.PHONY: ci-all ci-hott ci-math-comp ci-compcert
+
+ci-all: ci-hott ci-math-comp ci-compcert
+
+# TODO Do generic rule
+ci-hott:
+	./tools/ci/ci-hott.sh
+
+ci-math-comp:
+	./tools/ci/ci-math-comp.sh
+
+ci-compcert:
+	./tools/ci/ci-compcert.sh
diff --git a/Makefile.contrib b/Makefile.contrib
deleted file mode 100644
index 2e3ed94c53..0000000000
--- a/Makefile.contrib
+++ /dev/null
@@ -1,13 +0,0 @@
-.PHONY: contrib-all contrib-hott contrib-math-comp
-
-contrib-all: contrib-hott contrib-math-comp
-
-# TODO Do generic rule
-contrib-hott:
-	./tools/ci/contrib-hott.sh
-
-contrib-math-comp:
-	./tools/ci/contrib-math-comp.sh
-
-contrib-compcert:
-	./tools/ci/contrib-compcert.sh
diff --git a/tools/ci/ci-compcert.sh b/tools/ci/ci-compcert.sh
new file mode 100755
index 0000000000..416e283254
--- /dev/null
+++ b/tools/ci/ci-compcert.sh
@@ -0,0 +1,17 @@
+#!/bin/bash
+
+# Proof of concept contrib build script.
+
+set -xe
+
+export PATH=`pwd`/bin:$PATH
+ls `pwd`/bin
+
+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
diff --git a/tools/ci/ci-hott.sh b/tools/ci/ci-hott.sh
new file mode 100755
index 0000000000..35af76ceb7
--- /dev/null
+++ b/tools/ci/ci-hott.sh
@@ -0,0 +1,13 @@
+#!/bin/bash
+
+# Proof of concept contrib build script.
+
+set -xe
+
+export PATH=`pwd`/bin:$PATH
+
+git clone --depth 3 -b mz-8.6 https://github.com/ejgallego/HoTT.git
+
+pushd HoTT
+./autogen.sh && ./configure && make -j ${NJOBS}
+popd
diff --git a/tools/ci/ci-math-comp.sh b/tools/ci/ci-math-comp.sh
new file mode 100755
index 0000000000..39a92a2d89
--- /dev/null
+++ b/tools/ci/ci-math-comp.sh
@@ -0,0 +1,15 @@
+#!/bin/bash
+
+# Proof of concept contrib build script.
+
+set -xe
+
+export PATH=`pwd`/bin:$PATH
+
+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/contrib-compcert.sh b/tools/ci/contrib-compcert.sh
deleted file mode 100755
index 416e283254..0000000000
--- a/tools/ci/contrib-compcert.sh
+++ /dev/null
@@ -1,17 +0,0 @@
-#!/bin/bash
-
-# Proof of concept contrib build script.
-
-set -xe
-
-export PATH=`pwd`/bin:$PATH
-ls `pwd`/bin
-
-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
diff --git a/tools/ci/contrib-hott.sh b/tools/ci/contrib-hott.sh
deleted file mode 100755
index 35af76ceb7..0000000000
--- a/tools/ci/contrib-hott.sh
+++ /dev/null
@@ -1,13 +0,0 @@
-#!/bin/bash
-
-# Proof of concept contrib build script.
-
-set -xe
-
-export PATH=`pwd`/bin:$PATH
-
-git clone --depth 3 -b mz-8.6 https://github.com/ejgallego/HoTT.git
-
-pushd HoTT
-./autogen.sh && ./configure && make -j ${NJOBS}
-popd
diff --git a/tools/ci/contrib-math-comp.sh b/tools/ci/contrib-math-comp.sh
deleted file mode 100755
index 39a92a2d89..0000000000
--- a/tools/ci/contrib-math-comp.sh
+++ /dev/null
@@ -1,15 +0,0 @@
-#!/bin/bash
-
-# Proof of concept contrib build script.
-
-set -xe
-
-export PATH=`pwd`/bin:$PATH
-
-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 )
-- 
cgit v1.2.3


From 487e19a495b8727b0d3f11a8f0238d17aa9e9303 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 5 Feb 2017 01:02:39 +0100
Subject: [travis] [External CI] C-Corn color coquelicot cpdt fiat-crypto floqc
 iris-coq math-classes sf

- [TLC] [metacoq] not ready for 8.6 yet
---
 .travis.yml                 | 13 ++++++++++++-
 Makefile.ci                 | 17 +++++++----------
 tools/ci/ci-color.sh        |  8 ++++++++
 tools/ci/ci-common.sh       |  6 ++++++
 tools/ci/ci-compcert.sh     | 13 +++----------
 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         | 11 +++--------
 tools/ci/ci-iris-coq.sh     | 30 ++++++++++++++++++++++++++++++
 tools/ci/ci-math-classes.sh | 12 ++++++++++++
 tools/ci/ci-math-comp.sh    |  8 +++-----
 tools/ci/ci-metacoq.sh      | 16 ++++++++++++++++
 tools/ci/ci-sf.sh           | 11 +++++++++++
 tools/ci/ci-tlc.sh          |  8 ++++++++
 16 files changed, 179 insertions(+), 34 deletions(-)
 create mode 100755 tools/ci/ci-color.sh
 create mode 100644 tools/ci/ci-common.sh
 create mode 100755 tools/ci/ci-coquelicot.sh
 create mode 100755 tools/ci/ci-cpdt.sh
 create mode 100755 tools/ci/ci-fiat-crypto.sh
 create mode 100755 tools/ci/ci-flocq.sh
 create mode 100755 tools/ci/ci-iris-coq.sh
 create mode 100755 tools/ci/ci-math-classes.sh
 create mode 100755 tools/ci/ci-metacoq.sh
 create mode 100755 tools/ci/ci-sf.sh
 create mode 100755 tools/ci/ci-tlc.sh

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} )
-- 
cgit v1.2.3


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


From f8c1284a3f5454964aa3002575159b2c9c3df34c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 7 Feb 2017 11:04:27 +0100
Subject: [travis] Enable 32bit test-suite + validate.

---
 .travis.yml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/.travis.yml b/.travis.yml
index 1dc08fb3db..7529870cdd 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -13,6 +13,7 @@ addons:
     packages:
     - opam
     - aspcud
+    - gcc-multilib
 env:
   global:
   - NJOBS=2
@@ -20,7 +21,9 @@ env:
   - COMPILER="system"
   # Main test suites
   matrix:
-  - TEST_TARGET="validate"           TW="travis_wait"
+  - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit"
+  - TEST_TARGET="validate"                           TW="travis_wait"
+  - TEST_TARGET="validate"   COMPILER="4.02.3+32bit" TW="travis_wait"
   - TEST_TARGET="ci-color"
   - TEST_TARGET="ci-compcert"
   - TEST_TARGET="ci-coquelicot"
-- 
cgit v1.2.3


From 2a59cdce8c142d451988709a3939b884c63993c9 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 7 Feb 2017 14:04:43 +0100
Subject: [travis] [External CI] GeoCoq

---
 .travis.yml         |  1 +
 Makefile.ci         |  2 +-
 dev/ci/ci-geocoq.sh | 12 ++++++++++++
 3 files changed, 14 insertions(+), 1 deletion(-)
 create mode 100755 dev/ci/ci-geocoq.sh

diff --git a/.travis.yml b/.travis.yml
index 7529870cdd..188e446007 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -28,6 +28,7 @@ env:
   - TEST_TARGET="ci-compcert"
   - TEST_TARGET="ci-coquelicot"
   - TEST_TARGET="ci-cpdt"
+  - TEST_TARGET="ci-geocoq"
   - TEST_TARGET="ci-fiat-crypto"
   - TEST_TARGET="ci-flocq"
   - TEST_TARGET="ci-hott"
diff --git a/Makefile.ci b/Makefile.ci
index d69028ce13..040144e6e8 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -1,6 +1,6 @@
 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-coquelicot ci-flocq ci-iris-coq ci-metacoq ci-geocoq
 
 .PHONY: $(CI_TARGETS)
 
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
new file mode 100755
index 0000000000..7b5811dc4a
--- /dev/null
+++ b/dev/ci/ci-geocoq.sh
@@ -0,0 +1,12 @@
+#!/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 && make -j ${NJOBS} )
-- 
cgit v1.2.3