[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.

2 files changed, 99 insertions, 5 deletions

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...
+