14 files changed, 1066 insertions, 656 deletions
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
index 61cf6bc4cc..33feeed45c 100755
--- a/dev/build/windows/MakeCoq_MinGW.bat
+++ b/dev/build/windows/MakeCoq_MinGW.bat
@@ -1,488 +1,488 @@
-@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== NOTES ==========
-
-REM For Cygwin setup command line options
-REM see https://cygwin.com/faq/faq.html#faq.setup.cli
-
-REM ========== DEFAULT VALUES FOR PARAMETERS ==========
-
-REM For a description of all parameters, see ReadMe.txt
-
-SET BATCHFILE=%~0
-SET BATCHDIR=%~dp0
-
-REM see -arch in ReadMe.txt, but values are x86_64 or i686 (not 64 or 32)
-SET ARCH=x86_64
-
-REM see -mode in ReadMe.txt
-SET INSTALLMODE=absolute
-
-REM see -installer in ReadMe.txt
-SET MAKEINSTALLER=N
-
-REM see -ocaml in ReadMe.txt
-SET INSTALLOCAML=N
-
-REM see -make in ReadMe.txt
-SET INSTALLMAKE=N
-
-REM see -destcyg in ReadMe.txt
-SET DESTCYG=C:\bin\cygwin_coq
-
-REM see -destcoq in ReadMe.txt
-SET DESTCOQ=C:\bin\coq
-
-REM see -setup in ReadMe.txt
-SET SETUP=setup-x86_64.exe
-
-REM see -proxy in ReadMe.txt
-IF DEFINED HTTP_PROXY (
-  SET PROXY=%HTTP_PROXY:http://=%
-) else (
-  REM One can't set a variable to empty in DOS, but you can set it to a space this way.
-  REM The quotes are just there to make the space visible and to protect from "remove trailing spaces".
-  SET "PROXY= "
-)
-
-REM see -cygrepo in ReadMe.txt
-SET CYGWIN_REPOSITORY=http://ftp.inf.tu-dresden.de/software/windows/cygwin32
-
-REM see -cygcache in ReadMe.txt
-SET CYGWIN_LOCAL_CACHE_WFMT=%BATCHDIR%cygwin_cache
-
-REM see -cyglocal in ReadMe.txt
-SET CYGWIN_FROM_CACHE=N
-
-REM see -cygquiet in ReadMe.txt
-SET CYGWIN_QUIET=Y
-
-REM see -srccache in ReadMe.txt
-SET SOURCE_LOCAL_CACHE_WFMT=%BATCHDIR%source_cache
-
-REM see -coqver in ReadMe.txt
-SET COQ_VERSION=8.5pl3
-
-REM see -gtksrc in ReadMe.txt
-SET GTK_FROM_SOURCES=N
-
-REM see -threads in ReadMe.txt
-SET MAKE_THREADS=8
-
-REM see -addon in ReadMe.txt
-SET "COQ_ADDONS= "
-
-REM ========== PARSE COMMAND LINE PARAMETERS ==========
-
-SHIFT
-
-:Parse
-
-IF "%~0" == "-arch" (
-  IF "%~1" == "32" (
-    SET ARCH=i686
-    SET SETUP=setup-x86.exe
-  ) ELSE (
-    IF "%~1" == "64" (
-      SET ARCH=x86_64
-      SET SETUP=setup-x86_64.exe
-    ) ELSE (
-      ECHO "Invalid -arch, valid are 32 and 64"
-      GOTO :EOF
-    )
-  )
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-mode" (
-  IF "%~1" == "mingwincygwin" (
-    SET INSTALLMODE=%~1
-  ) ELSE (
-    IF "%~1" == "absolute" (
-      SET INSTALLMODE=%~1
-    ) ELSE (
-      IF "%~1" == "relocatable" (
-        SET INSTALLMODE=%~1
-      ) ELSE (
-        ECHO "Invalid -mode, valid are mingwincygwin, absolute and relocatable"
-        GOTO :EOF
-      )
-    )
-  )
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-installer" (
-  SET MAKEINSTALLER=%~1
-  CALL :CheckYN -installer %~1 || GOTO ErrorExit
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-ocaml" (
-  SET INSTALLOCAML=%~1
-  CALL :CheckYN -installer %~1 || GOTO ErrorExit
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-make" (
-  SET INSTALLMAKE=%~1
-  CALL :CheckYN -installer %~1 || GOTO ErrorExit
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-destcyg" (
-  SET DESTCYG=%~1
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-destcoq" (
-  SET DESTCOQ=%~1
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-setup" (
-  SET SETUP=%~1
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-proxy" (
-  SET PROXY=%~1
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-cygrepo" (
-  SET CYGWIN_REPOSITORY=%~1
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-cygcache" (
-  SET CYGWIN_LOCAL_CACHE_WFMT=%~1
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-cyglocal" (
-  SET CYGWIN_FROM_CACHE=%~1
-  CALL :CheckYN -cyglocal %~1 || GOTO ErrorExit
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-cygquiet" (
-  SET CYGWIN_QUIET=%~1
-  CALL :CheckYN -cygquiet %~1 || GOTO ErrorExit
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-srccache" (
-  SET SOURCE_LOCAL_CACHE_WFMT=%~1
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-coqver" (
-  SET COQ_VERSION=%~1
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-gtksrc" (
-  SET GTK_FROM_SOURCES=%~1
-  CALL :CheckYN -gtksrc %~1 || GOTO ErrorExit
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-threads" (
-  SET MAKE_THREADS=%~1
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-IF "%~0" == "-addon" (
-  SET "COQ_ADDONS=%COQ_ADDONS% %~1"
-  SHIFT
-  SHIFT
-  GOTO Parse
-)
-
-
-IF NOT "%~0" == "" (
-  ECHO Install cygwin and download, compile and install OCaml and Coq for MinGW
-  ECHO !!! Illegal parameter %~0
-  ECHO Usage:
-  ECHO MakeCoq_MinGW
-  CALL :PrintPars
-  GOTO :EOF
-)
-
-IF NOT EXIST %SETUP% (
-  ECHO The cygwin setup program %SETUP% doesn't exist. You must download it from https://cygwin.com/install.html.
-  ECHO If the setup is in a different folder, set the full path to %SETUP% using the -setup option.
-  GOTO :EOF
-)
-
-REM ========== ADJUST PARAMETERS ==========
-
-IF "%INSTALLMODE%" == "mingwincygwin" (
-  SET DESTCOQ=%DESTCYG%\usr\%ARCH%-w64-mingw32\sys-root\mingw
-)
-
-IF "%MAKEINSTALLER%" == "Y" (
-  SET INSTALLMODE=relocatable
-)
-
-REM ========== CONFIRM PARAMETERS ==========
-
-CALL :PrintPars
-REM Note: DOS batch replaces variables on parsing, so one can't use a variable just set in an () block
-IF "%COQREGTESTING%"=="Y" (GOTO DontAsk)
-  SET /p ANSWER="Is this correct? y/n "
-  IF NOT "%ANSWER%"=="y" (GOTO :EOF)
-:DontAsk
-
-REM ========== DERIVED VARIABLES ==========
-
-SET CYGWIN_INSTALLDIR_WFMT=%DESTCYG%
-SET RESULT_INSTALLDIR_WFMT=%DESTCOQ%
-SET TARGET_ARCH=%ARCH%-w64-mingw32
-SET BASH=%CYGWIN_INSTALLDIR_WFMT%\bin\bash
-
-REM Convert pathes to various formats
-REM WFMT = windows format (C:\..)          Used in this batch file.
-REM CFMT = cygwin format (\cygdrive\c\..)  Used for Cygwin PATH varible, which is : separated, so C: doesn't work.
-REM MFMT = MinGW format (C:/...)           Used for the build, because \\ requires escaping. Mingw can handle \ and /.
-
-SET CYGWIN_INSTALLDIR_MFMT=%CYGWIN_INSTALLDIR_WFMT:\=/%
-SET RESULT_INSTALLDIR_MFMT=%RESULT_INSTALLDIR_WFMT:\=/%
-SET SOURCE_LOCAL_CACHE_MFMT=%SOURCE_LOCAL_CACHE_WFMT:\=/%
-
-SET CYGWIN_INSTALLDIR_CFMT=%CYGWIN_INSTALLDIR_MFMT:C:/=/cygdrive/c/%
-SET RESULT_INSTALLDIR_CFMT=%RESULT_INSTALLDIR_MFMT:C:/=/cygdrive/c/%
-SET SOURCE_LOCAL_CACHE_CFMT=%SOURCE_LOCAL_CACHE_MFMT:C:/=/cygdrive/c/%
-
-SET CYGWIN_INSTALLDIR_CFMT=%CYGWIN_INSTALLDIR_CFMT:D:/=/cygdrive/d/%
-SET RESULT_INSTALLDIR_CFMT=%RESULT_INSTALLDIR_CFMT:D:/=/cygdrive/d/%
-SET SOURCE_LOCAL_CACHE_CFMT=%SOURCE_LOCAL_CACHE_CFMT:D:/=/cygdrive/d/%
-
-SET CYGWIN_INSTALLDIR_CFMT=%CYGWIN_INSTALLDIR_CFMT:E:/=/cygdrive/e/%
-SET RESULT_INSTALLDIR_CFMT=%RESULT_INSTALLDIR_CFMT:E:/=/cygdrive/e/%
-SET SOURCE_LOCAL_CACHE_CFMT=%SOURCE_LOCAL_CACHE_CFMT:E:/=/cygdrive/e/%
-
-ECHO CYGWIN INSTALL DIR (WIN)    = %CYGWIN_INSTALLDIR_WFMT%
-ECHO CYGWIN INSTALL DIR (MINGW)  = %CYGWIN_INSTALLDIR_MFMT%
-ECHO CYGWIN INSTALL DIR (CYGWIN) = %CYGWIN_INSTALLDIR_CFMT%
-ECHO RESULT INSTALL DIR (WIN)    = %RESULT_INSTALLDIR_WFMT%
-ECHO RESULT INSTALL DIR (MINGW)  = %RESULT_INSTALLDIR_MFMT%
-ECHO RESULT INSTALL DIR (CYGWIN) = %RESULT_INSTALLDIR_CFMT%
-
-REM WARNING: Add a space after the = in case you want set this to empty, otherwise the variable will be unset
-SET MAKE_OPT=-j %MAKE_THREADS%
-
-REM ========== DERIVED CYGWIN SETUP OPTIONS ==========
-
-REM One can't set a variable to empty in DOS, but you can set it to a space this way.
-REM The quotes are just there to make the space visible and to protect from "remove trailing spaces".
-SET "CYGWIN_OPT= "
-
-IF "%CYGWIN_FROM_CACHE%" == "Y" (
-  SET CYGWIN_OPT= %CYGWIN_OPT% -L
-)
-
-IF "%CYGWIN_QUIET%" == "Y" (
-  SET CYGWIN_OPT= %CYGWIN_OPT% -q --no-admin
-)
-
-IF "%GTK_FROM_SOURCES%"=="N" (
-  SET CYGWIN_OPT= %CYGWIN_OPT% -P mingw64-%ARCH%-gtk2.0,mingw64-%ARCH%-gtksourceview2.0
-)
-
-REM Cygwin setup sets proper ACLs (permissions) for folders it CREATES.
-REM Otherwise chmod won't work and e.g. the ocaml build will fail.
-REM Cygwin setup does not touch the ACLs of existing folders.
-
-REM Run Cygwin Setup
-
-SET RUNSETUP=Y
-IF EXIST "%CYGWIN_INSTALLDIR_WFMT%\etc\setup\installed.db" (
-  SET RUNSETUP=N
-)
-IF NOT "%CYGWIN_QUIET%" == "Y" (
-  SET RUNSETUP=Y
-)
-
-IF "%COQREGTESTING%" == "Y" (
-  ECHO "========== REMOVE EXISTING CYGWIN =========="
-  DEL /S /F /Q "%CYGWIN_INSTALLDIR_WFMT%" > NUL
-  SET RUNSETUP=Y
-)
-
-SET "EXTRAPACKAGES= "
-
-IF NOT "%APPVEYOR%" == "True" (
-  SET EXTRAPACKAGES=-P wget,curl,git,gcc-core,gcc-g++,automake1.5
-)
-
-ECHO "========== INSTALL CYGWIN =========="
-
-IF "%RUNSETUP%"=="Y" (
-  %SETUP% ^
-    --proxy "%PROXY%" ^
-    --site "%CYGWIN_REPOSITORY%" ^
-    --root "%CYGWIN_INSTALLDIR_WFMT%" ^
-    --local-package-dir "%CYGWIN_LOCAL_CACHE_WFMT%" ^
-    --no-shortcuts ^
-    %CYGWIN_OPT% ^
-    -P make,unzip ^
-    -P gdb,liblzma5 ^
-    -P patch,automake1.14 ^
-    -P mingw64-%ARCH%-binutils,mingw64-%ARCH%-gcc-core,mingw64-%ARCH%-gcc-g++,mingw64-%ARCH%-pkg-config,mingw64-%ARCH%-windows_default_manifest ^
-    -P mingw64-%ARCH%-headers,mingw64-%ARCH%-runtime,mingw64-%ARCH%-pthreads,mingw64-%ARCH%-zlib ^
-    -P libiconv-devel,libunistring-devel,libncurses-devel ^
-    -P gettext-devel,libgettextpo-devel ^
-    -P libglib2.0-devel,libgdk_pixbuf2.0-devel ^
-    -P libfontconfig1 ^
-    -P gtk-update-icon-cache ^
-    -P libtool,automake ^
-    -P intltool ^
-    %EXTRAPACKAGES% ^
-    || GOTO ErrorExit
-
-  MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build"
-  MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\buildlogs"
-)
-
-IF NOT "%CYGWIN_QUIET%" == "Y" (
-  REM Like most setup programs, cygwin setup starts the real setup as a separate process, so wait for it.
-  REM This is not required with the -cygquiet=Y and the resulting --no-admin option.
-  :waitsetup
-  tasklist /fi "imagename eq %SETUP%" | find ":" > NUL
-  IF ERRORLEVEL 1 GOTO waitsetup
-)
-
-ECHO ========== CONFIGURE CYGWIN USER ACCOUNT ==========
-
-REM In case this batch file is called from a cygwin bash (e.g. a git repo) we need to clear
-REM HOME (otherwise we get to the home directory of the other installation)
-REM PROFILEREAD (this is set to true if the /etc/profile has been read, which creates user)
-SET "HOME="
-SET "PROFILEREAD="
-
-copy "%BATCHDIR%\configure_profile.sh" "%CYGWIN_INSTALLDIR_WFMT%\var\tmp" || GOTO ErrorExit
-%BASH% --login "%CYGWIN_INSTALLDIR_CFMT%\var\tmp\configure_profile.sh" "%PROXY%" || GOTO ErrorExit
-
-ECHO ========== BUILD COQ ==========
-
-MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build"
-MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\patches"
-
-COPY "%BATCHDIR%\makecoq_mingw.sh" "%CYGWIN_INSTALLDIR_WFMT%\build" || GOTO ErrorExit
-COPY "%BATCHDIR%\patches_coq\*.*" "%CYGWIN_INSTALLDIR_WFMT%\build\patches" || GOTO ErrorExit
-
-%BASH% --login "%CYGWIN_INSTALLDIR_CFMT%\build\makecoq_mingw.sh" || GOTO ErrorExit
-
-ECHO ========== FINISHED ==========
-
-GOTO :EOF
-
-ECHO ========== BATCH FUNCTIONS ==========
-
-:PrintPars
-  REM  01234567890123456789012345678901234567890123456789012345678901234567890123456789
-  ECHO -arch     ^<i686 or x86_64^> Set cygwin, ocaml and coq to 32 or 64 bit
-  ECHO -mode     ^<mingwincygwin = install coq in default cygwin mingw sysroot^>
-  ECHO           ^<absoloute = install coq in -destcoq absulute path^>
-  ECHO           ^<relocatable = install relocatable coq in -destcoq path^>
-  ECHO -installer^<Y or N^> create a windows installer (will be in /build/coq/dev/nsis)
-  ECHO -ocaml    ^<Y or N^> install OCaml in Coq folder (Y) or just in cygwin folder (N)
-  ECHO -make     ^<Y or N^> install GNU Make in Coq folder (Y) or not (N)
-  ECHO -destcyg  ^<path to cygwin destination folder^>
-  ECHO -destcoq  ^<path to coq destination folder (mode=absoloute/relocatable)^>
-  ECHO -setup    ^<cygwin setup program name^> (auto adjusted to -arch)
-  ECHO -proxy    ^<internet proxy^>
-  ECHO -cygrepo  ^<cygwin download repository^>
-  ECHO -cygcache ^<local cygwin repository/cache^>
-  ECHO -cyglocal ^<Y or N^> install cygwin from cache
-  ECHO -cygquiet ^<Y or N^> install cygwin without user interaction
-  ECHO -srccache ^<local source code repository/cache^>
-  ECHO -coqver   ^<Coq version to install^>
-  ECHO -gtksrc   ^<Y or N^> build GTK ^(90 min^) or use cygwin version
-  ECHO -threads  ^<1..N^> Number of make threads
-  ECHO -addon    ^<name^>  Enable building selected addon (can be repeated)
-  ECHO(
-  ECHO See ReadMe.txt for a detailed description of all parameters
-  ECHO(
-  ECHO Parameter values (default or currently set):
-  ECHO -arch     = %ARCH%
-  ECHO -mode     = %INSTALLMODE%
-  ECHO -ocaml    = %INSTALLOCAML%
-  ECHO -installer= %MAKEINSTALLER%
-  ECHO -make     = %INSTALLMAKE%
-  ECHO -destcyg  = %DESTCYG%
-  ECHO -destcoq  = %DESTCOQ%
-  ECHO -setup    = %SETUP%
-  ECHO -proxy    = %PROXY%
-  ECHO -cygrepo  = %CYGWIN_REPOSITORY%
-  ECHO -cygcache = %CYGWIN_LOCAL_CACHE_WFMT%
-  ECHO -cyglocal = %CYGWIN_FROM_CACHE%
-  ECHO -cygquiet = %CYGWIN_QUIET%
-  ECHO -srccache = %SOURCE_LOCAL_CACHE_WFMT%
-  ECHO -coqver   = %COQ_VERSION%
-  ECHO -gtksrc   = %GTK_FROM_SOURCES%
-  ECHO -threads  = %MAKE_THREADS%
-  ECHO -addon    = %COQ_ADDONS%
-  GOTO :EOF
-
-:CheckYN
-  REM Reset errorlevel to 0
-  CMD /c "EXIT /b 0"
-  IF "%2" == "Y" (
-    REM OK Y
-  ) ELSE IF "%2" == "N" (
-    REM OK N
-  ) ELSE (
-    ECHO ERROR Parameter %1 must be Y or N, but is %2
-    GOTO ErrorExit
-  )
-  GOTO :EOF
-
-:ErrorExit
-  ECHO ERROR MakeCoq_MinGW.bat failed
-  EXIT /b 1
+@ECHO OFF
+
+REM ========== COPYRIGHT/COPYLEFT ==========
+
+REM (C) 2016 Intel Deutschland GmbH
+REM Author: Michael Soegtrop
+
+REM Released to the public by Intel under the
+REM GNU Lesser General Public License Version 2.1 or later
+REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
+
+REM ========== NOTES ==========
+
+REM For Cygwin setup command line options
+REM see https://cygwin.com/faq/faq.html#faq.setup.cli
+
+REM ========== DEFAULT VALUES FOR PARAMETERS ==========
+
+REM For a description of all parameters, see ReadMe.txt
+
+SET BATCHFILE=%~0
+SET BATCHDIR=%~dp0
+
+REM see -arch in ReadMe.txt, but values are x86_64 or i686 (not 64 or 32)
+SET ARCH=x86_64
+
+REM see -mode in ReadMe.txt
+SET INSTALLMODE=absolute
+
+REM see -installer in ReadMe.txt
+SET MAKEINSTALLER=N
+
+REM see -ocaml in ReadMe.txt
+SET INSTALLOCAML=N
+
+REM see -make in ReadMe.txt
+SET INSTALLMAKE=N
+
+REM see -destcyg in ReadMe.txt
+SET DESTCYG=C:\bin\cygwin_coq
+
+REM see -destcoq in ReadMe.txt
+SET DESTCOQ=C:\bin\coq
+
+REM see -setup in ReadMe.txt
+SET SETUP=setup-x86_64.exe
+
+REM see -proxy in ReadMe.txt
+IF DEFINED HTTP_PROXY (
+  SET PROXY=%HTTP_PROXY:http://=%
+) else (
+  REM One can't set a variable to empty in DOS, but you can set it to a space this way.
+  REM The quotes are just there to make the space visible and to protect from "remove trailing spaces".
+  SET "PROXY= "
+)
+
+REM see -cygrepo in ReadMe.txt
+SET CYGWIN_REPOSITORY=http://ftp.inf.tu-dresden.de/software/windows/cygwin32
+
+REM see -cygcache in ReadMe.txt
+SET CYGWIN_LOCAL_CACHE_WFMT=%BATCHDIR%cygwin_cache
+
+REM see -cyglocal in ReadMe.txt
+SET CYGWIN_FROM_CACHE=N
+
+REM see -cygquiet in ReadMe.txt
+SET CYGWIN_QUIET=Y
+
+REM see -srccache in ReadMe.txt
+SET SOURCE_LOCAL_CACHE_WFMT=%BATCHDIR%source_cache
+
+REM see -coqver in ReadMe.txt
+SET COQ_VERSION=8.5pl3
+
+REM see -gtksrc in ReadMe.txt
+SET GTK_FROM_SOURCES=N
+
+REM see -threads in ReadMe.txt
+SET MAKE_THREADS=8
+
+REM see -addon in ReadMe.txt
+SET "COQ_ADDONS= "
+
+REM ========== PARSE COMMAND LINE PARAMETERS ==========
+
+SHIFT
+
+:Parse
+
+IF "%~0" == "-arch" (
+  IF "%~1" == "32" (
+    SET ARCH=i686
+    SET SETUP=setup-x86.exe
+  ) ELSE (
+    IF "%~1" == "64" (
+      SET ARCH=x86_64
+      SET SETUP=setup-x86_64.exe
+    ) ELSE (
+      ECHO "Invalid -arch, valid are 32 and 64"
+      GOTO :EOF
+    )
+  )
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-mode" (
+  IF "%~1" == "mingwincygwin" (
+    SET INSTALLMODE=%~1
+  ) ELSE (
+    IF "%~1" == "absolute" (
+      SET INSTALLMODE=%~1
+    ) ELSE (
+      IF "%~1" == "relocatable" (
+        SET INSTALLMODE=%~1
+      ) ELSE (
+        ECHO "Invalid -mode, valid are mingwincygwin, absolute and relocatable"
+        GOTO :EOF
+      )
+    )
+  )
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-installer" (
+  SET MAKEINSTALLER=%~1
+  CALL :CheckYN -installer %~1 || GOTO ErrorExit
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-ocaml" (
+  SET INSTALLOCAML=%~1
+  CALL :CheckYN -installer %~1 || GOTO ErrorExit
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-make" (
+  SET INSTALLMAKE=%~1
+  CALL :CheckYN -installer %~1 || GOTO ErrorExit
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-destcyg" (
+  SET DESTCYG=%~1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-destcoq" (
+  SET DESTCOQ=%~1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-setup" (
+  SET SETUP=%~1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-proxy" (
+  SET PROXY=%~1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-cygrepo" (
+  SET CYGWIN_REPOSITORY=%~1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-cygcache" (
+  SET CYGWIN_LOCAL_CACHE_WFMT=%~1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-cyglocal" (
+  SET CYGWIN_FROM_CACHE=%~1
+  CALL :CheckYN -cyglocal %~1 || GOTO ErrorExit
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-cygquiet" (
+  SET CYGWIN_QUIET=%~1
+  CALL :CheckYN -cygquiet %~1 || GOTO ErrorExit
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-srccache" (
+  SET SOURCE_LOCAL_CACHE_WFMT=%~1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-coqver" (
+  SET COQ_VERSION=%~1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-gtksrc" (
+  SET GTK_FROM_SOURCES=%~1
+  CALL :CheckYN -gtksrc %~1 || GOTO ErrorExit
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-threads" (
+  SET MAKE_THREADS=%~1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%~0" == "-addon" (
+  SET "COQ_ADDONS=%COQ_ADDONS% %~1"
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+
+IF NOT "%~0" == "" (
+  ECHO Install cygwin and download, compile and install OCaml and Coq for MinGW
+  ECHO !!! Illegal parameter %~0
+  ECHO Usage:
+  ECHO MakeCoq_MinGW
+  CALL :PrintPars
+  GOTO :EOF
+)
+
+IF NOT EXIST %SETUP% (
+  ECHO The cygwin setup program %SETUP% doesn't exist. You must download it from https://cygwin.com/install.html.
+  ECHO If the setup is in a different folder, set the full path to %SETUP% using the -setup option.
+  GOTO :EOF
+)
+
+REM ========== ADJUST PARAMETERS ==========
+
+IF "%INSTALLMODE%" == "mingwincygwin" (
+  SET DESTCOQ=%DESTCYG%\usr\%ARCH%-w64-mingw32\sys-root\mingw
+)
+
+IF "%MAKEINSTALLER%" == "Y" (
+  SET INSTALLMODE=relocatable
+)
+
+REM ========== CONFIRM PARAMETERS ==========
+
+CALL :PrintPars
+REM Note: DOS batch replaces variables on parsing, so one can't use a variable just set in an () block
+IF "%COQREGTESTING%"=="Y" (GOTO DontAsk)
+  SET /p ANSWER="Is this correct? y/n "
+  IF NOT "%ANSWER%"=="y" (GOTO :EOF)
+:DontAsk
+
+REM ========== DERIVED VARIABLES ==========
+
+SET CYGWIN_INSTALLDIR_WFMT=%DESTCYG%
+SET RESULT_INSTALLDIR_WFMT=%DESTCOQ%
+SET TARGET_ARCH=%ARCH%-w64-mingw32
+SET BASH=%CYGWIN_INSTALLDIR_WFMT%\bin\bash
+
+REM Convert pathes to various formats
+REM WFMT = windows format (C:\..)          Used in this batch file.
+REM CFMT = cygwin format (\cygdrive\c\..)  Used for Cygwin PATH varible, which is : separated, so C: doesn't work.
+REM MFMT = MinGW format (C:/...)           Used for the build, because \\ requires escaping. Mingw can handle \ and /.
+
+SET CYGWIN_INSTALLDIR_MFMT=%CYGWIN_INSTALLDIR_WFMT:\=/%
+SET RESULT_INSTALLDIR_MFMT=%RESULT_INSTALLDIR_WFMT:\=/%
+SET SOURCE_LOCAL_CACHE_MFMT=%SOURCE_LOCAL_CACHE_WFMT:\=/%
+
+SET CYGWIN_INSTALLDIR_CFMT=%CYGWIN_INSTALLDIR_MFMT:C:/=/cygdrive/c/%
+SET RESULT_INSTALLDIR_CFMT=%RESULT_INSTALLDIR_MFMT:C:/=/cygdrive/c/%
+SET SOURCE_LOCAL_CACHE_CFMT=%SOURCE_LOCAL_CACHE_MFMT:C:/=/cygdrive/c/%
+
+SET CYGWIN_INSTALLDIR_CFMT=%CYGWIN_INSTALLDIR_CFMT:D:/=/cygdrive/d/%
+SET RESULT_INSTALLDIR_CFMT=%RESULT_INSTALLDIR_CFMT:D:/=/cygdrive/d/%
+SET SOURCE_LOCAL_CACHE_CFMT=%SOURCE_LOCAL_CACHE_CFMT:D:/=/cygdrive/d/%
+
+SET CYGWIN_INSTALLDIR_CFMT=%CYGWIN_INSTALLDIR_CFMT:E:/=/cygdrive/e/%
+SET RESULT_INSTALLDIR_CFMT=%RESULT_INSTALLDIR_CFMT:E:/=/cygdrive/e/%
+SET SOURCE_LOCAL_CACHE_CFMT=%SOURCE_LOCAL_CACHE_CFMT:E:/=/cygdrive/e/%
+
+ECHO CYGWIN INSTALL DIR (WIN)    = %CYGWIN_INSTALLDIR_WFMT%
+ECHO CYGWIN INSTALL DIR (MINGW)  = %CYGWIN_INSTALLDIR_MFMT%
+ECHO CYGWIN INSTALL DIR (CYGWIN) = %CYGWIN_INSTALLDIR_CFMT%
+ECHO RESULT INSTALL DIR (WIN)    = %RESULT_INSTALLDIR_WFMT%
+ECHO RESULT INSTALL DIR (MINGW)  = %RESULT_INSTALLDIR_MFMT%
+ECHO RESULT INSTALL DIR (CYGWIN) = %RESULT_INSTALLDIR_CFMT%
+
+REM WARNING: Add a space after the = in case you want set this to empty, otherwise the variable will be unset
+SET MAKE_OPT=-j %MAKE_THREADS%
+
+REM ========== DERIVED CYGWIN SETUP OPTIONS ==========
+
+REM One can't set a variable to empty in DOS, but you can set it to a space this way.
+REM The quotes are just there to make the space visible and to protect from "remove trailing spaces".
+SET "CYGWIN_OPT= "
+
+IF "%CYGWIN_FROM_CACHE%" == "Y" (
+  SET CYGWIN_OPT= %CYGWIN_OPT% -L
+)
+
+IF "%CYGWIN_QUIET%" == "Y" (
+  SET CYGWIN_OPT= %CYGWIN_OPT% -q --no-admin
+)
+
+IF "%GTK_FROM_SOURCES%"=="N" (
+  SET CYGWIN_OPT= %CYGWIN_OPT% -P mingw64-%ARCH%-gtk2.0,mingw64-%ARCH%-gtksourceview2.0
+)
+
+REM Cygwin setup sets proper ACLs (permissions) for folders it CREATES.
+REM Otherwise chmod won't work and e.g. the ocaml build will fail.
+REM Cygwin setup does not touch the ACLs of existing folders.
+
+REM Run Cygwin Setup
+
+SET RUNSETUP=Y
+IF EXIST "%CYGWIN_INSTALLDIR_WFMT%\etc\setup\installed.db" (
+  SET RUNSETUP=N
+)
+IF NOT "%CYGWIN_QUIET%" == "Y" (
+  SET RUNSETUP=Y
+)
+
+IF "%COQREGTESTING%" == "Y" (
+  ECHO "========== REMOVE EXISTING CYGWIN =========="
+  DEL /S /F /Q "%CYGWIN_INSTALLDIR_WFMT%" > NUL
+  SET RUNSETUP=Y
+)
+
+SET "EXTRAPACKAGES= "
+
+IF NOT "%APPVEYOR%" == "True" (
+  SET EXTRAPACKAGES=-P wget,curl,git,gcc-core,gcc-g++,automake1.5
+)
+
+ECHO "========== INSTALL CYGWIN =========="
+
+IF "%RUNSETUP%"=="Y" (
+  %SETUP% ^
+    --proxy "%PROXY%" ^
+    --site "%CYGWIN_REPOSITORY%" ^
+    --root "%CYGWIN_INSTALLDIR_WFMT%" ^
+    --local-package-dir "%CYGWIN_LOCAL_CACHE_WFMT%" ^
+    --no-shortcuts ^
+    %CYGWIN_OPT% ^
+    -P make,unzip ^
+    -P gdb,liblzma5 ^
+    -P patch,automake1.14 ^
+    -P mingw64-%ARCH%-binutils,mingw64-%ARCH%-gcc-core,mingw64-%ARCH%-gcc-g++,mingw64-%ARCH%-pkg-config,mingw64-%ARCH%-windows_default_manifest ^
+    -P mingw64-%ARCH%-headers,mingw64-%ARCH%-runtime,mingw64-%ARCH%-pthreads,mingw64-%ARCH%-zlib ^
+    -P libiconv-devel,libunistring-devel,libncurses-devel ^
+    -P gettext-devel,libgettextpo-devel ^
+    -P libglib2.0-devel,libgdk_pixbuf2.0-devel ^
+    -P libfontconfig1 ^
+    -P gtk-update-icon-cache ^
+    -P libtool,automake ^
+    -P intltool ^
+    %EXTRAPACKAGES% ^
+    || GOTO ErrorExit
+
+  MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build"
+  MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\buildlogs"
+)
+
+IF NOT "%CYGWIN_QUIET%" == "Y" (
+  REM Like most setup programs, cygwin setup starts the real setup as a separate process, so wait for it.
+  REM This is not required with the -cygquiet=Y and the resulting --no-admin option.
+  :waitsetup
+  tasklist /fi "imagename eq %SETUP%" | find ":" > NUL
+  IF ERRORLEVEL 1 GOTO waitsetup
+)
+
+ECHO ========== CONFIGURE CYGWIN USER ACCOUNT ==========
+
+REM In case this batch file is called from a cygwin bash (e.g. a git repo) we need to clear
+REM HOME (otherwise we get to the home directory of the other installation)
+REM PROFILEREAD (this is set to true if the /etc/profile has been read, which creates user)
+SET "HOME="
+SET "PROFILEREAD="
+
+copy "%BATCHDIR%\configure_profile.sh" "%CYGWIN_INSTALLDIR_WFMT%\var\tmp" || GOTO ErrorExit
+%BASH% --login "%CYGWIN_INSTALLDIR_CFMT%\var\tmp\configure_profile.sh" "%PROXY%" || GOTO ErrorExit
+
+ECHO ========== BUILD COQ ==========
+
+MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build"
+MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\patches"
+
+COPY "%BATCHDIR%\makecoq_mingw.sh" "%CYGWIN_INSTALLDIR_WFMT%\build" || GOTO ErrorExit
+COPY "%BATCHDIR%\patches_coq\*.*" "%CYGWIN_INSTALLDIR_WFMT%\build\patches" || GOTO ErrorExit
+
+%BASH% --login "%CYGWIN_INSTALLDIR_CFMT%\build\makecoq_mingw.sh" || GOTO ErrorExit
+
+ECHO ========== FINISHED ==========
+
+GOTO :EOF
+
+ECHO ========== BATCH FUNCTIONS ==========
+
+:PrintPars
+  REM  01234567890123456789012345678901234567890123456789012345678901234567890123456789
+  ECHO -arch     ^<i686 or x86_64^> Set cygwin, ocaml and coq to 32 or 64 bit
+  ECHO -mode     ^<mingwincygwin = install coq in default cygwin mingw sysroot^>
+  ECHO           ^<absoloute = install coq in -destcoq absulute path^>
+  ECHO           ^<relocatable = install relocatable coq in -destcoq path^>
+  ECHO -installer^<Y or N^> create a windows installer (will be in /build/coq/dev/nsis)
+  ECHO -ocaml    ^<Y or N^> install OCaml in Coq folder (Y) or just in cygwin folder (N)
+  ECHO -make     ^<Y or N^> install GNU Make in Coq folder (Y) or not (N)
+  ECHO -destcyg  ^<path to cygwin destination folder^>
+  ECHO -destcoq  ^<path to coq destination folder (mode=absoloute/relocatable)^>
+  ECHO -setup    ^<cygwin setup program name^> (auto adjusted to -arch)
+  ECHO -proxy    ^<internet proxy^>
+  ECHO -cygrepo  ^<cygwin download repository^>
+  ECHO -cygcache ^<local cygwin repository/cache^>
+  ECHO -cyglocal ^<Y or N^> install cygwin from cache
+  ECHO -cygquiet ^<Y or N^> install cygwin without user interaction
+  ECHO -srccache ^<local source code repository/cache^>
+  ECHO -coqver   ^<Coq version to install^>
+  ECHO -gtksrc   ^<Y or N^> build GTK ^(90 min^) or use cygwin version
+  ECHO -threads  ^<1..N^> Number of make threads
+  ECHO -addon    ^<name^>  Enable building selected addon (can be repeated)
+  ECHO(
+  ECHO See ReadMe.txt for a detailed description of all parameters
+  ECHO(
+  ECHO Parameter values (default or currently set):
+  ECHO -arch     = %ARCH%
+  ECHO -mode     = %INSTALLMODE%
+  ECHO -ocaml    = %INSTALLOCAML%
+  ECHO -installer= %MAKEINSTALLER%
+  ECHO -make     = %INSTALLMAKE%
+  ECHO -destcyg  = %DESTCYG%
+  ECHO -destcoq  = %DESTCOQ%
+  ECHO -setup    = %SETUP%
+  ECHO -proxy    = %PROXY%
+  ECHO -cygrepo  = %CYGWIN_REPOSITORY%
+  ECHO -cygcache = %CYGWIN_LOCAL_CACHE_WFMT%
+  ECHO -cyglocal = %CYGWIN_FROM_CACHE%
+  ECHO -cygquiet = %CYGWIN_QUIET%
+  ECHO -srccache = %SOURCE_LOCAL_CACHE_WFMT%
+  ECHO -coqver   = %COQ_VERSION%
+  ECHO -gtksrc   = %GTK_FROM_SOURCES%
+  ECHO -threads  = %MAKE_THREADS%
+  ECHO -addon    = %COQ_ADDONS%
+  GOTO :EOF
+
+:CheckYN
+  REM Reset errorlevel to 0
+  CMD /c "EXIT /b 0"
+  IF "%2" == "Y" (
+    REM OK Y
+  ) ELSE IF "%2" == "N" (
+    REM OK N
+  ) ELSE (
+    ECHO ERROR Parameter %1 must be Y or N, but is %2
+    GOTO ErrorExit
+  )
+  GOTO :EOF
+
+:ErrorExit
+  ECHO ERROR MakeCoq_MinGW.bat failed
+  EXIT /b 1
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 23eb6fbc63..74dd4d41c1 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -159,19 +159,19 @@ if [ "${COQREGTESTING:-N}" == "Y" ] ; then
   # Log command output - take log target name from command name (like log1 make => log target is "<module>-make")
   log1() {
     { local -; set +x; } 2> /dev/null
-    "$@" >"$LOGS/$LOGTARGET-$1.log"  2>"$LOGS/$LOGTARGET-$1.err"
+    "$@" >"$LOGS/$LOGTARGET-$1_log.txt"  2>"$LOGS/$LOGTARGET-$1_err.txt"
   }
 
   # Log command output - take log target name from command name and first argument (like log2 make install => log target is "<module>-make-install")
   log2() {
     { local -; set +x; } 2> /dev/null
-    "$@" >"$LOGS/$LOGTARGET-$1-$2.log" 2>"$LOGS/$LOGTARGET-$1-$2.err"
+    "$@" >"$LOGS/$LOGTARGET-$1-$2_log.txt" 2>"$LOGS/$LOGTARGET-$1-$2_err.txt"
   }
 
   # Log command output - take log target name from command name and second argument (like log_1_3 ocaml setup.ml -configure => log target is "<module>-ocaml--configure")
   log_1_3() {
     { local -; set +x; } 2> /dev/null
-    "$@" >"$LOGS/$LOGTARGET-$1-$3.log" 2>"$LOGS/$LOGTARGET-$1-$3.err"
+    "$@" >"$LOGS/$LOGTARGET-$1-$3_log.txt" 2>"$LOGS/$LOGTARGET-$1-$3_err.txt"
   }
 
   # Log command output - log target name is first argument (like logn untar tar xvaf ... => log target is "<module>-untar")
@@ -179,26 +179,26 @@ if [ "${COQREGTESTING:-N}" == "Y" ] ; then
     { local -; set +x; } 2> /dev/null
     LOGTARGETEX=$1
     shift
-    "$@" >"$LOGS/$LOGTARGET-$LOGTARGETEX.log" 2>"$LOGS/$LOGTARGET-$LOGTARGETEX.err"
+    "$@" >"$LOGS/$LOGTARGET-${LOGTARGETEX}_log.txt" 2>"$LOGS/$LOGTARGET-${LOGTARGETEX}_err.txt"
   }
 else
   # If COQREGTESTING, log to log files and console
   # Log command output - take log target name from command name (like log1 make => log target is "<module>-make")
   log1() {
     { local -; set +x; } 2> /dev/null
-    "$@" > >(tee "$LOGS/$LOGTARGET-$1.log" | sed -e "s/^/$LOGTARGET-$1.log: /") 2> >(tee "$LOGS/$LOGTARGET-$1.err" | sed -e "s/^/$LOGTARGET-$1.err: /" 1>&2)
+    "$@" > >(tee "$LOGS/$LOGTARGET-$1_log.txt" | sed -e "s/^/$LOGTARGET-$1_log.txt: /") 2> >(tee "$LOGS/$LOGTARGET-$1_err.txt" | sed -e "s/^/$LOGTARGET-$1_err.txt: /" 1>&2)
   }
 
   # Log command output - take log target name from command name and first argument (like log2 make install => log target is "<module>-make-install")
   log2() {
     { local -; set +x; } 2> /dev/null
-    "$@" > >(tee "$LOGS/$LOGTARGET-$1-$2.log" | sed -e "s/^/$LOGTARGET-$1-$2.log: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$2.err" | sed -e "s/^/$LOGTARGET-$1-$2.err: /" 1>&2)
+    "$@" > >(tee "$LOGS/$LOGTARGET-$1-$2_log.txt" | sed -e "s/^/$LOGTARGET-$1-$2_log.txt: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$2_err.txt" | sed -e "s/^/$LOGTARGET-$1-$2_err.txt: /" 1>&2)
   }
 
   # Log command output - take log target name from command name and second argument (like log_1_3 ocaml setup.ml -configure => log target is "<module>-ocaml--configure")
   log_1_3() {
     { local -; set +x; } 2> /dev/null
-    "$@" > >(tee "$LOGS/$LOGTARGET-$1-$3.log" | sed -e "s/^/$LOGTARGET-$1-$3.log: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$3.err" | sed -e "s/^/$LOGTARGET-$1-$3.err: /" 1>&2)
+    "$@" > >(tee "$LOGS/$LOGTARGET-$1-$3_log.txt" | sed -e "s/^/$LOGTARGET-$1-$3_log.txt: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$3_err.txt" | sed -e "s/^/$LOGTARGET-$1-$3_err.txt: /" 1>&2)
   }
 
   # Log command output - log target name is first argument (like logn untar tar xvaf ... => log target is "<module>-untar")
@@ -206,7 +206,7 @@ else
     { local -; set +x; } 2> /dev/null
     LOGTARGETEX=$1
     shift
-    "$@" > >(tee "$LOGS/$LOGTARGET-$LOGTARGETEX.log" | sed -e "s/^/$LOGTARGET-$LOGTARGETEX.log: /") 2> >(tee "$LOGS/$LOGTARGET-$LOGTARGETEX.err" | sed -e "s/^/$LOGTARGET-$LOGTARGETEX.err: /" 1>&2)
+    "$@" > >(tee "$LOGS/$LOGTARGET-${LOGTARGETEX}_log.txt" | sed -e "s/^/$LOGTARGET-${LOGTARGETEX}_log.txt: /") 2> >(tee "$LOGS/$LOGTARGET-${LOGTARGETEX}_err.txt" | sed -e "s/^/$LOGTARGET-${LOGTARGETEX}_err.txt: /" 1>&2)
   }
 fi
 
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 63d5541f48..8620b01b26 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -226,3 +226,10 @@
 : "${quickchick_CI_REF:=master}"
 : "${quickchick_CI_GITURL:=https://github.com/QuickChick/QuickChick}"
 : "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}"
+
+########################################################################
+# quickchick
+########################################################################
+: "${plugin_tutorial_CI_REF:=master}"
+: "${plugin_tutorial_CI_GITURL:=https://github.com/ybertot/plugin_tutorials}"
+: "${plugin_tutorial_CI_ARCHIVEURL:=${plugin_tutorial_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 4acc0e86cf..7a450d0d48 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -16,13 +16,6 @@ then
     then
         export CI_PULL_REQUEST="${CI_BRANCH#pr-}"
     fi
-elif [ -n "${TRAVIS}" ];
-then
-    # Travis build, `-local` passed to `configure`
-    export OCAMLPATH="$PWD:$OCAMLPATH"
-    export COQBIN="$PWD/bin"
-    export CI_PULL_REQUEST="$TRAVIS_PULL_REQUEST"
-    export CI_BRANCH="$TRAVIS_BRANCH"
 elif [ -d "$PWD/_build/install/default/" ];
 then
     # Dune build
diff --git a/dev/ci/ci-plugin-tutorial.sh b/dev/ci/ci-plugin-tutorial.sh
new file mode 100755
index 0000000000..6c26a71a21
--- /dev/null
+++ b/dev/ci/ci-plugin-tutorial.sh
@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download plugin_tutorial
+
+( cd "${CI_BUILD_DIR}/plugin_tutorial" && \
+  pushd tuto0 && make && popd          && \
+  pushd tuto1 && make && popd          && \
+  pushd tuto2 && make && popd          && \
+  pushd tuto3 && make && popd          )
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 8d0f69626e..fcfa591ce1 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-09-24-V01"
+# CACHEKEY: "bionic_coq-V2018-09-25-V1"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -32,33 +32,31 @@ ENV NJOBS="2" \
     OPAMYES="true"
 
 # Base opam is the set of base packages required by Coq
-ENV COMPILER="4.02.3"
+ENV COMPILER="4.05.0"
 
 # Common OPAM packages.
 # `num` does not have a version number as the right version to install varies
 # with the compiler version.
-ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8" \
+ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8 odoc.1.2.0" \
     CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
-ENV CAMLP5_VER="6.14" \
+ENV CAMLP5_VER="7.01" \
     COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2"
 
-# The separate `opam install ocamlfind` workarounds an OPAM repository bug in 4.02.3
+# base switch
 RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \
-    opam install ocamlfind.1.8.0 && \
     opam install $BASE_OPAM camlp5.$CAMLP5_VER $COQIDE_OPAM $CI_OPAM
 
 # base+32bit switch
 RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
-    opam install ocamlfind.1.8.0 && \
     opam install $BASE_OPAM camlp5.$CAMLP5_VER
 
 # EDGE switch
 ENV COMPILER_EDGE="4.07.0" \
     CAMLP5_VER_EDGE="7.06" \
     COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \
-    BASE_OPAM_EDGE="odoc.1.2.0 dune-release.0.3.0"
+    BASE_OPAM_EDGE="dune-release.0.3.0"
 
 RUN opam switch create $COMPILER_EDGE && eval $(opam env) && \
     opam install $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index a848c49d75..09e9762261 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -1,120 +1,120 @@
-@ECHO OFF
-
-REM This script builds and signs the Windows packages on Gitlab
-
-ECHO "Start Time"
-TIME /T
-
-REM List currently used cygwin and target folders for debugging / maintenance purposes
-
-ECHO "Currently used cygwin folders"
-DIR C:\ci\cygwin*
-ECHO "Currently used target folders"
-DIR C:\ci\coq*
-ECHO "Root folders"
-DIR C:\
-
-if %ARCH% == 32 (
-  SET ARCHLONG=i686
-  SET SETUP=setup-x86.exe
-)
-
-if %ARCH% == 64 (
-  SET ARCHLONG=x86_64
-  SET SETUP=setup-x86_64.exe
-)
-
-SET CYGROOT=C:\ci\cygwin%ARCH%
-SET DESTCOQ=C:\ci\coq%ARCH%
-
-CALL :MakeUniqueFolder %CYGROOT% CYGROOT
-CALL :MakeUniqueFolder %DESTCOQ% DESTCOQ
-
-powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/%SETUP%', '%SETUP%')"
-SET CYGCACHE=%CYGROOT%\var\cache\setup
-SET CI_PROJECT_DIR_MFMT=%CI_PROJECT_DIR:\=/%
-SET CI_PROJECT_DIR_CFMT=%CI_PROJECT_DIR_MFMT:C:/=/cygdrive/c/%
-SET COQREGTESTING=Y
-SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\v7.1\Bin
-
-if exist %CYGROOT%\build\ rd /s /q %CYGROOT%\build
-if exist %DESTCOQ%\ rd /s /q %DESTCOQ%
-
-call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
-  -arch=%ARCH% -installer=Y -coqver=%CI_PROJECT_DIR_CFMT% ^
-  -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
-  -addon="bignums ltac2 equations" -make=N ^
-  -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorCopyLogFilesAndExit
-
-
-ECHO "Start Artifact Creation"
-TIME /T
-
-mkdir artifacts
-
-CALL :CopyLogFiles
-
-copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" artifacts || GOTO ErrorExit
-REM The open source archive is only required for release builds
-IF DEFINED WIN_CERTIFICATE_PATH (
-  7z a artifacts\coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit
-) ELSE (
-  REM In non release builds, create a dummy file
-  ECHO "This is not a release build - open source archive not created / uploaded" > artifacts\coq-opensource-info.txt
-)
-
-REM DO NOT echo the signing command below, as this would leak secrets in the logs
-IF DEFINED WIN_CERTIFICATE_PATH (
-  IF DEFINED WIN_CERTIFICATE_PASSWORD (
-    ECHO Signing package
-    @signtool sign /f %WIN_CERTIFICATE_PATH% /p %WIN_CERTIFICATE_PASSWORD% dev\nsis\*.exe
-    signtool verify /pa dev\nsis\*.exe
-  )
-)
-
-ECHO "Finished Artifact Creation"
-TIME /T
-
-CALL :CleanupFolders
-
-ECHO "Finished Cleanup"
-TIME /T
-
-GOTO :EOF
-
-:CopyLogFiles
-  ECHO Copy log files for artifact upload
-  MKDIR artifacts\buildlogs
-  COPY %CYGROOT%\build\buildlogs\* artifacts\buildlogs
-  MKDIR artifacts\filelists
-  COPY %CYGROOT%\build\filelists\* artifacts\filelists
-  MKDIR artifacts\flagfiles
-  COPY %CYGROOT%\build\flagfiles\* artifacts\flagfiles
-  GOTO :EOF
-
-:CleanupFolders
-  ECHO "Cleaning %CYGROOT%"
-  RMDIR /S /Q "%CYGROOT%"
-  ECHO "Cleaning %DESTCOQ%"
-  RMDIR /S /Q "%DESTCOQ%"
-  GOTO :EOF
-
-:MakeUniqueFolder
-  REM Create a uniquely named folder
-  REM This script is safe because folder creation is atomic - either we create it or fail
-  REM %1 = base path or directory (_%RANDOM%_%RANDOM% is appended to this)
-  REM %2 = name of the variable which receives the unique folder name
-  SET "UNIQUENAME=%1_%RANDOM%_%RANDOM%"
-  MKDIR "%UNIQUENAME%"
-  IF ERRORLEVEL 1 GOTO :MakeUniqueFolder
-  SET "%2=%UNIQUENAME%"
-  GOTO :EOF
-
-:ErrorCopyLogFilesAndExit
-  CALL :CopyLogFiles
-  REM fall through
-
-:ErrorExit
-  CALL :CleanupFolders
-  ECHO ERROR %0 failed
-  EXIT /b 1
+@ECHO OFF
+
+REM This script builds and signs the Windows packages on Gitlab
+
+ECHO "Start Time"
+TIME /T
+
+REM List currently used cygwin and target folders for debugging / maintenance purposes
+
+ECHO "Currently used cygwin folders"
+DIR C:\ci\cygwin*
+ECHO "Currently used target folders"
+DIR C:\ci\coq*
+ECHO "Root folders"
+DIR C:\
+
+if %ARCH% == 32 (
+  SET ARCHLONG=i686
+  SET SETUP=setup-x86.exe
+)
+
+if %ARCH% == 64 (
+  SET ARCHLONG=x86_64
+  SET SETUP=setup-x86_64.exe
+)
+
+SET CYGROOT=C:\ci\cygwin%ARCH%
+SET DESTCOQ=C:\ci\coq%ARCH%
+
+CALL :MakeUniqueFolder %CYGROOT% CYGROOT
+CALL :MakeUniqueFolder %DESTCOQ% DESTCOQ
+
+powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/%SETUP%', '%SETUP%')"
+SET CYGCACHE=%CYGROOT%\var\cache\setup
+SET CI_PROJECT_DIR_MFMT=%CI_PROJECT_DIR:\=/%
+SET CI_PROJECT_DIR_CFMT=%CI_PROJECT_DIR_MFMT:C:/=/cygdrive/c/%
+SET COQREGTESTING=Y
+SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\v7.1\Bin
+
+if exist %CYGROOT%\build\ rd /s /q %CYGROOT%\build
+if exist %DESTCOQ%\ rd /s /q %DESTCOQ%
+
+call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
+  -arch=%ARCH% -installer=Y -coqver=%CI_PROJECT_DIR_CFMT% ^
+  -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
+  -addon="bignums ltac2 equations" -make=N ^
+  -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorCopyLogFilesAndExit
+
+
+ECHO "Start Artifact Creation"
+TIME /T
+
+mkdir artifacts
+
+CALL :CopyLogFiles
+
+copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" artifacts || GOTO ErrorExit
+REM The open source archive is only required for release builds
+IF DEFINED WIN_CERTIFICATE_PATH (
+  7z a artifacts\coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit
+) ELSE (
+  REM In non release builds, create a dummy file
+  ECHO "This is not a release build - open source archive not created / uploaded" > artifacts\coq-opensource-info.txt
+)
+
+REM DO NOT echo the signing command below, as this would leak secrets in the logs
+IF DEFINED WIN_CERTIFICATE_PATH (
+  IF DEFINED WIN_CERTIFICATE_PASSWORD (
+    ECHO Signing package
+    @signtool sign /f %WIN_CERTIFICATE_PATH% /p %WIN_CERTIFICATE_PASSWORD% dev\nsis\*.exe
+    signtool verify /pa dev\nsis\*.exe
+  )
+)
+
+ECHO "Finished Artifact Creation"
+TIME /T
+
+CALL :CleanupFolders
+
+ECHO "Finished Cleanup"
+TIME /T
+
+GOTO :EOF
+
+:CopyLogFiles
+  ECHO Copy log files for artifact upload
+  MKDIR artifacts\buildlogs
+  COPY %CYGROOT%\build\buildlogs\* artifacts\buildlogs
+  MKDIR artifacts\filelists
+  COPY %CYGROOT%\build\filelists\* artifacts\filelists
+  MKDIR artifacts\flagfiles
+  COPY %CYGROOT%\build\flagfiles\* artifacts\flagfiles
+  GOTO :EOF
+
+:CleanupFolders
+  ECHO "Cleaning %CYGROOT%"
+  RMDIR /S /Q "%CYGROOT%"
+  ECHO "Cleaning %DESTCOQ%"
+  RMDIR /S /Q "%DESTCOQ%"
+  GOTO :EOF
+
+:MakeUniqueFolder
+  REM Create a uniquely named folder
+  REM This script is safe because folder creation is atomic - either we create it or fail
+  REM %1 = base path or directory (_%RANDOM%_%RANDOM% is appended to this)
+  REM %2 = name of the variable which receives the unique folder name
+  SET "UNIQUENAME=%1_%RANDOM%_%RANDOM%"
+  MKDIR "%UNIQUENAME%"
+  IF ERRORLEVEL 1 GOTO :MakeUniqueFolder
+  SET "%2=%UNIQUENAME%"
+  GOTO :EOF
+
+:ErrorCopyLogFilesAndExit
+  CALL :CopyLogFiles
+  REM fall through
+
+:ErrorExit
+  CALL :CleanupFolders
+  ECHO ERROR %0 failed
+  EXIT /b 1
diff --git a/dev/ci/user-overlays/08456-fix-6764.sh b/dev/ci/user-overlays/08456-fix-6764.sh
new file mode 100644
index 0000000000..3b951d9c07
--- /dev/null
+++ b/dev/ci/user-overlays/08456-fix-6764.sh
@@ -0,0 +1,5 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "8456" ] || [ "$CI_BRANCH" = "fix-6764" ]; then
+    Elpi_CI_REF=overlay/8456
+fi
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index 85aaf317ef..7349360be8 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -3,29 +3,45 @@ Dune-based build system. If you want to enhance the build system
 itself (or are curious about its implementation details), see
 build-system.dev.txt, and in particular its initial HISTORY section.
 
-Dune
-====
+About Dune
+==========
 
-Coq can now be built using
-[Dune](https://github.com/ocaml/dune). Contrary to other systems,
-Dune, doesn't use a global`makefile` but local build files named
-`dune` that are later composed to form a global build.
+Coq can now be built using [Dune](https://github.com/ocaml/dune).
+
+## Quick Start
+
+You need Dune >= 1.2.1 ; just type `dune build` to build the base Coq
+libraries. No call to `./configure` is needed.
+
+Dune will get confused if it finds leftovers of in-tree compilation,
+so please be sure your tree is clean from objects files generated by
+the make-based system.
+
+If you want to build the standard libraries and plugins you should
+call `make -f Makefile.dune voboot`. It is usually enough to do that
+once per-session.
+
+More helper targets are availabe in `Makefile.dune`, `make -f
+Makefile.dune` will display some help.
+
+Dune places build artifacts in a separate directory `_build`; it will
+also generate an `.install` file so files can be properly installed by
+package managers.
+
+Contrary to other systems, Dune doesn't use a global `Makefile` but
+local build files named `dune` that are later composed to form a
+global build.
 
 As a developer, Dune should take care of all OCaml-related build tasks
-including library management, merlin files, and link order. You are
+including library management, merlin files, and linking order. You are
 are not supposed to modify the `dune` files unless you are adding a
 new binary, library, or plugin.
 
-The current Dune setup also doesn't require a call to `configure`. The
-auto-generated configuration files are properly included in the
-dependency graph so it will be automatically generated by Dune with
-reasonable developer defaults. You can still override the defaults by
-manually calling `./configure`, but note that some configure options
-such as install paths are not used by Dune.
+## Per-User Custom Settings
 
-Dune uses a separate directory `_build` to store build artifacts; it
-will generate an `.install` file so artifacts in the build can be
-properly installed by package managers.
+Dune will read the file `~/.config/dune/config`; see `man
+dune-config`. Among others, you can set in this file the custom number
+of build threads `(jobs N)` and display options `(display _mode_)`.
 
 ## Targets
 
@@ -36,8 +52,10 @@ project, creating an "install" overlay in `_build/install/default`.
 You can build some other target by doing `dune build $TARGET`.
 
 In order to build a single package, you can do `dune build
-$PACKAGE.install`. Dune also provides targets for documentation and
-testing, see below.
+$PACKAGE.install`.
+
+Dune also provides targets for documentation, testing, and release
+builds, please see below.
 
 ## Developer shell
 
@@ -66,7 +84,8 @@ current Coq source tree contains two packages [Coq and CoqIDE], and in
 the OPAM CoqIDE package we don't want to build CoqIDE against the
 local copy of Coq. For this purpose, Dune supports the `-p` option, so
 `dune build -p coqide` will build CoqIDE against the system-installed
-version of Coq libs.
+version of Coq libs, and use a "release" profile that for example
+enables stronger compiler optimizations.
 
 ## Stanzas
 
diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt
index 45766293c7..29e87df6b8 100644
--- a/dev/doc/profiling.txt
+++ b/dev/doc/profiling.txt
@@ -7,7 +7,7 @@ want to profile time or memory consumption. AFAIK, this only works for Linux.
 
 In Coq source folder:
 
-opam switch 4.02.3+fp
+opam switch 4.05.0+trunk+fp
 ./configure -local -debug
 make
 perf record -g bin/coqtop -compile file.v
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index 1821a181f1..b33a1cbd73 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -6,6 +6,35 @@
   the present checklist.
 - [ ] Change the version name to the next major version and the magic numbers
   (see [#7008](https://github.com/coq/coq/pull/7008/files)).
+- [ ] Update the compatibility infrastructure, which consists of doing
+      the following steps.  Note that all but the final step can be
+      performed automatically by
+      [`dev/tools/update-compat.py`](/dev/tools/update-compat.py) so
+      long as you have already updated `coq_version` in
+      [`configure.ml`](/configure.ml).
+  + [ ] Add a file `theories/Compat/CoqXX.v` which contains just the header
+        from [`dev/header.ml`](/dev/header.ml)
+  + [ ] Add the line `Require Export Coq.Compat.CoqXX.` at the top of
+        `theories/Compat/CoqYY.v`, where Y.Y is the version prior to X.X.
+  + [ ] Delete the file `theories/Compat/CoqWW.v`, where W.W is three versions
+        prior to X.X.
+  + [ ] Update
+        [`doc/stdlib/index-list.html.template`](/doc/stdlib/index-list.html.template)
+        with the deleted/added files.
+  + [ ] Remove any notations in the standard library which have `compat "W.W"`.
+  + [ ] Update the type `compat_version` in [`lib/flags.ml`](/lib/flags.ml) by
+        bumping all the version numbers by one, and update the interpretations
+        of those flags in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml) and
+        [`vernac/g_vernac.mlg`](/vernac/g_vernac.mlg).
+  + [ ] Update the files
+        [`test-suite/success/CompatCurrentFlag.v`](/test-suite/success/CompatCurrentFlag.v),
+        [`test-suite/success/CompatPreviousFlag.v`](/test-suite/success/CompatPreviousFlag.v),
+        and
+        [`test-suite/success/CompatOldFlag.v`](/test-suite/success/CompatOldFlag.v)
+        by bumping all version numbers by 1.
+  + [ ] Decide what to do about all test-suite files which mention `-compat
+        W.W` or `Coq.Comapt.CoqWW` (which is no longer valid, since we only
+        keep compatibility against the two previous versions)
 - [ ] Put the corresponding alpha tag using `git tag -s`.
   The `VX.X+alpha` tag marks the first commit to be in `master` and not in the
   branch of the previous version.
@@ -57,7 +86,6 @@
 ## Before the beta release date ##
 
 - [ ] Ensure the Credits chapter has been updated.
-- [ ] Ensure an empty `CompatXX.v` file has been created.
 - [ ] Ensure that an appropriate version of the plugins we will distribute with
   Coq has been tagged.
 - [ ] Have some people test the recently auto-generated Windows and MacOS
diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all
new file mode 100644
index 0000000000..44857ed050
--- /dev/null
+++ b/dev/dune-workspace.all
@@ -0,0 +1,11 @@
+(lang dune 1.2)
+
+; Add custom flags here. Default developer profile is `dev`
+(env
+ (dev     (flags :standard -rectypes -w -9-27-50))
+ (release (flags :standard -rectypes)))
+
+(context (opam (switch 4.05.0)))
+(context (opam (switch 4.05.0+32bit)))
+(context (opam (switch 4.07.0)))
+(context (opam (switch 4.07.0+flambda)))
diff --git a/dev/tools/sudo-apt-get-update.sh b/dev/tools/sudo-apt-get-update.sh
deleted file mode 100755
index f8bf6bed41..0000000000
--- a/dev/tools/sudo-apt-get-update.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-#!/usr/bin/env bash
-
-(sudo apt-get update "$@" 2>&1 || echo 'E: update failed') | tee /tmp/apt.err
-! grep -q '^\(E:\|W: Failed to fetch\)' /tmp/apt.err || exit $?
diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py
new file mode 100755
index 0000000000..7c8b9f025c
--- /dev/null
+++ b/dev/tools/update-compat.py
@@ -0,0 +1,341 @@
+#!/usr/bin/env python
+from __future__ import with_statement
+import os, re, sys
+
+# Obtain the absolute path of the script being run.  By assuming that
+# the script lives in dev/tools/, and basing all calls on the path of
+# the script, rather than the current working directory, we can be
+# robust to users who choose to run the script from any location.
+SCRIPT_PATH = os.path.dirname(os.path.realpath(__file__))
+ROOT_PATH = os.path.realpath(os.path.join(SCRIPT_PATH, '..', '..'))
+CONFIGURE_PATH = os.path.join(ROOT_PATH, 'configure.ml')
+HEADER_PATH = os.path.join(ROOT_PATH, 'dev', 'header.ml')
+DEFAULT_NUMBER_OF_OLD_VERSIONS = 2
+EXTRA_HEADER = '\n(** Compatibility file for making Coq act similar to Coq v%s *)\n'
+FLAGS_MLI_PATH = os.path.join(ROOT_PATH, 'lib', 'flags.mli')
+FLAGS_ML_PATH = os.path.join(ROOT_PATH, 'lib', 'flags.ml')
+COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'toplevel', 'coqargs.ml')
+G_VERNAC_PATH = os.path.join(ROOT_PATH, 'vernac', 'g_vernac.mlg')
+DOC_INDEX_PATH = os.path.join(ROOT_PATH, 'doc', 'stdlib', 'index-list.html.template')
+BUG_4798_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', '4798.v')
+TEST_SUITE_PATHS = tuple(os.path.join(ROOT_PATH, 'test-suite', 'success', i)
+                         for i in ('CompatOldOldFlag.v', 'CompatOldFlag.v', 'CompatPreviousFlag.v', 'CompatCurrentFlag.v'))
+TEST_SUITE_DESCRIPTIONS = ('current-minus-three', 'current-minus-two', 'current-minus-one', 'current')
+# sanity check that we are where we think we are
+assert(os.path.normpath(os.path.realpath(SCRIPT_PATH)) == os.path.normpath(os.path.realpath(os.path.join(ROOT_PATH, 'dev', 'tools'))))
+assert(os.path.exists(CONFIGURE_PATH))
+
+def get_header():
+    with open(HEADER_PATH, 'r') as f: return f.read()
+
+HEADER = get_header()
+
+def get_version(cur_version=None):
+    if cur_version is not None: return cur_version
+    with open(CONFIGURE_PATH, 'r') as f:
+        for line in f.readlines():
+            found = re.findall(r'let coq_version = "([0-9]+\.[0-9]+)', line)
+            if len(found) > 0:
+                return found[0]
+    raise Exception("No line 'let coq_version = \"X.X' found in %s" % os.path.relpath(CONFIGURE_PATH, ROOT_PATH))
+
+def compat_name_to_version_name(compat_file_name):
+    assert(compat_file_name.startswith('Coq') and compat_file_name.endswith('.v'))
+    v = compat_file_name[len('Coq'):][:-len('.v')]
+    assert(len(v) == 2 or (len(v) >= 2 and v[0] in ('8', '9'))) # we'll have to change this scheme when we hit Coq 10.*
+    return '%s.%s' % (v[0], v[1:])
+
+def version_name_to_compat_name(v, ext='.v'):
+    return 'Coq%s%s%s' % tuple(v.split('.') + [ext])
+
+# returns (lines of compat files, lines of not compat files
+def get_doc_index_lines():
+    with open(DOC_INDEX_PATH, 'r') as f:
+        lines = f.readlines()
+    return (tuple(line for line in lines if 'theories/Compat/Coq' in line),
+            tuple(line for line in lines if 'theories/Compat/Coq' not in line))
+
+COMPAT_INDEX_LINES, DOC_INDEX_LINES = get_doc_index_lines()
+
+def version_to_int_pair(v):
+    return tuple(map(int, v.split('.')))
+
+def get_known_versions():
+    # We could either get the files from the doc index, or from the
+    # directory list.  We assume that the doc index is more
+    # representative.  If we wanted to use the directory list, we
+    # would do:
+    # compat_files = os.listdir(os.path.join(ROOT_PATH, 'theories', 'Compat'))
+    compat_files = re.findall(r'Coq[^\.]+\.v', '\n'.join(COMPAT_INDEX_LINES))
+    return tuple(sorted((compat_name_to_version_name(i) for i in compat_files if i.startswith('Coq') and i.endswith('.v')), key=version_to_int_pair))
+
+def get_new_versions(known_versions, **args):
+    if args['cur_version'] in known_versions:
+        assert(known_versions[-1] == args['cur_version'])
+        assert(len(known_versions) == args['number_of_compat_versions'])
+        return known_versions
+    assert(len(known_versions) >= args['number_of_old_versions'])
+    return tuple(list(known_versions[-args['number_of_old_versions']:]) + [args['cur_version']])
+
+def update_compat_files(old_versions, new_versions, assert_unchanged=False, **args):
+    for v in old_versions:
+        if v not in new_versions:
+            compat_file = os.path.join('theories', 'Compat', version_name_to_compat_name(v))
+            if not assert_unchanged:
+                print('Removing %s...' % compat_file)
+                compat_path = os.path.join(ROOT_PATH, compat_file)
+                os.rename(compat_path, compat_path + '.bak')
+            else:
+                raise Exception('%s exists!' % compat_file)
+    for v, next_v in zip(new_versions, list(new_versions[1:]) + [None]):
+        compat_file = os.path.join('theories', 'Compat', version_name_to_compat_name(v))
+        compat_path = os.path.join(ROOT_PATH, compat_file)
+        if not os.path.exists(compat_path):
+            print('Creating %s...' % compat_file)
+            contents = HEADER + (EXTRA_HEADER % v)
+            if next_v is not None:
+                contents += '\nRequire Export Coq.Compat.%s.\n' % version_name_to_compat_name(next_v, ext='')
+            if not assert_unchanged:
+                with open(compat_path, 'w') as f:
+                    f.write(contents)
+                print(r"Don't forget to 'git add %s'!" % compat_file)
+            else:
+                raise Exception('%s does not exist!' % compat_file)
+        else:
+            # print('Checking %s...' % compat_file)
+            with open(compat_path, 'r') as f:
+                contents = f.read()
+            header = HEADER + (EXTRA_HEADER % v)
+            if not contents.startswith(HEADER):
+                raise Exception("Invalid header in %s; does not match %s" % (compat_file, os.path.relpath(HEADER_PATH, ROOT_PATH)))
+            if not contents.startswith(header):
+                raise Exception("Invalid header in %s; missing line %s" % (compat_file, EXTRA_HEADER.strip('\n') % v))
+            if next_v is not None:
+                line = 'Require Export Coq.Compat.%s.' % version_name_to_compat_name(next_v, ext='')
+                if ('\n%s\n' % line) not in contents:
+                    if not contents.startswith(header + '\n'):
+                        contents = contents.replace(header, header + '\n')
+                    contents = contents.replace(header, '%s\n%s' % (header, line))
+                    if not assert_unchanged:
+                        print('Updating %s...' % compat_file)
+                        with open(compat_path, 'w') as f:
+                            f.write(contents)
+                    else:
+                        raise Exception('Compat file %s is missing line %s' % (compat_file, line))
+
+def update_compat_versions_type_line(new_versions, contents, relpath):
+    compat_version_string = ' | '.join(['V%s_%s' % tuple(v.split('.')) for v in new_versions[:-1]] + ['Current'])
+    new_compat_line = 'type compat_version = %s' % compat_version_string
+    new_contents = re.sub(r'^type compat_version = .*$', new_compat_line, contents, flags=re.MULTILINE)
+    if new_compat_line not in new_contents:
+        raise Exception("Could not find 'type compat_version =' in %s" % relpath)
+    return new_contents
+
+def update_version_compare(new_versions, contents, relpath):
+    first_line = 'let version_compare v1 v2 = match v1, v2 with'
+    new_lines = [first_line]
+    for v in new_versions[:-1]:
+        V = 'V%s_%s' % tuple(v.split('.'))
+        new_lines.append('  | %s, %s -> 0' % (V, V))
+        new_lines.append('  | %s, _ -> -1' % V)
+        new_lines.append('  | _, %s -> 1' % V)
+    new_lines.append('  | Current, Current -> 0')
+    new_lines = '\n'.join(new_lines)
+    new_contents = re.sub(first_line + '.*' + 'Current, Current -> 0', new_lines, contents, flags=re.DOTALL|re.MULTILINE)
+    if new_lines not in new_contents:
+        raise Exception('Could not find version_compare in %s' % relpath)
+    return new_contents
+
+def update_pr_version(new_versions, contents, relpath):
+    first_line = 'let pr_version = function'
+    new_lines = [first_line]
+    for v in new_versions[:-1]:
+        V = 'V%s_%s' % tuple(v.split('.'))
+        new_lines.append('  | %s -> "%s"' % (V, v))
+    new_lines.append('  | Current -> "current"')
+    new_lines = '\n'.join(new_lines)
+    new_contents = re.sub(first_line + '.*' + 'Current -> "current"', new_lines, contents, flags=re.DOTALL|re.MULTILINE)
+    if new_lines not in new_contents:
+        raise Exception('Could not find pr_version in %s' % relpath)
+    return new_contents
+
+def update_add_compat_require(new_versions, contents, relpath):
+    first_line = 'let add_compat_require opts v ='
+    new_lines = [first_line, '  match v with']
+    for v in new_versions[:-1]:
+        V = 'V%s_%s' % tuple(v.split('.'))
+        new_lines.append('  | Flags.%s -> add_vo_require opts "Coq.Compat.%s" None (Some false)' % (V, version_name_to_compat_name(v, ext='')))
+    new_lines.append('  | Flags.Current -> add_vo_require opts "Coq.Compat.%s" None (Some false)' % version_name_to_compat_name(new_versions[-1], ext=''))
+    new_lines = '\n'.join(new_lines)
+    new_contents = re.sub(first_line + '.*' + 'Flags.Current -> add_vo_require opts "Coq.Compat.[^"]+" None .Some false.', new_lines, contents, flags=re.DOTALL|re.MULTILINE)
+    if new_lines not in new_contents:
+        raise Exception('Could not find add_compat_require in %s' % relpath)
+    return new_contents
+
+def update_parse_compat_version(new_versions, contents, relpath, **args):
+    line_count = args['number_of_compat_versions']+2 # 1 for the first line, 1 for the invalid flags
+    first_line = 'let parse_compat_version = let open Flags in function'
+    old_function_lines = contents[contents.index(first_line):].split('\n')[:line_count]
+    if re.match(r'^  \| \([0-9 "\.\|]*\) as s ->$', old_function_lines[-1]) is None:
+        raise Exception('Could not recognize line %d of parse_compat_version in %s as a list of invalid versions' % (line_count, relpath))
+    all_versions = re.findall(r'"([0-9\.]+)"', ''.join(old_function_lines))
+    invalid_versions = tuple(i for i in all_versions if i not in new_versions)
+    new_function_lines = [first_line]
+    for v, V in reversed(list(zip(new_versions, ['V%s_%s' % tuple(v.split('.')) for v in new_versions[:-1]] + ['Current']))):
+        new_function_lines.append('  | "%s" -> %s' % (v, V))
+    new_function_lines.append('  | (%s) as s ->' % ' | '.join('"%s"' % v for v in invalid_versions))
+    new_lines = '\n'.join(new_function_lines)
+    new_contents = contents.replace('\n'.join(old_function_lines), new_lines)
+    if new_lines not in new_contents:
+        raise Exception('Could not find parse_compat_version in %s' % relpath)
+    return new_contents
+
+def check_no_old_versions(old_versions, new_versions, contents, relpath):
+    for v in old_versions:
+        if v not in new_versions:
+            V = 'V%s_%s' % tuple(v.split('.'))
+            if V in contents:
+                raise Exception('Unreplaced usage of %s remaining in %s' % (V, relpath))
+
+def update_if_changed(contents, new_contents, path, assert_unchanged=False, **args):
+    if contents != new_contents:
+        if not assert_unchanged:
+            print('Updating %s...' % os.path.relpath(path, ROOT_PATH))
+            with open(path, 'w') as f:
+                f.write(new_contents)
+        else:
+            raise Exception('%s changed!' % os.path.relpath(path, ROOT_PATH))
+
+def update_flags_mli(old_versions, new_versions, **args):
+    with open(FLAGS_MLI_PATH, 'r') as f: contents = f.read()
+    new_contents = update_compat_versions_type_line(new_versions, contents, os.path.relpath(FLAGS_MLI_PATH, ROOT_PATH))
+    check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(FLAGS_MLI_PATH, ROOT_PATH))
+    update_if_changed(contents, new_contents, FLAGS_MLI_PATH, **args)
+
+def update_flags_ml(old_versions, new_versions, **args):
+    with open(FLAGS_ML_PATH, 'r') as f: contents = f.read()
+    new_contents = update_compat_versions_type_line(new_versions, contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH))
+    new_contents = update_version_compare(new_versions, new_contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH))
+    new_contents = update_pr_version(new_versions, new_contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH))
+    check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH))
+    update_if_changed(contents, new_contents, FLAGS_ML_PATH, **args)
+
+def update_coqargs_ml(old_versions, new_versions, **args):
+    with open(COQARGS_ML_PATH, 'r') as f: contents = f.read()
+    new_contents = update_add_compat_require(new_versions, contents, os.path.relpath(COQARGS_ML_PATH, ROOT_PATH))
+    check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(COQARGS_ML_PATH, ROOT_PATH))
+    update_if_changed(contents, new_contents, COQARGS_ML_PATH, **args)
+
+def update_g_vernac(old_versions, new_versions, **args):
+    with open(G_VERNAC_PATH, 'r') as f: contents = f.read()
+    new_contents = update_parse_compat_version(new_versions, contents, os.path.relpath(G_VERNAC_PATH, ROOT_PATH), **args)
+    check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(G_VERNAC_PATH, ROOT_PATH))
+    update_if_changed(contents, new_contents, G_VERNAC_PATH, **args)
+
+def update_flags(old_versions, new_versions, **args):
+    update_flags_mli(old_versions, new_versions, **args)
+    update_flags_ml(old_versions, new_versions, **args)
+    update_coqargs_ml(old_versions, new_versions, **args)
+    update_g_vernac(old_versions, new_versions, **args)
+
+def update_test_suite(new_versions, assert_unchanged=False, test_suite_paths=TEST_SUITE_PATHS, test_suite_descriptions=TEST_SUITE_DESCRIPTIONS, **args):
+    assert(len(new_versions) == len(test_suite_paths))
+    assert(len(new_versions) == len(test_suite_descriptions))
+    for i, (v, path, descr) in enumerate(zip(new_versions, test_suite_paths, test_suite_descriptions)):
+        if not os.path.exists(path):
+            raise Exception('Could not find existing file %s' % os.path.relpath(path, ROOT_PATH))
+        if '%s' in descr: descr = descr % v
+        with open(path, 'r') as f: contents = f.read()
+        lines = ['(* -*- coq-prog-args: ("-compat" "%s") -*- *)' % v,
+                 '(** Check that the %s compatibility flag actually requires the relevant modules. *)' % descr]
+        for imp_v in reversed(new_versions[i:]):
+            lines.append('Import Coq.Compat.%s.' % version_name_to_compat_name(imp_v, ext=''))
+        lines.append('')
+        new_contents = '\n'.join(lines)
+        update_if_changed(contents, new_contents, path, **args)
+
+def update_doc_index(new_versions, **args):
+    with open(DOC_INDEX_PATH, 'r') as f: contents = f.read()
+    firstline = '    theories/Compat/AdmitAxiom.v'
+    new_contents = ''.join(DOC_INDEX_LINES)
+    if firstline not in new_contents:
+        raise Exception("Could not find line '%s' in %s" % (firstline, os.path.relpath(DOC_INDEX_PATH, ROOT_PATH)))
+    extra_lines = ['    theories/Compat/%s' % version_name_to_compat_name(v) for v in new_versions]
+    new_contents = new_contents.replace(firstline, '\n'.join([firstline] + extra_lines))
+    update_if_changed(contents, new_contents, DOC_INDEX_PATH, **args)
+
+def update_bug_4789(new_versions, **args):
+    # we always update this compat notation to oldest
+    # currently-supported compat version, which should never be the
+    # current version
+    with open(BUG_4798_PATH, 'r') as f: contents = f.read()
+    new_contents = r"""Check match 2 with 0 => 0 | S n => n end.
+Notation "|" := 1 (compat "%s").
+Check match 2 with 0 => 0 | S n => n end. (* fails *)
+""" % new_versions[0]
+    update_if_changed(contents, new_contents, BUG_4798_PATH, **args)
+
+def update_compat_notations_in(old_versions, new_versions, contents):
+    for v in old_versions:
+        if v not in new_versions:
+            reg = re.compile(r'^[ \t]*(?:Notation|Infix)[^\n]*?compat "%s"[^\n]*?\n' % v, flags=re.MULTILINE)
+            contents = re.sub(r'^[ \t]*(?:Notation|Infix)[^\n]*?compat "%s"[^\n]*?\n' % v, '', contents, flags=re.MULTILINE)
+    return contents
+
+def update_compat_notations(old_versions, new_versions, **args):
+    for root, dirs, files in os.walk(os.path.join(ROOT_PATH, 'theories')):
+        for fname in files:
+            if not fname.endswith('.v'): continue
+            with open(os.path.join(root, fname), 'r') as f: contents = f.read()
+            new_contents = update_compat_notations_in(old_versions, new_versions, contents)
+            update_if_changed(contents, new_contents, os.path.join(root, fname), **args)
+
+def display_git_grep(old_versions, new_versions):
+    Vs = ['V%s_%s' % tuple(v.split('.')) for v in old_versions if v not in new_versions]
+    compat_vs = ['compat "%s"' % v for v in old_versions if v not in new_versions]
+    all_options = tuple(Vs + compat_vs)
+    options = (['"-compat" "%s"' % v for v in old_versions if v not in new_versions] +
+               [version_name_to_compat_name(v, ext='') for v in old_versions if v not in new_versions])
+    if len(options) > 0 or len(all_options) > 0:
+        print('To discover what files require manual updating, run:')
+        if len(options) > 0: print("git grep -- '%s' test-suite/" % r'\|'.join(options))
+        if len(all_options) > 0: print("git grep -- '%s'" % r'\|'.join(all_options))
+
+def parse_args(argv):
+    args = {
+        'assert_unchanged': False,
+        'cur_version': None,
+        'number_of_old_versions': DEFAULT_NUMBER_OF_OLD_VERSIONS
+    }
+    for arg in argv[1:]:
+        if arg == '--assert-unchanged':
+            args['assert_unchanged'] = True
+        elif arg.startswith('--cur-version='):
+            args['cur_version'] = arg[len('--cur-version='):]
+            assert(len(args['cur_version'].split('.')) == 2)
+            assert(all(map(str.isdigit, args['cur_version'].split('.'))))
+        elif arg.startswith('--number-of-old-versions='):
+            args['number_of_old_versions'] = int(arg[len('--number-of-old-versions='):])
+        else:
+            print('USAGE: %s [--assert-unchanged] [--cur-version=NN.NN] [--number-of-old-versions=NN]' % argv[0])
+            print('')
+            print('ERROR: Unrecognized argument: %s' % arg)
+            sys.exit(1)
+    return args
+
+if __name__ == '__main__':
+    args = parse_args(sys.argv)
+    args['cur_version'] = get_version(args['cur_version'])
+    args['number_of_compat_versions'] = args['number_of_old_versions'] + 1
+    known_versions = get_known_versions()
+    new_versions = get_new_versions(known_versions, **args)
+    assert(len(TEST_SUITE_PATHS) >= args['number_of_compat_versions'])
+    args['test_suite_paths'] = tuple(TEST_SUITE_PATHS[-args['number_of_compat_versions']:])
+    args['test_suite_descriptions'] = tuple(TEST_SUITE_DESCRIPTIONS[-args['number_of_compat_versions']:])
+    update_compat_files(known_versions, new_versions, **args)
+    update_flags(known_versions, new_versions, **args)
+    update_test_suite(new_versions, **args)
+    update_doc_index(new_versions, **args)
+    update_bug_4789(new_versions, **args)
+    update_compat_notations(known_versions, new_versions, **args)
+    display_git_grep(known_versions, new_versions)