9 files changed, 240 insertions, 29 deletions
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
index b2efe2ddd4..a420b5d8bb 100644
--- a/dev/build/windows/MakeCoq_MinGW.bat
+++ b/dev/build/windows/MakeCoq_MinGW.bat
@@ -344,6 +344,9 @@ IF EXIST "%CYGWIN_INSTALLDIR_WFMT%\etc\setup\installed.db" (
 IF NOT "%CYGWIN_QUIET%" == "Y" (
   SET RUNSETUP=Y
 )
+IF "%COQREGTESTING%" == "Y" (
+  SET RUNSETUP=Y
+)
 
 IF "%RUNSETUP%"=="Y" (
   %SETUP% ^
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index e179239514..f3e4cec0b9 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1058,13 +1058,18 @@ function copq_coq_gtk {
     install_rec  "$PREFIX/share/themes/" '*'                          "$PREFIXCOQ/share/themes"
     
     # This below item look like a bug in make install
+    if [ -d "$PREFIXCOQ/share/coq/" ] ; then
+      COQSHARE="$PREFIXCOQ/share/coq/"
+    else
+      COQSHARE="$PREFIXCOQ/share/"
+    fi
     if [[ ! $COQ_VERSION == 8.4* ]] ; then
-      mv "$PREFIXCOQ/share/coq/"*.lang "$PREFIXCOQ/share/gtksourceview-2.0/language-specs"
-      mv "$PREFIXCOQ/share/coq/"*.xml  "$PREFIXCOQ/share/gtksourceview-2.0/styles"
+      mv "$COQSHARE"*.lang "$PREFIXCOQ/share/gtksourceview-2.0/language-specs"
+      mv "$COQSHARE"*.xml  "$PREFIXCOQ/share/gtksourceview-2.0/styles"
     fi
     mkdir -p "$PREFIXCOQ/ide"
-    mv "$PREFIXCOQ/share/coq/"*.png  "$PREFIXCOQ/ide"
-    rmdir "$PREFIXCOQ/share/coq"
+    mv "$COQSHARE"*.png  "$PREFIXCOQ/ide"
+    rmdir "$PREFIXCOQ/share/coq" || true
   fi
 }
 
@@ -1119,11 +1124,11 @@ function make_coq {
   then
     if [ "$INSTALLMODE" == "relocatable" ]; then
       # HACK: for relocatable builds, first configure with ./, then build but before install reconfigure with the real target path
-      logn configure ./configure -debug -with-doc no -prefix ./ -libdir ./lib -mandir ./man
+      ./configure -with-doc no -prefix ./ -libdir ./lib -mandir ./man
     elif [ "$INSTALLMODE" == "absolute" ]; then
-      logn configure ./configure -debug -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man"
+      ./configure -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man"
     else
-      logn configure ./configure -debug -with-doc no -prefix "$PREFIXCOQ"
+      ./configure -with-doc no -prefix "$PREFIXCOQ"
     fi
 
     # The windows resource compiler binary name is hard coded
@@ -1134,17 +1139,17 @@ function make_coq {
     if [[ $COQ_VERSION == 8.4* ]] ; then
       log1 make
     else
-      log1 make $MAKE_OPT
+      make $MAKE_OPT
     fi
     
     if [ "$INSTALLMODE" == "relocatable" ]; then
-      logn reconfigure ./configure -debug -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man"
+      ./configure -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man"
     fi
 
-    log2 make install
-    log1 copy_coq_dlls
+    make install
+    copy_coq_dlls
     if [ "$INSTALLOCAML" == "Y" ]; then
-      log1 copy_coq_objects
+      copy_coq_objects
     fi
     
     copq_coq_gtk
@@ -1267,7 +1272,7 @@ function get_cygwin_mingw_sources {
 function make_coq_installer {
   make_coq
   make_mingw_make
-  # get_cygwin_mingw_sources
+  get_cygwin_mingw_sources
 
   # Prepare the file lists for the installer. We created to file list dumps of the target folder during the build:
   # ocaml: ocaml + menhir + camlp5 + findlib
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/build/windows/appveyor.sh b/dev/ci/appveyor.sh
index 53f7a23466..524a55a423 100644
--- a/dev/build/windows/appveyor.sh
+++ b/dev/ci/appveyor.sh
@@ -1,8 +1,9 @@
 #!/bin/bash
 set -e -x
-wget $opam_url
+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'
diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.md
index 3e2b435b3e..7e9373b294 100644
--- a/dev/doc/debugging.txt
+++ b/dev/doc/debugging.md
@@ -25,8 +25,9 @@ Debugging from Coq toplevel using Caml trace mechanism
 Debugging from Caml debugger
 ============================
 
-   Needs tuareg mode in Emacs
-   Coq must be configured with -debug and -local (./configure -debug -local)
+   Requires [Tuareg mode](https://github.com/ocaml/tuareg) in Emacs.\
+   Coq must be configured with `-local` (`./configure -local`) and the
+   byte-code version of `coqtop` must have been generated with `make byte`.
 
    1. M-x camldebug
    2. give the binary name bin/coqtop.byte
@@ -53,6 +54,9 @@ Debugging from Caml debugger
      of each of error* functions or anomaly* functions in lib/util.ml
    - If "source db" fails, do a "make printers" and try again (it should build
      top_printers.cmo and the core cma files).
+   - If you have the OCAMLRUNPARAM environment variable set, Coq may hang on
+     startup when run from the debugger. If this happens, unset the variable,
+     re-start Emacs, and run the debugger again.
 
 Global gprof-based profiling
 ============================
@@ -65,14 +69,14 @@ Global gprof-based profiling
 Per function profiling
 ======================
 
-   1. To profile function foo in file bar.ml, add the following lines, just
-      after the definition of the function:
+   To profile function foo in file bar.ml, add the following lines, just
+   after the definition of the function:
 
      let fookey = Profile.declare_profile "foo";;
      let foo a b c = Profile.profile3 fookey foo a b c;;
 
-     where foo is assumed to have three arguments (adapt using
-     Profile.profile1, Profile. profile2, etc).
+   where foo is assumed to have three arguments (adapt using
+   Profile.profile1, Profile. profile2, etc).
 
-     This has the effect to cumulate the time passed in foo under a
-     line of name "foo" which is displayed at the time coqtop exits.
+   This has the effect to cumulate the time passed in foo under a
+   line of name "foo" which is displayed at the time coqtop exits.