6 files changed, 214 insertions, 7 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md
new file mode 100644
index 0000000000..f4423558cc
--- /dev/null
+++ b/dev/ci/README.md
@@ -0,0 +1,130 @@
+Continuous Integration for the Coq Proof Assistant
+==================================================
+
+Changes to Coq are systematically tested for regression and compatibility
+breakage on our Continuous Integration (CI) platforms *before* integration,
+so as to ensure better robustness and catch problems as early as possible.
+These tests include the compilation of several external libraries / plugins.
+
+This document contains information for both external library / plugin authors,
+who might be interested in having their development tested, and for Coq
+developers / contributors, who must ensure that they don't break these
+external developments accidentally.
+
+*Remark:* the CI policy outlined in this document is susceptible to evolve and
+specific accommodations are of course possible.
+
+Information for external library / plugin authors
+-------------------------------------------------
+
+You are encouraged to consider submitting your development for addition to
+our CI. This means that:
+
+- Any time that a proposed change is breaking your development, Coq developers
+  will send you patches to adapt it or, at the very least, will work with you
+  to see how to adapt it.
+
+On the condition that:
+
+- At the time of the submission, your development works with Coq master branch.
+
+- Your development is publicly available in a git repository and we can easily
+  send patches to you (e.g. through pull / merge requests).
+
+- You react in a timely manner to discuss / integrate those patches.
+
+- You do not push, to the branches that we test, commits that haven't been
+  first tested to compile with the corresponding branch(es) of Coq.
+
+- Your development compiles in less than 35 minutes with just two threads.
+  If this is not the case, consider adding a "lite" target that compiles just
+  part of it.
+
+In case you forget to comply with these last three conditions, we would reach
+out to you and give you a 30-day grace period during which your development
+would be moved into our "allow failure" category. At the end of the grace
+period, in the absence of progress, the development would be removed from our
+CI.
+
+### Add your development by submitting a pull request
+
+Add a new `ci-mydev.sh` script to [`dev/ci`](/dev/ci) (have a look at
+[`ci-coq-dpdgraph.sh`](/dev/ci/ci-coq-dpdgraph.sh) or
+[`ci-fiat-parsers.sh`](/dev/ci/ci-fiat-parsers.sh) for simple examples);
+set the corresponding variables in
+[`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh); add the corresponding
+target to [`Makefile.ci`](/Makefile.ci); add new jobs to
+[`.travis.yml`](/.travis.yml) and [`.gitlab-ci.yml`](/.gitlab-ci.yml) so that
+this new target is run. **Do not hesitate to submit an incomplete pull request
+if you need help to finish it.**
+
+You may also be interested in having your development tested in our
+performance benchmark. Currently this is done by providing an OPAM package
+in https://github.com/coq/opam-coq-archive and opening an issue at
+https://github.com/coq/coq-bench/issues.
+
+
+Information for developers
+--------------------------
+
+When you submit a pull request (PR) on Coq GitHub repository, this will
+automatically launch a battery of CI tests. The PR will not be integrated
+unless these tests pass.
+
+Currently, we have two CI platforms:
+
+- Travis is the main CI platform. It tests the compilation of Coq, of the
+  documentation, and of CoqIDE on Linux with several versions of OCaml /
+  camlp5, and with warnings as errors; it runs the test-suite and tests the
+  compilation of several external developments. It also tests the compilation
+  of Coq on OS X.
+
+- AppVeyor is used to test the compilation of Coq and run the test-suite on
+  Windows.
+
+You can anticipate the results of these tests prior to submitting your PR
+by having them run of your fork of Coq, on GitHub or GitLab. This can be
+especially helpful given that our Travis platform is often overloaded and
+therefore there can be a significant delay before these tests are actually
+run on your PR. To take advantage of this, simply create a Travis account
+and link it to your GitHub account, or activate the pipelines on your GitLab
+fork.
+
+You can also run one CI target locally (using `make ci-somedev`).
+
+Whenever your PR breaks tested developments, you should either adapt it
+so that it doesn't, or provide a branch fixing these developments (or at
+least work with the author of the development / other Coq developers to
+prepare these fixes). Then, add an overlay in
+[`dev/ci/user-overlays`](/dev/ci/user-overlays) (see the README there)
+in a separate commit in your PR.
+
+The process to merge your PR is then to submit PRs to the external
+development repositories, merge the latter first (if the fixes are
+backward-compatible), drop the overlay commit and merge the PR on Coq then.
+
+
+Travis specific information
+---------------------------
+
+Travis rebuilds all of Coq's executables and stdlib for each job. Coq
+is built with `./configure -local`, then used for the job's test.
+
+
+GitLab specific information
+---------------------------
+
+GitLab is set up to use the "build artifact" feature to avoid
+rebuilding Coq. In one job, Coq is built with `./configure -prefix
+install` and `make install` is run, then the `install` directory
+persists to and is used by the next jobs.
+
+Artifacts can also be downloaded from the GitLab repository.
+Currently, available artifacts are:
+- the Coq executables and stdlib, in three copies varying in
+  architecture and Ocaml version used to build Coq.
+- the Coq documentation, in two different copies varying in the OCaml
+  version used to build Coq
+
+As an exception to the above, jobs testing that compilation triggers
+no Ocaml warnings build Coq in parallel with other tests.
diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat
new file mode 100644
index 0000000000..ca6a5643c1
--- /dev/null
+++ b/dev/ci/appveyor.bat
@@ -0,0 +1,35 @@
+REM This script either runs the test suite with OPAM (if USEOPAM is true) or
+REM builds the Coq binary packages for windows (if USEOPAM is false).
+
+if %ARCH% == 32 (
+  SET ARCHLONG=i686
+  SET CYGROOT=C:\cygwin
+  SET SETUP=setup-x86.exe
+)
+
+if %ARCH% == 64 (
+  SET ARCHLONG=x86_64
+  SET CYGROOT=C:\cygwin64
+  SET SETUP=setup-x86_64.exe
+)
+
+SET CYGCACHE=%CYGROOT%\var\cache\setup
+SET APPVEYOR_BUILD_FOLDER_MFMT=%APPVEYOR_BUILD_FOLDER:\=/%
+SET APPVEYOR_BUILD_FOLDER_CFMT=%APPVEYOR_BUILD_FOLDER_MFMT:C:/=/cygdrive/c/%
+SET DESTCOQ=C:\coq%ARCH%_inst
+SET COQREGTESTING=Y
+
+if %USEOPAM% == false (
+  call %APPVEYOR_BUILD_FOLDER%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
+    -arch=%ARCH% -installer=Y -coqver=%APPVEYOR_BUILD_FOLDER_CFMT% ^
+    -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
+    -setup %CYGROOT%\%SETUP%
+  copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis
+  7z a coq-opensource-archive-%ARCHLONG%.zip %CYGROOT%\build\tarballs\*
+)
+
+if %USEOPAM% == true (
+  %CYGROOT%\%SETUP% -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% ^
+    -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time
+  %CYGROOT%/bin/bash -l %APPVEYOR_BUILD_FOLDER%/dev/ci/appveyor.sh
+)
diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh
new file mode 100644
index 0000000000..524a55a423
--- /dev/null
+++ b/dev/ci/appveyor.sh
@@ -0,0 +1,9 @@
+#!/bin/bash
+set -e -x
+wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.1/opam64.tar.xz
+tar -xf opam64.tar.xz
+bash opam64/install.sh
+opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp 4.02.3+mingw64c --switch 4.02.3+mingw64c
+eval $(opam config env)
+opam install -y ocamlfind camlp5
+cd $APPVEYOR_BUILD_FOLDER && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= && make validate
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 4b3b44875f..8e7265969b 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -114,7 +114,9 @@
 ########################################################################
 # SF
 ########################################################################
-: ${sf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/current/sf.tgz}
+: ${sf_lf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/lf-current/lf.tgz}
+: ${sf_plf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/plf-current/plf.tgz}
+: ${sf_vfa_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/vfa-current/vfa.tgz}
 
 ########################################################################
 # TLC
@@ -125,5 +127,5 @@
 ########################################################################
 # Bignums
 ########################################################################
-: ${bignums_CI_BRANCH:=master}
-: ${bignums_CI_GITURL:=https://github.com/coq/bignums.git}
+: ${bignums_CI_BRANCH:=fix-thunk-printer}
+: ${bignums_CI_GITURL:=https://github.com/ppedrot/bignums.git}
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index 6e6c7012b7..272041205c 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -4,11 +4,18 @@ ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
 # XXX: Needs fixing to properly set the build directory.
-wget ${sf_CI_TARURL}
-tar xvfz sf.tgz
+wget ${sf_lf_CI_TARURL}
+wget ${sf_plf_CI_TARURL}
+wget ${sf_vfa_CI_TARURL}
+tar xvfz lf.tgz
+tar xvfz plf.tgz
+tar xvfz vfa.tgz
 
-sed -i.bak '15i From Coq Require Extraction.' sf/Extraction.v
+sed -i.bak '1i From Coq Require Extraction.' lf/Extraction.v
+sed -i.bak '1i From Coq Require Extraction.' vfa/Extract.v
 
-( cd sf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make )
+( cd lf && make clean && make )
 
+( cd plf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make )
 
+( cd vfa && make clean && make )
diff --git a/dev/ci/ci-wrapper.sh b/dev/ci/ci-wrapper.sh
new file mode 100755
index 0000000000..96acc5a11c
--- /dev/null
+++ b/dev/ci/ci-wrapper.sh
@@ -0,0 +1,24 @@
+#!/usr/bin/env bash
+
+# Use this script to preserve the exit code of $CI_SCRIPT when piping
+# it to `tee time-of-build.log`.  We have a separate script, because
+# this only works in bash, which we don't require project-wide.
+
+set -eo pipefail
+
+function travis_fold {
+    if [ -n "${TRAVIS}" ];
+    then
+	echo "travis_fold:$1:$2"
+    fi
+}
+
+CI_SCRIPT="$1"
+DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
+# assume this script is in dev/ci/, cd to the root Coq directory
+cd "${DIR}/../.."
+
+"${DIR}/${CI_SCRIPT}" 2>&1 | tee time-of-build.log
+travis_fold 'start' 'coq.test.timing' && echo 'Aggregating timing log...'
+python ./tools/make-one-time-file.py time-of-build.log
+travis_fold 'end' 'coq.test.timing'