7 files changed, 98 insertions, 21 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/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'