[win] remove old scripts, we now use the platform ones

26 files changed, 0 insertions, 6814 deletions

diff --git a/dev/build/windows/CAVEATS.txt b/dev/build/windows/CAVEATS.txt
deleted file mode 100644
index cb1ae3aaaf..0000000000
--- a/dev/build/windows/CAVEATS.txt
+++ /dev/null
@@ -1,22 +0,0 @@
-===== Environemt SIZE =====

-

-find and xargs can fail if the environment is to large. I think the limit is 8k.

-

-xargs --show-limits

-

-shows the actual environment size

-

-The configure_profile.sh script sets ORIGINAL_PATH (set by cygwin) to "" to

-avoid issues

-

-===== OCAMLLIB =====

-

-If the environment variable OCAMLLIB is defined, it takes precedence over the

-internal paths of ocaml tools. This usually messes up things considerably. A

-typical failure is

-

-Error: Error on dynamically loaded library: .\dlllablgtk2.dll: %1 is not a valid Win32 application.

-

-The configure_profile.sh script clears OCAMLLIB, but if you use the ocaml

-compiler from outside the provided cygwin shell, OCAMLLIB might be defined.

-

diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
deleted file mode 100755
index 8eff2cf577..0000000000
--- a/dev/build/windows/MakeCoq_MinGW.bat
+++ /dev/null
@@ -1,499 +0,0 @@
-@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=https://mirrors.kernel.org/sourceware/cygwin

-

-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 paths to various formats

-REM WFMT = windows format (C:\..)          Used in this batch file.

-REM CFMT = cygwin format (\cygdrive\c\..)  Used for Cygwin PATH variable, 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%-gtk3,mingw64-%ARCH%-libxml2

-  REM gtksourceview3 is always built from sources until the bug in DLLMain is fixed in cygwin

-  REM SET CYGWIN_OPT= %CYGWIN_OPT% -P mingw64-%ARCH%-gtksourceview3.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 =========="

-

-REM If you need to add packages, see https://cygwin.com/packages/package_list.html for package names

-REM In the description of each package you also find the file list and maintainer there

-

-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 pkg-config ^

-    -P mingw64-%ARCH%-binutils,mingw64-%ARCH%-gcc-core,mingw64-%ARCH%-gcc-g++,mingw64-%ARCH%-windows_default_manifest ^

-    -P mingw64-%ARCH%-headers,mingw64-%ARCH%-runtime,mingw64-%ARCH%-pthreads,mingw64-%ARCH%-zlib ^

-    -P mingw64-%ARCH%-gmp,mingw64-%ARCH%-mpfr ^

-    -P adwaita-icon-theme ^

-    -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 libgmp-devel ^

-    -P intltool ^

-    -P bison,flex ^

-    %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"

-RMDIR /S /Q "%CYGWIN_INSTALLDIR_WFMT%\build\patches"

-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           ^<absolute = install coq in -destcoq absolute 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=absolute/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_SetRootPath.bat b/dev/build/windows/MakeCoq_SetRootPath.bat
deleted file mode 100644
index bcb104772c..0000000000
--- a/dev/build/windows/MakeCoq_SetRootPath.bat
+++ /dev/null
@@ -1,27 +0,0 @@
-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 ========== CHOOSE A SENSIBLE ROOT PATH ==========
-
-@ ECHO OFF
-
-REM Figure out a root path for coq and cygwin
-
-REM For the \nul trick for testing folders see
-REM https://support.microsoft.com/en-us/kb/65994
-
-IF EXIST D:\bin\nul (
-  SET ROOTPATH=D:\bin
-) else if EXIST C:\bin (
-  SET ROOTPATH=C:\bin
-) else (
-  SET ROOTPATH=C:
-)
-
-ECHO ROOTPATH set to %ROOTPATH%
diff --git a/dev/build/windows/MakeCoq_explicitcachefolders_installer.bat b/dev/build/windows/MakeCoq_explicitcachefolders_installer.bat
deleted file mode 100755
index d7d3c5b9d3..0000000000
--- a/dev/build/windows/MakeCoq_explicitcachefolders_installer.bat
+++ /dev/null
@@ -1,28 +0,0 @@
-@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 ========== BUILD COQ ==========

-

-call MakeCoq_SetRootPath

-

-call MakeCoq_MinGW.bat ^

-  -arch=64 ^

-  -installer=Y ^

-  -coqver=git-v8.6 ^

-  -destcyg="%ROOTPATH%\cygwin_coq64_cachefolder_inst" ^

-  -destcoq="%ROOTPATH%\coq64_cachefolder_inst" ^

-  -cygcache="%ROOTPATH%\cache\cygwin" ^

-  -srccache="%ROOTPATH%\cache\source"

-

-IF %ERRORLEVEL% NEQ 0 (

-  ECHO MakeCoq_explicitcachefolders_installer.bat failed with error code %ERRORLEVEL%

-  EXIT /b %ERRORLEVEL%

-)

diff --git a/dev/build/windows/MakeCoq_local_installer.bat b/dev/build/windows/MakeCoq_local_installer.bat
deleted file mode 100755
index 752b73c10a..0000000000
--- a/dev/build/windows/MakeCoq_local_installer.bat
+++ /dev/null
@@ -1,26 +0,0 @@
-@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 ========== BUILD COQ ==========

-

-call MakeCoq_SetRootPath

-

-call MakeCoq_MinGW.bat ^

-  -arch=64 ^

-  -installer=Y ^

-  -coqver=/cygdrive/d/coqgit/coq-8.6 ^

-  -destcyg="%ROOTPATH%\cygwin_coq64_local_inst" ^

-  -destcoq="%ROOTPATH%\coq64_local_inst"

-

-IF %ERRORLEVEL% NEQ 0 (

-  ECHO MakeCoq_local_installer.bat failed with error code %ERRORLEVEL%

-  EXIT /b %ERRORLEVEL%

-)

diff --git a/dev/build/windows/MakeCoq_master_installer.bat b/dev/build/windows/MakeCoq_master_installer.bat
deleted file mode 100755
index 72640d5d79..0000000000
--- a/dev/build/windows/MakeCoq_master_installer.bat
+++ /dev/null
@@ -1,26 +0,0 @@
-@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 ========== BUILD COQ ==========

-

-call MakeCoq_SetRootPath

-

-call MakeCoq_MinGW.bat ^

-  -arch=64 ^

-  -installer=Y ^

-  -coqver=git-master ^

-  -destcyg="%ROOTPATH%\cygwin_coq64_trunk_inst" ^

-  -destcoq="%ROOTPATH%\coq64_trunk_inst"

-

-IF %ERRORLEVEL% NEQ 0 (

-  ECHO MakeCoq_86git_installer.bat failed with error code %ERRORLEVEL%

-  EXIT /b %ERRORLEVEL%

-)

diff --git a/dev/build/windows/MakeCoq_regtest_noproxy.bat b/dev/build/windows/MakeCoq_regtest_noproxy.bat
deleted file mode 100644
index 7140a7c619..0000000000
--- a/dev/build/windows/MakeCoq_regtest_noproxy.bat
+++ /dev/null
@@ -1,29 +0,0 @@
-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 ========== BUILD COQ ==========

-

-call MakeCoq_SetRootPath

-

-SET HTTP_PROXY=

-SET HTTPS_PROXY=

-MKDIR C:\Temp\srccache

-

-call MakeCoq_MinGW.bat ^

-  -arch=64 ^

-  -mode=absolute ^

-  -ocaml=Y ^

-  -make=Y ^

-  -coqver 8.5pl2 ^

-  -srccache C:\Temp\srccache ^

-  -cygquiet=Y ^

-  -destcyg   %ROOTPATH%\cygwin_coq64_85pl2_abs ^

-  -destcoq   %ROOTPATH%\coq64_85pl2_abs

-

-pause

diff --git a/dev/build/windows/MakeCoq_regtests.bat b/dev/build/windows/MakeCoq_regtests.bat
deleted file mode 100644
index 74c26456b4..0000000000
--- a/dev/build/windows/MakeCoq_regtests.bat
+++ /dev/null
@@ -1,36 +0,0 @@
-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 ========== RUN REGRESSION TESTS FOR COQ BUILD SCRIPTS ==========
-
-SET COQREGTESTING=Y
-
-REM Current stable
-call MakeCoq_86git_abs_ocaml.bat || GOTO Error
-call MakeCoq_86git_installer.bat || GOTO Error
-call MakeCoq_86git_installer_32.bat || GOTO Error
-
-REM Old but might still be used
-call MakeCoq_85pl3_abs_ocaml.bat || GOTO Error
-call MakeCoq_84pl6_abs_ocaml.bat || GOTO Error
-
-REM Special variants, e.g. for debugging
-call MakeCoq_86git_abs_ocaml_gtksrc.bat || GOTO Error
-call MakeCoq_local_installer.bat || GOTO Error
-call MakeCoq_explicitcachefolders_installer.bat || GOTO Error
-
-REM Bleeding edge
-call MakeCoq_trunk_installer.bat || GOTO Error
-
-ECHO MakeCoq_regtests.bat: All tests finished successfully
-GOTO :EOF
-
-:Error
-ECHO MakeCoq_regtests.bat failed with error code %ERRORLEVEL%
-EXIT /b %ERRORLEVEL%
diff --git a/dev/build/windows/ReadMe.txt b/dev/build/windows/ReadMe.txt
deleted file mode 100644
index f34bbea4e9..0000000000
--- a/dev/build/windows/ReadMe.txt
+++ /dev/null
@@ -1,442 +0,0 @@
-(C) 2016 Intel Deutschland GmbH
-Author: Michael Soegtrop
-
-Released to the public by Intel under the
-GNU Lesser General Public License Version 2.1 or later
-See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-This license also applies to all files in the patches_coq subfolder.
-
-==================== Purpose / Goal ====================
-
-The main purpose of these scripts is to build Coq for Windows in a reproducible
-and at least by this script documented way without using binary libraries and
-executables from various sources. These scripts use only MinGW libraries
-provided by Cygwin or compile things from sources. For some libraries there are
-options to build them from sources or to use the Cygwin version.
-
-Another goal (which is not yet achieved) is to have a Coq installer for
-Windows, which includes all tools required for native compute and Coq plugin
-development without Cygwin.
-
-Coq requires OCaml for this and OCaml requires binutils, gcc and a posix shell.
-Since the standard Windows OCaml installation requires Cygwin to deliver some of
-these components, you might be able to imagine that this is not so easy.
-
-These scripts can produce the following:
-
-- Coq running on MinGW
-
-- OCaml producing MinGW code and running on MinGW
-
-- GCC producing MinGW code and running on MinGW
-
-- binutils producing MinGW code and running on MinGW
-
-With "running on MinGW" I mean that the tools accept paths like
-"C:\myfolder\myfile.txt" and that they don't link to a Cygwin or msys DLL. The
-MinGW gcc and binutils provided by Cygwin produce MinGW code, but they run only
-on Cygwin.
-
-With "producing MinGW code" I mean that the programs created by the tools accept
-paths like "C:\myfolder\myfile.txt" and that they don't link to a Cygwin or msys
-DLL.
-
-The missing piece is a posix shell running on plain Windows (without msys or
-Cygwin DLL) and not being a binary from obscure sources. I am working on it ...
-
-Since compiling gcc and binutils takes a while and it is not of much use without
-a shell, the building of these components is currently disabled. OCaml is built
-anyway, because this MinGW/MinGW OCaml (rather than a Cygwin/MinGW OCaml) is
-used to compile Coq.
-
-Until the shell is there, the Cygwin created by these scripts is required to run
-OCaml tools. When everything is finished, this will no longer be required.
-
-==================== Usage ====================
-
-The Script MakeCoq_MinGW does:
-- download Cygwin (except the Setup.exe or Setup64.exe)
-- install Cygwin
-- either installs MinGW GTK via Cygwin or compiles it fom sources
-- download, compile and install OCaml, CamlP5, Menhir, lablgtk
-- download, compile and install Coq
-- download, compile and install selected addons
-- create a Windows installer (NSIS based)
-
-The parameters are described below. Mostly paths and the HTTP proxy need to be
-set.
-
-There are two main usages:
-
-- Compile and install OCaml and Coq in a given folder
-
-  This works reliably, because absolute library paths can be compiled into Coq
-  and OCaml.
-  
-  WARNING: See the "Purpose / Goal" section above for status.
-  
-  See MakeCoq_85pl2_abs_ocaml.bat for parameters.
-
-- Create a Windows installer.
-
-  This works well for Coq but not so well for OCaml.
-
-  WARNING: See the "Purpose / Goal" section above for status.
-  
-  See MakeCoq_85pl2_installer.bat for parameters.
-
-There is also an option to compile OCaml and Coq inside Cygwin, but this is
-currently not recommended. The resulting Coq and OCaml work, but Coq is slow
-because it scans the largish Cygwin share folder. This will be fixed in a future
-version.
-
-Procedure:
-
-- Unzip contents of CoqSetup.zip in a folder
-
-- Adjust parameters in MakeCoq_85pl2_abs_ocaml.bat or in MakeCoq_85pl2_installer.bat.
-
-- Download Cygwin setup from https://Cygwin.com/install.html
-  For 32 bit Coq : setup-x86.exe    (https://Cygwin.com/setup-x86.exe)
-  For 64 bit Coq : setup-x86_64.exe (https://Cygwin.com/setup-x86_64.exe)
-
-- Run MakeCoq_85pl3_abs_ocaml.bat or MakeCoq_85pl3_installer.bat
-
-- Check MakeCoq_regtests.bat to see what combinations of options are tested
-
-==================== MakeCoq_MinGW Parameters ====================
-
-===== -arch =====
-
-Set the target architecture.
-
-Possible values:
-
-32: Install/build Cygwin, ocaml and coq for 32 bit windows
-
-64: Install/build Cygwin, ocaml and coq for 64 bit windows
-
-Default value: 64
-
-
-===== -mode =====
-
-Set the installation mode / target folder structure.
-  
-Possible values:
-
-mingwinCygwin: Install coq in the default Cygwin mingw sysroot folder.
-               This is %DESTCYG%\usr\%ARCH%-w64-mingw32\sys-root\mingw.
-               Todo: The coq share folder should be configured to e.g. /share/coq.
-               As is, coqc scans the complete share folder, which slows it down 5x for short files.
-               
-absolute:     Install coq in the absolute path given with -destcoq.
-               The resulting Coq will not be relocatable.
-               That is the root folder must not be renamed/moved.
-
-relocatable:   Install coq in the absolute path given with -destcoq.
-               The resulting Coq will be relocatable.
-               That is the root folder may be renamed/moved.
-               If OCaml is installed, please note that OCaml cannot be build really relocatable.
-               If the root folder is moved, the environment variable OCAMLLIB must be set to the libocaml sub folder.
-               Also the file <root>\libocaml\ld.conf must be adjusted.
-
-Default value: absolute
-
-
-===== -installer =====
-
-Create a Windows installer (it will be in build/coq-8.xplx/dev/nsis)
-
-Possible values:
-
-Y: Create a windows installer - this forces -mode=relocatable.
-
-N: Don't create a windows installer - use the created Coq installation as is.
-
-Default value: N
-
-
-===== -ocaml =====
-
-Install OCaml for later use with Coq or just for building.
-
-Possible values:
-
-Y: Install OCaml in the same root as Coq (as given with -coqdest)
-   This also copies all .o, .cmo, .a, .cmxa files in the lib folder required for compiling plugins.
-
-N: Install OCaml in the default Cygwin mingw sysroot folder.
-   This is %DESTCYG%\usr\%ARCH%-w64-mingw32\sys-root\mingw.
-
-Default value: N
-
-
-===== -make =====
-
-Build and install MinGW GNU make
-
-Possible values:
-
-Y: Install MinGW GNU make in the same root as Coq (as given with -coqdest).
-
-N: Don't build or install MinGW GNU make.
-   For building everything always Cygwin GNU make is used.
-
-Default value: Y
-
-
-===== -destcyg =====
-
-Destination folder in which Cygwin is installed.
-
-This must be an absolute path in Windows format (with drive letter and \\).
-
->>>>> This folder may be deleted after the Coq build is finished! <<<<<
-
-Default value: C:\bin\Cygwin_coq
-
-
-===== -destcoq =====
-
-Destination folder in which Coq is installed.
-
-This must be an absolute path in Windows format (with drive letter and \\).
-
-This option is not required if -mode mingwinCygwin is used.
-
-Default value: C:\bin\coq
-
-
-===== -setup =====
-
-Name/path of the Cygwin setup program.
-
-The Cygwin setup program is called setup-x86.exe or setup-x86_64.exe.
-It can be downloaded from: https://Cygwin.com/install.html.
-
-Default value: setup-x86.exe or setup-x86_64.exe, depending on -arch.
-
-
-===== -proxy =====
-
-Internet proxy setting for downloading Cygwin, ocaml and coq.
-
-The format is <server>:<port>, e.g. proxy.mycompany.com:911
-
-The same proxy is used for HTTP, HTTPS and FTP.
-If you need separate proxies for separate protocols, you please put your proxies directly into configure_profile.sh (line 11..13).
-
-Default value: Value of HTTP_PROXY environment variable or none if this variable does not exist.
-
-ATTENTION: With the --proxy setting of the Cygwin setup, it is possible to
-supply a proxy server, but if this parameter is "", Cygwin setup might use proxy
-settings from previous setups. If you once did a Cygwin setup behind a firewall
-and now want to do a Cygwin setup without a firewall, use the -cygquiet=N
-setting to perform a GUI install, where you can adjust the proxy setting.
-
-===== -cygrepo =====
-
-The online repository, from which Cygwin packages are downloaded.
-
-Note: although most repositories end with Cygwin32, they are good for 32 and 64 bit Cygwin.
-
-Default value: http://ftp.inf.tu-dresden.de/software/windows/Cygwin32
-
->>>>> If you are not in Europe, you might want to change this! <<<<<
-
-
-===== -cygcache =====
-
-The local cache folder for Cygwin repositories.
-
-You can also copy files here from a backup/reference and set -cyglocal.
-The setup will then not download/update from the internet but only use the local cache.
-
-Default value: <folder of MakeCoq_MinGW.bat>\Cygwin_cache
-
-
-===== -cyglocal =====
-
-Control if the Cygwin setup uses the latest version from the internet or the version as is in the local folder.
-
-Possible values:
-
-Y: Install exactly the Cygwin version from the local repository cache.
-   Don't update from the internet.
-
-N: Download the latest Cygwin version from the internet.
-   Update the local repository cache with the latest version.
-
-Default value: N
-
-
-===== -cygquiet =====
-
-Control if the Cygwin setup runs quietly or interactive.
-
-Possible values:
-
-Y: Install Cygwin quietly without user interaction.
-
-N: Install Cygwin interactively (allows to select additional packages).
-
-Default value: Y
-
-
-===== -srccache =====
-
-The local cache folder for ocaml/coq/... sources.
-
-Default value: <folder of MakeCoq_MinGW.bat>\source_cache
-
-
-===== -coqver =====
-
-The version of Coq to download and compile.
-
-Possible values: 8.4pl6, 8.5pl2, 8.5pl3, 8.6
-                 (download from https://coq.inria.fr/distrib/V$COQ_VERSION/files/coq-<version>.tar.gz)
-                 Others versions might work, but are untested.
-                 8.4 is only tested in mode=absolute
-                 
-                 git-v8.6, git-trunk
-                 (download from https://github.com/coq/coq/archive/<version without git->.zip)
-                 
-                 /cygdrive/....
-                 Use local folder. The sources are archived as coq-local.tar.gz
-
-Default value: 8.5pl3
-
-If git- is prepended, the Coq sources are loaded from git.
-
-ATTENTION: with default options, the scripts cache source tar balls in two
-places, the <destination>/build/tarballs folder and the <scripts>/source_cache
-folder. If you modified something in git, you need to delete the cached tar ball
-in both places!
-
-===== -gtksrc =====
-
-Control if GTK and its prerequisites are build from sources or if binary MinGW packages from Cygwin are used
-
-Possible values:
-
-Y: Build GTK from sources, takes about 90 minutes extra.
-   This is useful, if you want to debug/fix GTK or library issues.
-
-N: Use prebuilt MinGW libraries from Cygwin
-
-
-===== -threads =====
-
-Control the maximum number of make threads for modules which support parallel make.
-
-Possible values: 1..N. 
-                 Should not be more than 1.5x the number of cores.
-                 Should not be more than available RAM/2GB (e.g. 4 for 8GB)
-
-===== -addon =====
-
-Enable build and installation of selected Coq package (can be repeated for
-selecting more packages)
-
-==================== TODO ====================
-
-- Check for spaces in destination paths
-- Check for = signs in all paths (DOS commands don't work with paths with = in it, possibly even when quoted)
-- Installer doesn't remove OCAMLLIB environment variables (it is in the script, but doesn't seem to work)
-- CoqIDE doesn't find theme files
-- Finish / test mingw_in_Cygwin mode (coqide doesn't start, coqc slow cause of scanning complete share folder)
-- Possibly create/login as specific user to bash (not sure if it makes sense - need to create additional bash login link then)
-- maybe move share/doc/menhir somewhere else (reduces coqc startup time)
-- Use original installed file list for removing files in uninstaller 
-
-==================== Issues with relocation ====================
-
-Coq and OCaml are built in a specific folder and are not really intended for relocation e.g. by an installer.
-Some absolute paths in config files are patched in coq_new.nsi.
-
-Coq is made fairly relocatable by first configuring it with PREFIX=./ and then PREFIX=<installdir>.
-OCaml is made relocatable mostly by defining the OCAMLLIB environment variable and by patching some files.
-If you have issues with one of the remaining (unpatched) files below, please let me know.
-
-Text files patched by the installer:
-
-./ocamllib/ld.conf
-./etc/findlib.conf:destdir="D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib"
-./etc/findlib.conf:path="D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib"
-
-Text files containing the install folder path after install:
-
-./libocaml/Makefile.config:PREFIX=D:/bin/coq64_buildtest_reloc_ocaml20
-./libocaml/Makefile.config:LIBDIR=D:/bin/coq64_buildtest_reloc_ocaml20/libocaml
-./libocaml/site-lib/findlib/Makefile.config:OCAML_CORE_BIN=/cygdrive/d/bin/coq64_buildtest_reloc_ocaml20/bin
-./libocaml/site-lib/findlib/Makefile.config:OCAML_SITELIB=D:/bin/coq64_buildtest_reloc_ocaml20\libocaml\site-lib
-./libocaml/site-lib/findlib/Makefile.config:OCAMLFIND_BIN=D:/bin/coq64_buildtest_reloc_ocaml20\bin
-./libocaml/site-lib/findlib/Makefile.config:OCAMLFIND_CONF=D:/bin/coq64_buildtest_reloc_ocaml20\etc\findlib.conf
-./libocaml/topfind:#directory "D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib/findlib";;
-./libocaml/topfind:  Topdirs.dir_load Format.err_formatter "D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib/findlib/findlib.cma";
-./libocaml/topfind:  Topdirs.dir_load Format.err_formatter "D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib/findlib/findlib_top.cma";
-./libocaml/topfind:(* #load "D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib/findlib/findlib.cma";; *)
-./libocaml/topfind:(* #load "D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib/findlib/findlib_top.cma";; *)
-
-Binary files containing the build folder path after install:
-
-$ find . -type f -exec grep "Cygwin_coq64_buildtest_reloc_ocaml20" {} /dev/null \;
-Binary file ./bin/coqtop.byte.exe matches
-Binary file ./bin/coqtop.exe matches
-Binary file ./bin/ocamldoc.exe matches
-Binary file ./bin/ocamldoc.opt.exe matches
-Binary file ./libocaml/ocamldoc/odoc_info.a matches
-Binary file ./libocaml/ocamldoc/odoc_info.cma matches
-
-Binary files containing the install folder path after install:
-
-$ find . -type f -exec grep "coq64_buildtest_reloc_ocaml20" {} /dev/null \;
-Binary file ./bin/coqc.exe matches
-Binary file ./bin/coqchk.exe matches
-Binary file ./bin/coqdep.exe matches
-Binary file ./bin/coqdoc.exe matches
-Binary file ./bin/coqide.exe matches
-Binary file ./bin/coqtop.byte.exe matches
-Binary file ./bin/coqtop.exe matches
-Binary file ./bin/coqworkmgr.exe matches
-Binary file ./bin/coq_makefile.exe matches
-Binary file ./bin/menhir matches
-Binary file ./bin/ocaml.exe matches
-Binary file ./bin/ocamlc.exe matches
-Binary file ./bin/ocamlc.opt.exe matches
-Binary file ./bin/ocamldebug.exe matches
-Binary file ./bin/ocamldep.exe matches
-Binary file ./bin/ocamldep.opt.exe matches
-Binary file ./bin/ocamldoc.exe matches
-Binary file ./bin/ocamldoc.opt.exe matches
-Binary file ./bin/ocamlfind.exe matches
-Binary file ./bin/ocamlmklib.exe matches
-Binary file ./bin/ocamlobjinfo.exe matches
-Binary file ./bin/ocamlopt.exe matches
-Binary file ./bin/ocamlopt.opt.exe matches
-Binary file ./bin/ocamlprof.exe matches
-Binary file ./bin/ocamlrun.exe matches
-Binary file ./bin/ocpp5.exe matches
-Binary file ./lib/config/coq_config.cmo matches
-Binary file ./lib/config/coq_config.o matches
-Binary file ./lib/grammar/grammar.cma matches
-Binary file ./lib/ide/coqide/ide_win32_stubs.o matches
-Binary file ./lib/lib/clib.a matches
-Binary file ./lib/lib/clib.cma matches
-Binary file ./lib/libcoqrun.a matches
-Binary file ./libocaml/compiler-libs/ocamlcommon.a matches
-Binary file ./libocaml/compiler-libs/ocamlcommon.cma matches
-Binary file ./libocaml/dynlink.cma matches
-Binary file ./libocaml/expunge.exe matches
-Binary file ./libocaml/extract_crc.exe matches
-Binary file ./libocaml/libcamlrun.a matches
-Binary file ./libocaml/ocamlbuild/ocamlbuildlib.a matches
-Binary file ./libocaml/ocamlbuild/ocamlbuildlib.cma matches
-Binary file ./libocaml/ocamldoc/odoc_info.a matches
-Binary file ./libocaml/ocamldoc/odoc_info.cma matches
-Binary file ./libocaml/site-lib/findlib/findlib.a matches
-Binary file ./libocaml/site-lib/findlib/findlib.cma matches
-Binary file ./libocaml/site-lib/findlib/findlib.cmxs matches
diff --git a/dev/build/windows/configure_profile.sh b/dev/build/windows/configure_profile.sh
deleted file mode 100644
index 7e606b5544..0000000000
--- a/dev/build/windows/configure_profile.sh
+++ /dev/null
@@ -1,43 +0,0 @@
-#!/bin/bash
-
-###################### COPYRIGHT/COPYLEFT ######################
-
-# (C) 2016 Intel Deutschland GmbH
-# Author: Michael Soegtrop
-#
-# Released to the public by Intel under the
-# GNU Lesser General Public License Version 2.1 or later
-# See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-###################### CONFIGURE CYGWIN USER PROFILE FOR BUILDING COQ ######################
-
-rcfile=~/.bash_profile
-donefile=~/.bash_profile.upated
-
-# to learn about `exec >> $file`, see https://www.tldp.org/LDP/abs/html/x17974.html
-exec >> $rcfile
-
-if [ ! -f $donefile ] ; then
-
-    if [ "$1" != "" ] && [ "$1" != " " ]; then
-      echo export http_proxy="http://$1"
-      echo export https_proxy="http://$1"
-      echo export ftp_proxy="http://$1"
-    fi
-
-    mkdir -p "$RESULT_INSTALLDIR_CFMT/bin"
-
-    # A tightly controlled path helps to avoid issues
-    # Note: the order is important: first have the cygwin binaries, then the mingw binaries in the path!
-    # Note: /bin is mounted at /usr/bin and /lib at /usr/lib and it is common to use /usr/bin in PATH
-    # See cat /proc/mounts
-    echo "export PATH=/usr/local/bin:/usr/bin:$RESULT_INSTALLDIR_CFMT/bin:/usr/$TARGET_ARCH/sys-root/mingw/bin:/cygdrive/c/Windows/system32:/cygdrive/c/Windows"
-
-    # find and xargs complain if the environment is larger than (I think) 8k.
-    # ORIGINAL_PATH (set by cygwin) can be a few k and exceed the limit
-    echo unset ORIGINAL_PATH
-    # Other installations of OCaml will mess up things
-    echo unset OCAMLLIB
-
-    touch $donefile
-fi
diff --git a/dev/build/windows/difftar-folder.sh b/dev/build/windows/difftar-folder.sh
deleted file mode 100644
index 543ca972cd..0000000000
--- a/dev/build/windows/difftar-folder.sh
+++ /dev/null
@@ -1,89 +0,0 @@
-#!/bin/bash
-
-###################### COPYRIGHT/COPYLEFT ######################
-
-# (C) 2016 Intel Deutschland GmbH
-# Author: Michael Soegtrop
-#
-# Released to the public by Intel under the
-# GNU Lesser General Public License Version 2.1 or later
-# See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-###################### DIFF A TAR FILE AND A FOLDER ######################
-
-set -o nounset
-
-# Print usage
-
-if [ "$#" -lt 2 ] ; then
-  echo 'Diff a tar (or compressed tar) file with a folder'
-  echo 'difftar-folder.sh <tarfile> <folder> [strip]'
-  echo '<tarfile> is the name of the tar file do diff with (required)'
-  echo '<folder> is the name of the folder to diff with (required)'
-  echo '<strip> is the number of path components to strip from tar file (default is 0)'
-  echo 'All files in the tar file must have at least <strip> path components.'
-  echo 'This also adds new files from folder.new, if folder.new exists'
-  exit 1
-fi
-
-# Parse parameters
-
-tarfile=$1
-folder=$2
-
-if [ "$#" -ge 3 ] ; then
-  strip=$3
-else
-  strip=0
-fi
-
-# Get path prefix if --strip is used
-
-if [ "$strip" -gt 0 ] ; then
-  # Get the path/name of the first file from the tar and extract the first $strip path components
-  # This assumes that the first file in the tar file has at least $strip many path components
-  prefix=$(tar -t -f "$tarfile" | head -1 | cut -d / -f -$strip)/
-else
-  prefix=
-fi
-
-# Original folder
-
-orig=$folder.orig
-mkdir -p "$orig"
-
-# New amd empty filefolder
-
-new=$folder.new
-empty=$folder.empty
-mkdir -p "$empty"
-
-# Print information (this is ignored by patch)
-
-echo diff/patch file created on "$(date)" with:
-echo difftar-folder.sh "$@"
-echo TARFILE=    "$tarfile"
-echo FOLDER=     "$folder"
-echo TARSTRIP=   "$strip"
-echo TARPREFIX=  "$prefix"
-echo ORIGFOLDER= "$orig"
-
-# Make sure tar uses english output (for Mod time differs)
-export LC_ALL=C
-
-# Search all files with a deviating modification time using tar --diff
-tar --diff -a -f "$tarfile" --strip $strip --directory "$folder" | grep "Mod time differs" | while read -r file ; do
-  # Substitute ': Mod time differs' with nothing
-  file=${file/: Mod time differs/}
-  # Check if file exists
-  if [ -f "$folder/$file" ] ; then
-    # Extract original file
-    tar -x -a -f "$tarfile" --strip $strip --directory "$orig" "$prefix$file"
-    # Compute diff
-    diff -u "$orig/$file" "$folder/$file"
-  fi
-done
-
-if [ -d "$new" ] ; then
-  diff -u -r --unidirectional-new-file "$empty" "$new"
-fi
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
deleted file mode 100755
index 4c376f563f..0000000000
--- a/dev/build/windows/makecoq_mingw.sh
+++ /dev/null
@@ -1,2033 +0,0 @@
-#!/bin/bash
-
-###################### COPYRIGHT/COPYLEFT ######################
-
-# (C) 2016..2018 Intel Deutschland GmbH
-# Author: Michael Soegtrop
-#
-# Released to the public by Intel under the
-# GNU Lesser General Public License Version 2.1 or later
-# See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-#
-# With very valuable help on building GTK from
-#   https://wiki.gnome.org/Projects/GTK+/Win32/MSVCCompilationOfGTKStack
-#   http://www.gaia-gis.it/spatialite-3.0.0-BETA/mingw64_how_to.html
-
-###################### Script safety and debugging settings ######################
-
-set -o nounset
-set -o errexit
-set -x
-# Print current wall time as part of the xtrace
-export PS4='+\t '
-
-# Set this to 1 if all module directories shall be removed before build (no incremental make)
-RMDIR_BEFORE_BUILD=1
-
-###################### NOTES #####################
-
-# - This file goes together with MakeCoq_ForMignGW.bat, which sets up cygwin
-#   with all required packages and then calls this script.
-#
-# - This script uses set -o errexit, so if anything fails, the script will stop
-#
-# - cygwin provided mingw64 packages like mingw64-x86_64-zlib are installed to
-#   /usr/$TARGET_ARCH/sys-root/mingw, so we use this as install prefix
-#
-# - if mingw64-x86_64-pkg-config is installed BEFORE building libpng or pixman,
-#   the .pc files are properly created in /usr/$TARGET_ARCH/sys-root/mingw/lib/pkgconfig
-#
-# - pango and some others uses pkg-config executable names without path, which doesn't work in cross compile mode
-#   There are several possible solutions
-#     1.) patch build files to get the prefix from pkg-config and use $prefix/bin/ as path
-#         - doesn't work for pango because automake goes wild
-#         - mingw tools are not able to handle cygwin path (they need absolute windows paths)
-#     2.) export PATH=$PATH:/usr/$TARGET_ARCH/sys-root/mingw/bin
-#         - a bit dangerous because this exposes much more than required
-#         - mingw tools are not able to handle cygwin path (they need absolute windows paths)
-#     3.) Install required tools via cygwin modules libglib2.0-devel and libgdk_pixbuf2.0-devel
-#         - Possibly version compatibility issues
-#         - Possibly mingw/cygwin compatibility issues, e.g. when building font or terminfo databases
-#     4.) Build required tools for mingw and cygwin
-#         - Possibly mingw/cygwin compatibility issues, e.g. when building font or terminfo databases
-#
-#   We use method 3 below
-#   Method 2 can be tried by putting the cross tools in the path before the cygwin tools (in configure_profile.sh)
-#
-# - It is tricky to build 64 bit binaries with 32 bit cross tools and vice versa.
-#   This is because the linker needs to load DLLs from C:\windows\system32, which contains
-#   both 32 bit and 64 bit DLLs, and which one you get depends by some black magic on if the using
-#   app is a 32 bit or 64 bit app. So better build 32 bit mingw with 32 bit cygwin and 64 with 64.
-#   Alternatively the required 32 bit or 64 bit DLLs need to be copied with a 32 bit/64bit cp to some
-#   folder without such black magic.
-#
-# - The file selection for the Coq Windows Installer is done with make install (unlike the original script)
-#   Relocatble builds are first configured with prefix=./ then build and then
-#   reconfigured with prefix=<installroot> before make install.
-
-
-###################### ARCHITECTURES #####################
-
-# The OS on which the build of the tool/lib runs
-BUILD=$(gcc -dumpmachine)
-
-# The OS on which the tool runs
-# "`find /bin -name "*mingw32-gcc.exe"`" -dumpmachine
-HOST=$TARGET_ARCH
-
-# The OS for which the tool creates code/for which the libs are
-TARGET=$TARGET_ARCH
-
-# Cygwin uses different arch name for 32 bit than mingw/gcc
-case $ARCH in
-  x86_64) CYGWINARCH=x86_64 ;;
-  i686)   CYGWINARCH=x86 ;;
-  *)      false ;;
-esac
-
-###################### PATHS #####################
-
-# Name and create some 'global' folders
-PATCHES=/build/patches
-BUILDLOGS=/build/buildlogs
-FLAGFILES=/build/flagfiles
-TARBALLS=/build/tarballs
-FILELISTS=/build/filelists
-
-mkdir -p $BUILDLOGS
-mkdir -p $FLAGFILES
-mkdir -p $TARBALLS
-mkdir -p $FILELISTS
-cd /build
-
-# Create source cache folder
-mkdir -p "$SOURCE_LOCAL_CACHE_CFMT"
-
-# sysroot prefix for the above /build/host/target combination
-# This must be in MFMT (C:/.../) because the OCaml library path is based on it and OCaml is a MinGW application.
-PREFIXMINGW=$CYGWIN_INSTALLDIR_MFMT/usr/$TARGET_ARCH/sys-root/mingw
-
-# Install / Prefix folder for COQ
-PREFIXCOQ=$RESULT_INSTALLDIR_MFMT
-
-# Install / Prefix folder for OCaml
-if [ "$INSTALLOCAML" == "Y" ]; then
-  PREFIXOCAML=$PREFIXCOQ
-else
-  PREFIXOCAML=$PREFIXMINGW
-fi
-
-mkdir -p "$PREFIXMINGW/bin"
-mkdir -p "$PREFIXCOQ/bin"
-mkdir -p "$PREFIXOCAML/bin"
-
-# This is required for building addons and plugins
-# This must be CFMT (/cygdrive/c/...) otherwise coquelicot 3.0.2 configure fails.
-# coquelicot uses which ${COQBIN}/coqc to check if coqc exists. This does not work with COQBIN in MFMT.
-export COQBIN=$RESULT_INSTALLDIR_CFMT/bin/
-# This must be MFMT (C:/) otherwise bignums 68a7a3d7e0b21985913a6c3ee12067f4c5ac4e20 fails
-export COQLIB=$RESULT_INSTALLDIR_MFMT/lib/coq/
-
-###################### Copy Cygwin Setup Info #####################
-
-# Copy Cygwin repo ini file and installed files db to tarballs folder.
-# Both files together document the exact selection and version of cygwin packages.
-# Do this as early as possible to avoid changes by other setups (the repo folder is shared).
-
-# Escape URL to folder name
-CYGWIN_REPO_FOLDER=${CYGWIN_REPOSITORY}/
-CYGWIN_REPO_FOLDER=${CYGWIN_REPO_FOLDER//:/%3a}
-CYGWIN_REPO_FOLDER=${CYGWIN_REPO_FOLDER//\//%2f}
-
-# Copy files
-cp "$CYGWIN_LOCAL_CACHE_WFMT/$CYGWIN_REPO_FOLDER/$CYGWINARCH/setup.ini" $TARBALLS
-cp /etc/setup/installed.db $TARBALLS
-
-# Gtksourceview3 needs python but Cygwin now only installs python2
-ln -s -f /usr/bin/python2 /usr/bin/python
-
-###################### LOGGING #####################
-
-# The folder which receives log files
-mkdir -p buildlogs
-LOGS=$(pwd)/buildlogs
-
-# The current log target (first part of the log file name)
-LOGTARGET=other
-
-# For an explanation of ${COQREGTESTING:-N} search for ${parameter:-word} in
-# http://pubs.opengroup.org/onlinepubs/009695399/utilities/xcu_chap02.html
-
-if [ "${COQREGTESTING:-N}" == "Y" ] ; then
-  # If COQREGTESTING, log to log files only
-  # 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.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.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.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")
-  logn() {
-    { local -; set +x; } 2> /dev/null
-    LOGTARGETEX=$1
-    shift
-    "$@" >"$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.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.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.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")
-  logn() {
-    { local -; set +x; } 2> /dev/null
-    LOGTARGETEX=$1
-    shift
-    "$@" > >(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
-
-###################### 'UNFIX' SED #####################
-
-# In Cygwin SED used to do CR-LF to LF conversion, but since sed 4.4-1 this was changed
-# We replace sed with a shell script which restores the old behavior for piped input
-
-#if [ -f /bin/sed.exe ]
-#then
-#  mv /bin/sed.exe /bin/sed_orig.exe
-#fi
-#cat  > /bin/sed << EOF
-##!/bin/sh
-#dos2unix | /bin/sed_orig.exe "$@"
-#EOF
-#chmod a+x /bin/sed
-
-###################### UTILITY FUNCTIONS #####################
-
-# ------------------------------------------------------------------------------
-# Get a source tar ball, expand and patch it
-# - get source archive from $SOURCE_LOCAL_CACHE_CFMT or online using wget
-# - create build folder
-# - extract source archive
-# - patch source file if patch exists
-#
-# Parameters
-# $1 file server name including protocol prefix
-# $2 file name (without extension)
-# $3 file extension
-# $4 [optional] number of path levels to strip from tar (usually 1)
-# $5 [optional] module name (if different from archive)
-# $6 [optional] expand folder name (if different from module name)
-# $7 [optional] module base name (used as 2nd choice for patches, defaults to $5)
-# ------------------------------------------------------------------------------
-
-function get_expand_source_tar {
-  # Handle optional parameters
-  if [ "$#" -ge 4 ] ; then
-    strip=$4
-  else
-    strip=1
-  fi
-
-  if [ "$#" -ge 5 ] ; then
-    name=$5
-  else
-    name=$2
-  fi
-
-  if [ "$#" -ge 6 ] ; then
-    folder=$6
-  else
-    folder=$name
-  fi
-
-  if [ "$#" -ge 7 ] ; then
-    basename=$7
-  else
-    basename=$name
-  fi
-
-  # Set logging target
-  logtargetold=$LOGTARGET
-  LOGTARGET=$name
-
-  # Get the source archive either from the source cache or online
-  if [ ! -f "$TARBALLS/$name.$3" ] ; then
-    if [ -f "$SOURCE_LOCAL_CACHE_CFMT/$name.$3" ] ; then
-      cp "$SOURCE_LOCAL_CACHE_CFMT/$name.$3" "$TARBALLS"
-    else
-      wget --progress=dot:giga "$1/$2.$3"
-      if file -i "$2.$3" | grep text/html; then
-        echo Download failed: "$1/$2.$3"
-        echo The file wget downloaded is an html file:
-        cat "$2.$3"
-        exit 1
-      fi
-      if [ ! "$2.$3" == "$name.$3" ] ; then
-        mv "$2.$3" "$name.$3"
-      fi
-      mv "$name.$3" "$TARBALLS"
-      # Save the source archive in the source cache
-      if [ -d "$SOURCE_LOCAL_CACHE_CFMT" ] ; then
-        cp "$TARBALLS/$name.$3" "$SOURCE_LOCAL_CACHE_CFMT"
-      fi
-    fi
-  fi
-
-  # Remove build directory (clean build)
-  if [ $RMDIR_BEFORE_BUILD -eq 1 ] ; then
-    rm -f -r "$folder"
-  fi
-
-  # Create build directory and cd
-  mkdir -p "$folder"
-  cd "$folder"
-
-  # Extract source archive
-  if [ "$3" == "zip" ] ; then
-    log1 unzip "$TARBALLS/$name.$3"
-    if [ "$strip" == "1" ] ; then
-      # move subfolders of root folders one level up
-      find "$(ls)" -mindepth 1 -maxdepth 1 -exec mv -- "{}" . \;
-    else
-      echo "Unzip strip count not supported"
-      exit 1
-    fi
-  else
-    logn untar tar xvaf "$TARBALLS/$name.$3" --strip $strip
-  fi
-
-  # Patch if patch file exists
-  # First try specific patch file name then generic patch file name
-  # Note: set -o errexit does not work inside a function called in an if, so exit explicity.
-  if [ -f "$PATCHES/$name.patch" ] ; then
-    log1 patch -p1 -i "$PATCHES/$name.patch" || exit 1
-  elif  [ -f "$PATCHES/$basename.patch" ] ; then
-    log1 patch -p1 -i "$PATCHES/$basename.patch" || exit 1
-  fi
-
-  # Go back to base folder
-  cd ..
-
-  LOGTARGET=$logtargetold
-}
-
-# ------------------------------------------------------------------------------
-# Prepare a module build
-# - check if build is already done (name.finished file exists) - if so return 1
-# - create name.started
-# - get source archive from $SOURCE_LOCAL_CACHE_CFMT or online using wget
-# - create build folder
-# - cd to build folder and extract source archive
-# - create bin_special subfolder and add it to $PATH
-# - remember things for build_post
-#
-# Parameters
-# $1 file server name including protocol prefix
-# $2 file name (without extension)
-# $3 file extension
-# $4 [optional] number of path levels to strip from tar (usually 1)
-# $5 [optional] module name (if different from archive)
-# $6 [optional] module base name (used as 2nd choice for patches, defaults to $5)
-# ------------------------------------------------------------------------------
-
-function build_prep {
-  # Handle optional parameters
-  if [ "$#" -ge 4 ] ; then
-    strip=$4
-  else
-    strip=1
-  fi
-
-  if [ "$#" -ge 5 ] ; then
-    name=$5
-  else
-    name=$2
-  fi
-
-  if [ "$#" -ge 6 ] ; then
-    basename=$6
-  else
-    basename=$name
-  fi
-
-  # Set installer section to not set by default
-  installersection=
-
-  # Check if build is already done
-  if [ ! -f "$FLAGFILES/$name.finished" ] ; then
-    BUILD_PACKAGE_NAME=$name
-    BUILD_OLDPATH=$PATH
-    BUILD_OLDPWD=$(pwd)
-    LOGTARGET=$name
-
-    touch "$FLAGFILES/$name.started"
-
-    get_expand_source_tar "$1" "$2" "$3" "$strip" "$name" "$name" "$basename"
-
-    cd "$name"
-
-    # Create a folder and add it to path, where we can put special binaries
-    # The path is restored in build_post
-    mkdir bin_special
-    PATH=$(pwd)/bin_special:$PATH
-
-    return 0
-  else
-    return 1
-  fi
-}
-
-# ------------------------------------------------------------------------------
-# Like build_prep, but gets the data from an entry in ci-basic-overlay.sh
-# This assumes the following definitions exist in ci-basic-overlay.sh
-# $1_CI_REF
-# $1_CI_ARCHIVEURL
-# $1_CI_GITURL
-# ATTENTION: variables in ci-basic-overlay.sh are loaded by load_overlay_data.
-# load_overlay_data is is called at the end of make_coq (even if the build is skipped)
-#
-# Parameters
-# $1 base name of module in ci-basic-overlay.sh, e.g. mathcomp, bignums, ...
-# ------------------------------------------------------------------------------
-
-function build_prep_overlay {
-  urlvar=$1_CI_ARCHIVEURL
-  gitvar=$1_CI_GITURL
-  refvar=$1_CI_REF
-  url=${!urlvar}
-  git=${!gitvar}
-  ref=${!refvar}
-  ver=$(git ls-remote "$git" "refs/heads/$ref" | cut -f 1)
-  if [[ "$ver" == "" ]]; then
-      # $1_CI_REF must have been a tag or hash, not a branch
-      ver="$ref"
-  fi
-  build_prep "$url" "$ver" tar.gz 1 "$1-$ver" "$1"
-}
-
-# ------------------------------------------------------------------------------
-# Load overlay version variables from ci-basic-overlay.sh
-# ------------------------------------------------------------------------------
-
-function load_overlay_data {
-  if [ -n "${GITLAB_CI-}" ]; then
-    export CI_BRANCH="$CI_COMMIT_REF_NAME"
-    if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]]; then
-      export CI_PULL_REQUEST="${CI_BRANCH#pr-}"
-    else
-      export CI_PULL_REQUEST=""
-    fi
-  else
-    export CI_BRANCH=""
-    export CI_PULL_REQUEST=""
-  fi
-
-  . /build/ci-basic-overlay.sh
-}
-
-# ------------------------------------------------------------------------------
-# Finalize a module build
-# - create name.finished
-# - go back to base folder
-# ------------------------------------------------------------------------------
-
-function build_post {
-  if [ ! -f "$FLAGFILES/$BUILD_PACKAGE_NAME.finished" ]; then
-    cd "$BUILD_OLDPWD"
-    touch "$FLAGFILES/$BUILD_PACKAGE_NAME.finished"
-    PATH=$BUILD_OLDPATH
-    LOGTARGET=other
-    installer_addon_end
-  fi
-}
-
-# ------------------------------------------------------------------------------
-# Build and install a module using the standard configure/make/make install process
-# - prepare build (as above)
-# - configure
-# - make
-# - make install
-# - finalize build (as above)
-#
-# parameters
-# $1 file server name including protocol prefix
-# $2 file name (without extension)
-# $3 file extension
-# $4 patch function to call between untar and configure (or true if none)
-# $5.. extra configure arguments
-# ------------------------------------------------------------------------------
-
-function build_conf_make_inst {
-  if build_prep "$1" "$2" "$3" ; then
-    $4
-    logn configure ./configure --build="$BUILD" --host="$HOST" --target="$TARGET" --prefix="$PREFIXMINGW" "${@:5}"
-    # shellcheck disable=SC2086
-    log1 make $MAKE_OPT
-    log2 make install
-    log2 make clean
-    build_post
-  fi
-}
-
-# ------------------------------------------------------------------------------
-# Install all files given by a glob pattern to a given folder
-#
-# parameters
-# $1 source path
-# $2 pattern (in '')
-# $3 target folder
-# ------------------------------------------------------------------------------
-
-function install_glob {
-  SRCDIR=$(realpath -m $1)
-  DESTDIR=$(realpath -m $3)
-  ( cd "$SRCDIR" && find . -maxdepth 1 -type f -name "$2" -exec install -D -T  "$SRCDIR"/{} "$DESTDIR"/{} \; )
-}
-
-# ------------------------------------------------------------------------------
-# Recursively Install all files given by a glob pattern to a given folder
-#
-# parameters
-# $1 source path
-# $2 pattern (in '')
-# $3 target folder
-# ------------------------------------------------------------------------------
-
-function install_rec {
-  SRCDIR=$(realpath -m $1)
-  DESTDIR=$(realpath -m $3)
-  ( cd "$SRCDIR" && find . -type f -name "$2" -exec install -D -T  "$SRCDIR"/{} "$DESTDIR"/{} \; )
-}
-
-# ------------------------------------------------------------------------------
-# Write a file list of the target folder
-# The file lists are used to create file lists for the windows installer
-# Don't overwrite an existing file list
-#
-# parameters
-# $1 name of file list
-# ------------------------------------------------------------------------------
-
-function list_files {
-  if [ ! -e "/build/filelists/$1" ] ; then
-    ( cd "$PREFIXCOQ" && find . -type f | sort > /build/filelists/"$1" )
-  fi
-}
-
-# ------------------------------------------------------------------------------
-# Write a file list of the target folder
-# The file lists are used to create file lists for the windows installer
-# Do overwrite an existing file list
-#
-# parameters
-# $1 name of file list
-# ------------------------------------------------------------------------------
-
-function list_files_always {
-  ( cd "$PREFIXCOQ" && find . -type f | sort > /build/filelists/"$1" )
-}
-
-# ------------------------------------------------------------------------------
-# Compute the set difference of two file lists
-#
-# parameters
-# $1 name of list A-B (set difference of set A minus set B)
-# $2 name of list A
-# $3 name of list B
-# ------------------------------------------------------------------------------
-
-function diff_files {
-  # See http://www.catonmat.net/blog/set-operations-in-unix-shell/ for file list set operations
-  comm -23 <(sort "/build/filelists/$2") <(sort "/build/filelists/$3") > "/build/filelists/$1"
-}
-
-# ------------------------------------------------------------------------------
-# Filter a list of files with a regular expression
-#
-# parameters
-# $1 name of output file list
-# $2 name of input file list
-# $3 name of filter regexp
-# ------------------------------------------------------------------------------
-
-function filter_files {
-  grep -E "$3" "/build/filelists/$2" > "/build/filelists/$1"
-}
-
-# ------------------------------------------------------------------------------
-# Convert a file list to NSIS installer format
-#
-# parameters
-# $1 name of file list file (output file is the same with extension .nsi)
-# ------------------------------------------------------------------------------
-
-function files_to_nsis {
-  # Split the path in the file list into path and filename and create SetOutPath and File instructions
-  # Note: File /oname cannot be used, because it does not create the paths as SetOutPath does
-  # Note: I didn't check if the redundant SetOutPath instructions have a bad impact on installer size or install time
-  tr '/' '\\' < "/build/filelists/$1" | sed -r 's/^\.(.*)\\([^\\]+)$/SetOutPath $INSTDIR\\\1\nFile ${COQ_SRC_PATH}\\\1\\\2/' > "/build/filelists/$1.nsh"
-}
-
-# ------------------------------------------------------------------------------
-# Create an nsis installer addon section
-#
-# parameters
-# $1 identifier of installer section and base name of file list files
-# $2 human readable name of section
-# $3 description of section
-# $4 flags (space separated list of keywords): off = default off
-#
-# $1 must be a valid NSIS identifier!
-# ------------------------------------------------------------------------------
-
-function installer_addon_section {
-  installersection=$1
-  list_files "addon_pre_$installersection"
-
-  echo 'LangString' "DESC_$1" '${LANG_ENGLISH}' "\"$3\"" >> "/build/filelists/addon_strings.nsh"
-
-  echo '!insertmacro MUI_DESCRIPTION_TEXT' '${'"Sec_$1"'}' '$('"DESC_$1"')' >> "/build/filelists/addon_descriptions.nsh"
-
-  local sectionoptions=
-  if [[ "$4" == *off* ]] ; then sectionoptions+=" /o" ; fi
-
-  echo "Section $sectionoptions \"$2\" Sec_$1" >> "/build/filelists/addon_sections.nsh"
-  echo 'SetOutPath "$INSTDIR\"' >> "/build/filelists/addon_sections.nsh"
-  echo '!include "..\..\..\filelists\addon_'"$1"'.nsh"' >> "/build/filelists/addon_sections.nsh"
-  echo 'SectionEnd' >> "/build/filelists/addon_sections.nsh"
-}
-
-# ------------------------------------------------------------------------------
-# Start an installer addon dependency group
-#
-# parameters
-# $1 identifier of the section which depends on other sections
-# The parameters must match the $1 parameter of a installer_addon_section call
-# ------------------------------------------------------------------------------
-
-dependencysections=
-
-function installer_addon_dependency_beg {
-  installer_addon_dependency "$1"
-  dependencysections="$1 $dependencysections"
-}
-
-# ------------------------------------------------------------------------------
-# End an installer addon dependency group
-# ------------------------------------------------------------------------------
-
-function installer_addon_dependency_end {
-  set -- $dependencysections
-  shift
-  dependencysections="$*"
-}
-
-# ------------------------------------------------------------------------------
-# Create an nsis installer addon dependency entry
-# This needs to be bracketed with installer_addon_dependencies_beg/end
-#
-# parameters
-# $1 identifier of the section on which other sections might depend
-# The parameters must match the $1 parameter of a installer_addon_section call
-# ------------------------------------------------------------------------------
-
-function installer_addon_dependency {
-  for section in $dependencysections ; do
-    echo '${CheckSectionDependency} ${Sec_'"$section"'} ${Sec_'"$1"'} '"'$section' '$1'" >> "/build/filelists/addon_dependencies.nsh"
-  done
-}
-
-# ------------------------------------------------------------------------------
-# Finish an installer section after an addon build
-#
-# This creates the file list files
-#
-# parameters: none
-# ------------------------------------------------------------------------------
-
-function installer_addon_end {
-  if [ -n "$installersection" ]; then
-    list_files "addon_post_$installersection"
-    diff_files "addon_$installersection" "addon_post_$installersection" "addon_pre_$installersection"
-    files_to_nsis "addon_$installersection"
-  fi
-}
-
-# ------------------------------------------------------------------------------
-# Set all timeouts in all .v files to 1000
-# Since timeouts can lead to CI failures, this is useful
-#
-# parameters: none
-# ------------------------------------------------------------------------------
-
-function coq_set_timeouts_1000 {
-  find . -type f -name '*.v' -print0 | xargs -0 sed -i 's/timeout\s\+[0-9]\+/timeout 1000/g'
-}
-
-###################### MODULE BUILD FUNCTIONS #####################
-
-##### SED #####
-
-function make_sed {
-  if build_prep https://ftp.gnu.org/gnu/sed/  sed-4.2.2  tar.gz ; then
-    logn configure ./configure
-    log1 make $MAKE_OPT
-    log2 make install
-    log2 make clean
-    build_post
-  fi
-}
-
-##### LIBPNG #####
-
-function make_libpng {
-  build_conf_make_inst  http://prdownloads.sourceforge.net/libpng  libpng-1.6.34  tar.gz  true
-}
-
-##### PIXMAN #####
-
-function make_pixman {
-  build_conf_make_inst  http://cairographics.org/releases  pixman-0.34.0  tar.gz  true
-}
-
-##### FREETYPE #####
-
-function make_freetype {
-  build_conf_make_inst  http://sourceforge.net/projects/freetype/files/freetype2/2.9.1  freetype-2.9.1  tar.bz2  true
-}
-
-##### EXPAT #####
-
-function make_expat {
-  build_conf_make_inst  http://sourceforge.net/projects/expat/files/expat/2.1.0  expat-2.1.0  tar.gz  true
-}
-
-##### FONTCONFIG #####
-
-function make_fontconfig {
-  make_freetype
-  make_expat
-  # CONFIGURE PARAMETERS
-  # build/install fails without --disable-docs
-  build_conf_make_inst  http://www.freedesktop.org/software/fontconfig/release  fontconfig-2.12.93  tar.gz  true  --disable-docs
-}
-
-##### ICONV #####
-
-function make_libiconv {
-  build_conf_make_inst  http://ftp.gnu.org/pub/gnu/libiconv  libiconv-1.15  tar.gz  true
-}
-
-##### UNISTRING #####
-
-function make_libunistring {
-  build_conf_make_inst  http://ftp.gnu.org/gnu/libunistring  libunistring-0.9.5  tar.xz  true
-}
-
-##### NCURSES #####
-
-function make_ncurses {
-  # NOTE: ncurses is not required below. This is just kept for documentary purposes in case I need it later.
-  #
-  # NOTE: make install fails building the terminfo database because
-  # : ${TIC_PATH:=unknown} in run_tic.sh
-  # As a result pkg-config .pc files are not generated
-  # Also configure of gettext gives two "considers"
-  # checking where terminfo library functions come from... not found, consider installing GNU ncurses
-  # checking where termcap library functions come from... not found, consider installing GNU ncurses
-  # gettext make/make install work anyway
-  #
-  # CONFIGURE PARAMETERS
-  # --enable-term-driver --enable-sp-funcs is required for mingw (see README.MinGW)
-  # additional changes
-  # ADD --with-pkg-config
-  # ADD --enable-pc-files
-  # ADD --without-manpages
-  # REM --with-pthread
-  build_conf_make_inst  http://ftp.gnu.org/gnu/ncurses  ncurses-5.9  tar.gz  true  --disable-home-terminfo --enable-reentrant --enable-sp-funcs --enable-term-driver --enable-interop --with-pkg-config --enable-pc-files --without-manpages
-}
-
-##### GETTEXT #####
-
-function make_gettext {
-  # Cygwin packet dependencies: (not 100% sure) libiconv-devel,libunistring-devel,libncurses-devel
-  # Cygwin packet dependencies for gettext users: (not 100% sure) gettext-devel,libgettextpo-devel
-  # gettext configure complains that ncurses is also required, but it builds without it
-  # Ncurses is tricky to install/configure for mingw64, so I dropped ncurses
-  make_libiconv
-  make_libunistring
-  build_conf_make_inst  http://ftp.gnu.org/pub/gnu/gettext  gettext-0.19  tar.gz  true
-}
-
-##### LIBFFI #####
-
-function make_libffi {
-  # NOTE: The official download server is down  ftp://sourceware.org/pub/libffi/libffi-3.2.1.tar.gz
-  build_conf_make_inst  http://www.mirrorservice.org/sites/sourceware.org/pub/libffi  libffi-3.2.1  tar.gz  true
-}
-
-##### LIBEPOXY #####
-
-function make_libepoxy {
-  build_conf_make_inst  https://github.com/anholt/libepoxy/releases/download/v1.3.1  libepoxy-1.3.1  tar.bz2  true
-}
-
-##### LIBPCRE #####
-
-function make_libpcre {
-  build_conf_make_inst  ftp://ftp.csx.cam.ac.uk/pub/software/programming/pcre  pcre-8.39    tar.bz2  true
-}
-
-function make_libpcre2 {
-  build_conf_make_inst  ftp://ftp.csx.cam.ac.uk/pub/software/programming/pcre  pcre2-10.22  tar.bz2  true
-}
-
-##### GLIB #####
-
-function make_glib {
-  # Cygwin packet dependencies: mingw64-x86_64-zlib
-  make_gettext
-  make_libffi
-  make_libpcre
-
-  build_conf_make_inst  http://ftp.gnome.org/pub/gnome/sources/glib/2.57  glib-2.57.1  tar.xz  true
-
-}
-
-##### ATK #####
-
-function make_atk {
-  make_gettext
-  make_glib
-  build_conf_make_inst  http://ftp.gnome.org/pub/gnome/sources/atk/2.30  atk-2.30.0  tar.xz  true
-}
-
-##### PIXBUF #####
-
-function make_gdk-pixbuf {
-  # Cygwin packet dependencies: mingw64-x86_64-zlib
-  make_libpng
-  make_gettext
-  make_glib
-  # CONFIGURE PARAMETERS
-  # --with-included-loaders=yes statically links the image file format handlers
-  # This avoids "Cannot open pixbuf loader module file '/usr/x86_64-w64-mingw32/sys-root/mingw/lib/gdk-pixbuf-2.0/2.10.0/loaders.cache': No such file or directory"
-  build_conf_make_inst  http://ftp.gnome.org/pub/GNOME/sources/gdk-pixbuf/2.38  gdk-pixbuf-2.38.0  tar.xz  true  --with-included-loaders=yes
-}
-
-##### CAIRO #####
-
-function make_cairo {
-  # Cygwin packet dependencies: mingw64-x86_64-zlib
-  make_libpng
-  make_glib
-  make_pixman
-  make_fontconfig
-  build_conf_make_inst  http://cairographics.org/releases  rcairo-1.16.2  tar.xz  true
-}
-
-##### PANGO #####
-
-function make_pango {
-  make_cairo
-  make_glib
-  make_fontconfig
-  build_conf_make_inst  http://ftp.gnome.org/pub/GNOME/sources/pango/1.42  pango-1.42.4  tar.xz  true
-}
-
-##### GTK3 #####
-
-function make_gtk3 {
-
-  if [ "$GTK_FROM_SOURCES" == "Y" ]; then
-
-      make_glib
-      make_atk
-      make_pango
-      make_gdk-pixbuf
-      make_cairo
-      make_libepoxy
-      build_conf_make_inst  http://ftp.gnome.org/pub/gnome/sources/gtk+/3.24  gtk+-3.24.5  tar.xz  true
-  fi
-
-  # make all incl. tests and examples runs through fine
-  # make install fails with issue with
-  #
-  # make[5]: Entering directory '/home/soegtrop/GTK/gtk+-3.16.7/demos/gtk-demo'
-  # test -n "" || ../../gtk/gtk-update-icon-cache --ignore-theme-index --force "/usr/x86_64-w64-mingw32/sys-root/mingw/share/icons/hicolor"
-  # gtk-update-icon-cache.exe: Failed to open file /usr/x86_64-w64-mingw32/sys-root/mingw/share/icons/hicolor/.icon-theme.cache : No such file or directory
-  # Makefile:1373: recipe for target 'install-update-icon-cache' failed
-  # make[5]: *** [install-update-icon-cache] Error 1
-  # make[5]: Leaving directory '/home/soegtrop/GTK/gtk+-3.16.7/demos/gtk-demo'
-}
-
-##### LIBXML2 #####
-
-function make_libxml2 {
-  # Cygwin packet dependencies: libtool automake
-  # Note: latest release version 2.9.2 fails during configuring lzma, so using 2.9.1
-  # Note: python binding requires <sys/select.h> which doesn't exist on cygwin
-  if build_prep https://git.gnome.org/browse/libxml2/snapshot  libxml2-2.9.1  tar.xz ; then
-    # ./autogen.sh --build=$BUILD --host=$HOST --target=$TARGET --prefix="$PREFIXMINGW" --disable-shared --without-python
-    # shared library required by gtksourceview
-    ./autogen.sh --build="$BUILD" --host="$HOST" --target="$TARGET" --prefix="$PREFIXMINGW" --without-python
-    # shellcheck disable=SC2086
-    log1 make $MAKE_OPT all
-    log2 make install
-    log2 make clean
-    build_post
-  fi
-}
-
-##### GTK-SOURCEVIEW3 #####
-
-function make_gtk_sourceview3 {
-  # Cygwin packet dependencies: intltool
-  # Note: this is always built from sources cause of a bug in the cygwin delivery.
-  # Just dependencies are only built if we build from sources
-  if [ "$GTK_FROM_SOURCES" == "Y" ]; then
-    make_gtk3
-    make_libxml2
-  fi
-  build_conf_make_inst  https://download.gnome.org/sources/gtksourceview/3.24  gtksourceview-3.24.11  tar.xz  make_arch_pkg_config
-}
-
-##### LN replacement #####
-
-# Note: this does support symlinks, but symlinks require special user rights on Windows.
-# ocamlbuild uses symlinks to link the executables in the build folder to the base folder.
-# For this purpose hard links are better.
-
-function make_ln {
-  if [ ! -f $FLAGFILES/myln.finished ] ; then
-    touch $FLAGFILES/myln.started
-    mkdir -p myln
-    ( cd myln
-    cp $PATCHES/ln.c .
-    "$TARGET_ARCH-gcc" -DUNICODE -D_UNICODE -DIGNORE_SYMBOLIC -mconsole -o ln.exe ln.c
-    install -D ln.exe "$PREFIXCOQ/bin/ln.exe"
-    )
-    touch $FLAGFILES/myln.finished
-  fi
-}
-
-##### ARCH-pkg-config replacement #####
-
-# cygwin replaced ARCH-pkg-config with a shell script, which doesn't work e.g. for dune on Windows.
-# This builds a binary replacement for the shell script and puts it into the bin_special folder.
-# There is no global installation since it is module specific what pkg-config is needed under what name.
-
-function make_arch_pkg_config {
-  gcc -DARCH="$TARGET_ARCH" -o bin_special/pkg-config.exe $PATCHES/pkg-config.c
-}
-
-##### OCAML #####
-
-function make_ocaml {
-  if build_prep https://github.com/ocaml/ocaml/archive 4.10.2 tar.gz 1 ocaml-4.10.2 ; then
-    # see https://github.com/ocaml/ocaml/blob/4.08/README.win32.adoc
-
-    # get flexdll sources into folder ./flexdll
-    get_expand_source_tar https://github.com/alainfrisch/flexdll/archive 0.37 tar.gz 1 flexdll-0.37 flexdll
-
-    # We don't want to mess up Coq's directory structure so put the OCaml library in a separate folder
-    logn configure ./configure --build=i686-pc-cygwin --host="$TARGET_ARCH" --prefix="$PREFIXOCAML" --libdir="$PREFIXOCAML/libocaml"
-
-    log2 make flexdll $MAKE_OPT
-    # Note the next command might change after 4.09.x to just make
-    # see        https://github.com/ocaml/ocaml/blob/4.09/README.win32.adoc
-    # compare to https://github.com/ocaml/ocaml/blob/4.10/README.win32.adoc
-    log2 make world.opt $MAKE_OPT
-    log2 make flexlink.opt $MAKE_OPT
-    log2 make install $MAKE_OPT
-
-    # Move license files and other into into special folder
-    if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then
-      mkdir -p "$PREFIXOCAML/license_readme/ocaml"
-      # 4.01 installs these files, 4.02 doesn't. So delete them and copy them from the sources.
-      rm -f ./*.txt
-      cp LICENSE      "$PREFIXOCAML/license_readme/ocaml/License.txt"
-      cp INSTALL.adoc "$PREFIXOCAML/license_readme/ocaml/Install.txt"
-      cp README.adoc  "$PREFIXOCAML/license_readme/ocaml/ReadMe.txt"
-      cp README.win32.adoc "$PREFIXOCAML/license_readme/ocaml/ReadMeWin32.txt"
-      cp VERSION      "$PREFIXOCAML/license_readme/ocaml/Version.txt"
-      cp Changes      "$PREFIXOCAML/license_readme/ocaml/Changes.txt"
-    fi
-
-    # Since 4.07 this library is part of ocaml
-    mkdir -p "$PREFIXOCAML/libocaml/site-lib/seq/"
-    cat > "$PREFIXOCAML/libocaml/site-lib/seq/META" <<EOT
-name="seq"
-version="[distributed with OCaml 4.07 or above]"
-description="dummy backward-compatibility package for iterators"
-requires=""
-EOT
-
-    build_post
-  fi
-}
-
-##### OCAML EXTRA TOOLS #####
-
-function make_ocaml_tools {
-  make_findlib
-}
-
-##### OCAML EXTRA LIBRARIES #####
-
-function make_ocaml_libs {
-  make_num
-  make_zarith
-  make_findlib
-  make_lablgtk
-}
-
-##### Ocaml num library #####
-function make_num {
-  make_ocaml
-  # We need this commit due to windows fixed, IMHO this is better than patching v1.1.
-  if build_prep https://github.com/ocaml/num/archive 7dd5e935aaa2b902585b3b2d0e55ad9b2442fff0 zip 1 num-1.1-7d; then
-    log2 make all
-    # log2 make test
-    log2 make install
-    log2 make clean
-    build_post
-  fi
-}
-
-function make_zarith {
-  make_ocaml
-  if build_prep https://github.com/ocaml/Zarith/archive release-1.10 tar.gz 1 zarith-1.10; then
-    logn configure ./configure
-    log1 make
-    log2 make install
-    build_post
-  fi
-}
-
-##### OCAMLBUILD #####
-
-function make_ocamlbuild {
-  make_ocaml
-  if build_prep https://github.com/ocaml/ocamlbuild/archive 0.14.0 tar.gz 1 ocamlbuild-0.14.0; then
-    log2 make configure OCAML_NATIVE=true OCAMLBUILD_PREFIX=$PREFIXOCAML OCAMLBUILD_BINDIR=$PREFIXOCAML/bin OCAMLBUILD_LIBDIR=$PREFIXOCAML/lib
-    log1 make $MAKE_OPT
-    log2 make install
-    build_post
-  fi
-}
-
-##### FINDLIB Ocaml library manager #####
-
-function make_findlib {
-  make_ocaml
-  make_ocamlbuild
-  if build_prep http://download.camlcity.org/download/ findlib-1.8.1 tar.gz 1; then
-    logn configure ./configure -bindir "$PREFIXOCAML\\bin" -sitelib "$PREFIXOCAML\\libocaml\\site-lib" -config "$PREFIXOCAML\\etc\\findlib.conf"
-    # Note: findlib doesn't support -j 8, so don't pass MAKE_OPT
-    log2 make all
-    log2 make opt
-    log2 make install
-    log2 make clean
-    # Add Coq install library path to ocamlfind config file
-    # $(ocamlfind printconf conf | tr -d '\r') is the name of the config file
-    # printf "%q" "$PREFIXCOQ/lib" | sed -e 's/\\/\\\\/g' is the coq lib path double escaped for sed
-    sed -i -e 's|path="\(.*\)"|path="\1;'$(printf "%q" "$PREFIXCOQ/lib" | sed -e 's/\\/\\\\/g')'"|' $(ocamlfind printconf conf | tr -d '\r')
-    build_post
-  fi
-}
-
-##### Dune build system #####
-
-function make_dune {
-  make_ocaml
-
-  if build_prep https://github.com/ocaml/dune/archive/ 2.0.0 tar.gz 1 dune-2.0.0 ; then
-
-    log2 make release
-    log2 make install
-
-    # Dune support libs, we don't install glob and action-plugin as
-    # they are not needed by Coq
-    logn dune-private-build dune build -p dune-private-libs @install
-    logn dune-private-install dune install dune-private-libs
-
-    logn dune-configurator-build dune build -p dune-configurator @install
-    logn dune-configurator-install dune install dune-configurator
-
-    logn dune-build-info dune build -p dune-build-info @install
-    logn dune-build-info dune install dune-build-info
-
-    build_post
-  fi
-}
-
-##### MENHIR Ocaml Parser Generator #####
-
-function make_menhir {
-  make_ocaml
-  make_findlib
-  make_ocamlbuild
-  if build_prep https://gitlab.inria.fr/fpottier/menhir/-/archive/20200525 menhir-20200525 tar.gz 1 ; then
-    # ToDo: don't know if this is the intended / most reliable to do it, but it works
-    log2 dune build @install
-    log2 dune install menhir menhirSdk menhirLib
-    build_post
-  fi
-}
-
-##### CAMLP5 Ocaml Preprocessor #####
-
-function make_camlp5 {
-  make_ocaml
-  make_findlib
-
-  if build_prep https://github.com/camlp5/camlp5/archive rel711 tar.gz 1 camlp5-rel711; then
-    logn configure ./configure
-    # Somehow my virus scanner has the boot.new/SAVED directory locked after the move for a second => repeat until success
-    sed -i 's/mv boot.new boot/until mv boot.new boot; do sleep 1; done/' Makefile
-    # shellcheck disable=SC2086
-    log1 make world.opt $MAKE_OPT
-    log2 make install
-    cp lib/*.a "$PREFIXOCAML/libocaml/camlp5/"
-    log2 make clean
-    # For some reason META is not built / copied, but it is required
-    log2 make -C etc META
-    mkdir -p "$PREFIXOCAML/libocaml/site-lib/camlp5/"
-    cp etc/META "$PREFIXOCAML/libocaml/site-lib/camlp5/"
-    log2 make clean
-    build_post
-  fi
-}
-
-##### LABLGTK Ocaml GTK binding #####
-
-# Note: when rebuilding lablgtk by deleting the .finished file,
-# also delete <root>\usr\x86_64-w64-mingw32\sys-root\mingw\lib\site-lib
-# Otherwise make install fails
-
-function make_ocaml_cairo2 {
-  if build_prep https://github.com/Chris00/ocaml-cairo/archive 0.6 tar.gz 1 ocaml_cairo2-0.6; then
-    make_arch_pkg_config
-
-    log2 dune build cairo2.install
-    log2 dune install cairo2
-    # See https://github.com/ocaml/dune/issues/2921
-    # log2 dune clean
-    build_post
-
-  fi
-}
-
-function make_lablgtk {
-  make_ocaml
-  make_findlib
-  make_dune
-  make_gtk3
-  make_gtk_sourceview3
-  make_ocaml_cairo2
-
-  if build_prep https://github.com/garrigue/lablgtk/archive 3.1.1 tar.gz 1 lablgtk-3.1.1 ; then
-    make_arch_pkg_config
-
-    # lablgtk3 includes more packages that are not relevant for Coq,
-    # such as gtkspell
-    log2 dune build -p lablgtk3
-    log2 dune install lablgtk3
-
-    log2 dune build -p lablgtk3-sourceview3
-    log2 dune install lablgtk3-sourceview3
-
-    # See https://github.com/ocaml/dune/issues/2921
-    # log2 dune clean
-    build_post
-  fi
-}
-
-##### Elpi #####
-
-function make_seq {
-  make_ocaml
-  # since 4.07 this package is part of ocaml
-
-}
-
-function make_re {
-  make_ocaml
-  make_dune
-  make_seq
-
-  if build_prep https://github.com/ocaml/ocaml-re/archive 1.9.0 tar.gz 1 ocaml-re; then
-
-    log2 dune build -p re
-    log2 dune install re
-
-    build_post
-  fi
-
-}
-
-function make_elpi {
-  make_ocaml
-  make_findlib
-  make_camlp5
-  make_dune
-  make_re
-
-  if build_prep https://github.com/LPCIC/elpi/archive v1.12.0 tar.gz 1 elpi; then
-
-    log2 dune build -p elpi
-    log2 dune install elpi
-
-    build_post
-
-  fi
-
-}
-
-##### COQ #####
-
-# Copy one DLLfrom cygwin MINGW packages to Coq install folder
-
-function copy_coq_dll {
-  if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then
-    cp "$PREFIXMINGW/bin/$1" "$PREFIXCOQ/bin/$1"
-  fi
-}
-
-# Copy required DLLs from cygwin MINGW packages to Coq install folder
-
-function copy_coq_dlls {
-  # HOW TO CREATE THE DLL LIST
-  # With the list empty, after the build/install is finished, open coqide in dependency walker.
-  # See http://www.dependencywalker.com/
-  # Make sure to use the 32 bit / 64 bit version of depends matching the target architecture.
-  # Select all missing DLLs from the module list, right click "copy filenames"
-  # Delay loaded DLLs from Windows can be ignored (hour-glass icon at begin of line)
-  # Do this recursively until there are no further missing DLLs (File close + reopen)
-  # For running this quickly, just do "cd coq-<ver> ; copy_coq_dlls ; cd .." at the end of this script.
-  # Do the same for coqc and ocamlc (usually doesn't result in additional files)
-
-  copy_coq_dll LIBCAIRO-2.DLL
-  copy_coq_dll LIBFONTCONFIG-1.DLL
-  copy_coq_dll LIBFREETYPE-6.DLL
-  copy_coq_dll LIBGDK-3-0.DLL
-  copy_coq_dll LIBGDK_PIXBUF-2.0-0.DLL
-  copy_coq_dll LIBGLIB-2.0-0.DLL
-  copy_coq_dll LIBGOBJECT-2.0-0.DLL
-  copy_coq_dll LIBGTK-3-0.DLL
-  copy_coq_dll LIBGTKSOURCEVIEW-3.0-1.DLL
-  copy_coq_dll LIBPANGO-1.0-0.DLL
-  copy_coq_dll LIBATK-1.0-0.DLL
-  copy_coq_dll LIBBZ2-1.DLL
-  copy_coq_dll LIBCAIRO-GOBJECT-2.DLL
-  copy_coq_dll LIBEPOXY-0.DLL
-  copy_coq_dll LIBEXPAT-1.DLL
-  copy_coq_dll LIBFFI-6.DLL
-  copy_coq_dll LIBGIO-2.0-0.DLL
-  copy_coq_dll LIBGMODULE-2.0-0.DLL
-  copy_coq_dll LIBINTL-8.DLL
-  copy_coq_dll LIBPANGOCAIRO-1.0-0.DLL
-  copy_coq_dll LIBPANGOWIN32-1.0-0.DLL
-  copy_coq_dll LIBPCRE-1.DLL
-  copy_coq_dll LIBPIXMAN-1-0.DLL
-  copy_coq_dll LIBPNG16-16.DLL
-  copy_coq_dll LIBXML2-2.DLL
-  copy_coq_dll ZLIB1.DLL
-  copy_coq_dll ICONV.DLL
-  copy_coq_dll LIBLZMA-5.DLL
-  copy_coq_dll LIBPANGOFT2-1.0-0.DLL
-  copy_coq_dll LIBHARFBUZZ-0.DLL
-
-  # Depends on if GTK is built from sources
-  if [ "$GTK_FROM_SOURCES" == "Y" ]; then
-    echo "Building GTK from sources is currently not supported"
-    exit 1
-  fi;
-
-  # Architecture dependent files
-  case $ARCH in
-    x86_64) copy_coq_dll LIBGCC_S_SEH-1.DLL ;;
-    i686)   copy_coq_dll LIBGCC_S_SJLJ-1.DLL ;;
-    *)      false ;;
-  esac
-
-  # Win pthread version change
-  copy_coq_dll LIBWINPTHREAD-1.DLL
-}
-
-function copy_coq_objects {
-  # copy objects only from folders which exist in the target lib directory
-  find . -type d | while read -r FOLDER ; do
-    if [ -e "$PREFIXCOQ/lib/coq/$FOLDER" ] ; then
-      install_glob "$FOLDER" '*.cmxa' "$PREFIXCOQ/lib/coq/$FOLDER"
-      install_glob "$FOLDER" '*.cmi'  "$PREFIXCOQ/lib/coq/$FOLDER"
-      install_glob "$FOLDER" '*.cma'  "$PREFIXCOQ/lib/coq/$FOLDER"
-      install_glob "$FOLDER" '*.cmo'  "$PREFIXCOQ/lib/coq/$FOLDER"
-      install_glob "$FOLDER" '*.a'    "$PREFIXCOQ/lib/coq/$FOLDER"
-      install_glob "$FOLDER" '*.o'    "$PREFIXCOQ/lib/coq/$FOLDER"
-    fi
-  done
-}
-
-# Copy required GTK config and support files
-# This must be called from inside the coq build folder!
-
-function copy_coq_gtk {
-
-  glib-compile-schemas $PREFIXMINGW/share/glib-2.0/schemas/
-  echo 'gtk-theme-name = "Default"'     >  "$PREFIXMINGW/etc/gtk-3.0/gtkrc"
-
-  if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then
-    install_glob  "$PREFIXMINGW/etc/gtk-3.0" '*'                                 "$PREFIXCOQ/gtk-3.0"
-    install -D -T "$PREFIXMINGW/share/glib-2.0/schemas/gschemas.compiled"        "$PREFIXCOQ/share/glib-2.0/schemas/gschemas.compiled"
-
-    install_glob  "$PREFIXMINGW/share/gtksourceview-3.0/language-specs" '*'      "$PREFIXCOQ/share/gtksourceview-3.0/language-specs"
-    install -D -T "ide/coqide/coq.lang"                                                 "$PREFIXCOQ/share/gtksourceview-3.0/language-specs/coq.lang"
-    install -D -T "ide/coqide/coq-ssreflect.lang"                                       "$PREFIXCOQ/share/gtksourceview-3.0/language-specs/coq-ssreflect.lang"
-
-    install_glob  "$PREFIXMINGW/share/gtksourceview-3.0/styles" '*'              "$PREFIXCOQ/share/gtksourceview-3.0/styles"
-    install -D -T "ide/coqide/coq_style.xml"                                            "$PREFIXCOQ/share/gtksourceview-3.0/styles/coq_style.xml"
-
-    install_rec   "$PREFIXMINGW/share/themes" '*'                                "$PREFIXCOQ/share/themes"
-
-    FOLDERS=""
-    # The sizes include all default sizes given in index.theme
-    # The types used haven been recorded with ProcMon in an installation with all icons present
-    for SIZE in 16x16 22x22 32x32 48x48; do
-      for TYPE in \
-        actions/bookmark actions/document devices/drive actions/format-text actions/go actions/list \
-        actions/media actions/pan actions/process actions/system actions/window \
-        mimetypes/text places/folder places/user status/dialog
-      do
-        CLASS=$(dirname $TYPE)
-        ICON=$(basename $TYPE)
-        if [[ ! "$FOLDERS" =~ "$SIZE/$CLASS" ]] ;then
-          FOLDERS="$FOLDERS$SIZE/$CLASS,"
-        fi
-        install_rec "/usr/share/icons/Adwaita/$SIZE/$CLASS" "$ICON*"  "$PREFIXCOQ/share/icons/Adwaita/$SIZE/$CLASS"
-      done
-    done
-    echo Folders=$FOLDERS
-    install -D -T "/usr/share/icons/Adwaita/index.theme" "$PREFIXCOQ/share/icons/Adwaita/index.theme"
-    sed -i "s|^Directories=.*|Directories=$FOLDERS|" "$PREFIXCOQ/share/icons/Adwaita/index.theme"
-    gtk-update-icon-cache -f "$PREFIXCOQ/share/icons/Adwaita/"
-
-    # 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
-
-    # mkdir -p "$PREFIXCOQ/ide/coqide"
-    # mv "$COQSHARE"*.png  "$PREFIXCOQ/ide/coqide"
-    # rmdir "$PREFIXCOQ/share/coq" || true
-  fi
-}
-
-# Copy license and other info files
-
-function copy_coq_license {
-  if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then
-    install -D doc/LICENSE                    "$PREFIXCOQ/license_readme/coq/LicenseDoc.txt"
-    install -D LICENSE                        "$PREFIXCOQ/license_readme/coq/License.txt"
-    install -D plugins/micromega/LICENSE.sos  "$PREFIXCOQ/license_readme/coq/LicenseMicromega.txt"
-    # FIXME: this is not the micromega license
-    # It only applies to code that was copied into one single file!
-    install -D README.md                      "$PREFIXCOQ/license_readme/coq/ReadMe.md"
-    install -D INSTALL.md                     "$PREFIXCOQ/license_readme/coq/Install.txt"
-    install -D doc/README.md                  "$PREFIXCOQ/license_readme/coq/ReadMeDoc.md" || true
-  fi
-}
-
-# Main function for creating Coq
-
-function make_coq {
-  make_ocaml
-  make_num
-  make_findlib
-  make_lablgtk
-  if
-    case $COQ_VERSION in
-      # e.g. git-v8.6 => download from https://github.com/coq/coq/archive/v8.6.zip
-      # e.g. git-trunk => download from https://github.com/coq/coq/archive/trunk.zip
-      git-*)
-        COQ_BUILD_PATH=/build/coq-${COQ_VERSION}
-        build_prep https://github.com/coq/coq/archive "${COQ_VERSION##git-}" zip 1 "coq-${COQ_VERSION}"
-        ;;
-
-      # e.g. /cygdrive/d/coqgit
-      /*)
-        # Todo: --exclude-vcs-ignores doesn't work because tools/coqdoc/coqdoc.sty is excluded => fix .gitignore
-        # But this is not a big deal, only 2 files are removed with --exclude-vcs-ignores from a fresch clone
-        COQ_BUILD_PATH=/build/coq-local
-        tar -zcf $TARBALLS/coq-local.tar.gz --exclude-vcs -C "${COQ_VERSION%/*}" "${COQ_VERSION##*/}"
-        build_prep NEVER-DOWNLOADED coq-local tar.gz
-        ;;
-
-      # e.g. 8.6 => https://coq.inria.fr/distrib/8.6/files/coq-8.6.tar.gz
-      *)
-        COQ_BUILD_PATH=/build/coq-$COQ_VERSION
-        build_prep "https://coq.inria.fr/distrib/V$COQ_VERSION/files" "coq-$COQ_VERSION" tar.gz
-        ;;
-    esac
-  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 -with-doc no -prefix ./ -libdir ./lib/coq -mandir ./man
-    elif [ "$INSTALLMODE" == "absolute" ]; then
-      logn configure ./configure -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib/coq" -mandir "$PREFIXCOQ/man"
-    else
-      logn configure ./configure -with-doc no -prefix "$PREFIXCOQ"
-    fi
-
-    # 8.4x doesn't support parallel make
-    if [[ $COQ_VERSION == 8.4* ]] ; then
-      log1 make
-    else
-      # shellcheck disable=SC2086
-      log1 make $MAKE_OPT
-    fi
-
-    if [ "$INSTALLMODE" == "relocatable" ]; then
-      logn reconfigure ./configure -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib/coq" -mandir "$PREFIXCOQ/man"
-    fi
-
-    log2 make install
-    log1 copy_coq_dlls
-    log1 copy_coq_gtk
-
-    if [ "$INSTALLOCAML" == "Y" ]; then
-      copy_coq_objects
-    fi
-
-    log1 copy_coq_license
-
-    # make clean seems to be broken for 8.5pl2
-    # 1.) find | xargs fails on cygwin, can be fixed by sed -i 's|\| xargs rm -f|-exec rm -fv \{\} \+|' Makefile
-    # 2.) clean of test suites fails with "cannot run complexity tests (no bogomips found)"
-    # make clean
-
-    # Copy these files somewhere the plugin builds can find them
-    #logn copy-basic-overlays cp dev/ci/ci-basic-overlay.sh /build/
-
-    build_post
-  fi
-
-  #load_overlay_data
-}
-
-##### GNU Make for MinGW #####
-
-function make_mingw_make {
-  if build_prep http://ftp.gnu.org/gnu/make make-4.2 tar.bz2 ; then
-    # The config.h.win32 file is fine - don't edit it
-    # We need to copy the mingw gcc here as "gcc" - then the batch file will use it
-    cp "/usr/bin/${ARCH}-w64-mingw32-gcc-6.4.0.exe" ./gcc.exe
-    # By some magic cygwin bash can run batch files
-    logn build ./build_w32.bat gcc
-    # Copy make to Coq folder
-    cp GccRel/gnumake.exe "$PREFIXCOQ/bin/make.exe"
-    build_post
-  fi
-}
-
-##### GNU binutils for native OCaml #####
-
-function make_binutils {
-  if build_prep http://ftp.gnu.org/gnu/binutils binutils-2.27 tar.gz ; then
-    logn configure ./configure --build="$BUILD" --host="$HOST" --target="$TARGET" --prefix="$PREFIXCOQ" --program-prefix="$TARGET-"
-    # shellcheck disable=SC2086
-    log1 make $MAKE_OPT
-    log2 make install
-    # log2 make clean
-    build_post
-  fi
-}
-
-##### GNU GCC for native OCaml #####
-
-function make_gcc {
-  # Note: the bz2 file is smaller, but decompressing bz2 really takes ages
-  if build_prep ftp://ftp.fu-berlin.de/unix/languages/gcc/releases/gcc-5.4.0 gcc-5.4.0 tar.gz ; then
-    # This is equivalent to "contrib/download_prerequisites" but uses caching
-    # Update versions when updating gcc version
-    get_expand_source_tar  ftp://gcc.gnu.org/pub/gcc/infrastructure  mpfr-2.4.2 tar.bz2 1 mpfr-2.4.2 mpfr
-    get_expand_source_tar  ftp://gcc.gnu.org/pub/gcc/infrastructure  gmp-4.3.2  tar.bz2 1 gmp-4.3.2  gmp
-    get_expand_source_tar  ftp://gcc.gnu.org/pub/gcc/infrastructure  mpc-0.8.1  tar.gz  1 mpc-0.8.1  mpc
-    get_expand_source_tar  ftp://gcc.gnu.org/pub/gcc/infrastructure  isl-0.14   tar.bz2 1 isl-0.14   isl
-
-    # For whatever reason gcc needs this (although it never puts anything into it)
-    # Error: "The directory that should contain system headers does not exist:"
-    # mkdir -p /mingw/include    without --with-sysroot
-    mkdir -p "$PREFIXCOQ/mingw/include"
-
-    # See https://gcc.gnu.org/install/configure.html
-    logn configure ./configure --build="$BUILD" --host="$HOST" --target="$TARGET" \
-        --prefix="$PREFIXCOQ" --program-prefix="$TARGET-" --disable-win32-registry --with-sysroot="$PREFIXCOQ" \
-        --enable-languages=c --disable-nls \
-        --disable-libsanitizer --disable-libssp --disable-libquadmath --disable-libgomp --disable-libvtv --disable-lto
-        # --disable-decimal-float seems to be required
-        # --with-sysroot="$PREFIXMINGW"  results in configure error that this is not an absolute path
-    # shellcheck disable=SC2086
-    log1 make $MAKE_OPT
-    log2 make install
-    # log2 make clean
-    build_post
-  fi
-}
-
-##### Get sources for Cygwin MinGW packages #####
-
-function get_cygwin_mingw_sources {
-  if [ ! -f $FLAGFILES/cygwin_mingw_sources.finished ] ; then
-    touch $FLAGFILES/cygwin_mingw_sources.started
-
-    # Find all installed files with mingw in the name and download the corresponding source code file from cygwin
-    # Steps:
-    # grep /etc/setup/installed.db for mingw       => mingw64-x86_64-gcc-g++ mingw64-x86_64-gcc-g++-5.4.0-2.tar.bz2 1
-    # remove archive ending and trailing number    => mingw64-x86_64-gcc-g++ mingw64-x86_64-gcc-g++-5.4.0-2
-    # replace space with /                         => ${ARCHIVE} = mingw64-x86_64-gcc-g++/mingw64-x86_64-gcc-g++-5.4.0-2
-    # escape + signs using ${var//pattern/replace} => ${ARCHIVEESC} = mingw64-x86_64-gcc-g++/mingw64-x86_64-gcc-g\+\+-5.4.0-2
-    # grep cygwin setup.ini for installed line + next line (the -A 1 option includes and "after context" of 1 line)
-    # Note that the folders of the installed binaries and source are different. So we cannot grep just for the source line.
-    # We could strip off the path and just grep for the file, though.
-    # => install: x86_64/release/mingw64-x86_64-gcc/mingw64-x86_64-gcc-g++/mingw64-x86_64-gcc-g++-5.4.0-2.tar.xz 10163848 2f8cb7ba3e16ac8ce0455af01de490ded09061b1b06a9a8e367426635b5a33ce230e04005f059d4ea7b52580757da1f6d5bae88eba6b9da76d1bd95e8844b705
-    #    source: x86_64/release/mingw64-x86_64-gcc/mingw64-x86_64-gcc-5.4.0-2-src.tar.xz 95565368 03f22997b7173b243fff65ea46a39613a2e4e75fc7e6cf0fa73b7bcb86071e15ba6d0ca29d330c047fb556a5e684cad57cd2f5adb6e794249e4b01fe27f92c95
-    # Take the 2nd field of the last line          => ${SOURCE} = x86_64/release/mingw64-x86_64-gcc/mingw64-x86_64-gcc-5.4.0-2-src.tar.xz
-    # Remove that path part                        => ${SOURCEFILE} = mingw64-x86_64-gcc-5.4.0-2-src.tar.xz
-
-    grep "mingw" /etc/setup/installed.db | sed 's/\.tar\.bz2 [0-1]$//' | sed 's/ /\//'  | while read -r ARCHIVE ; do
-      local ARCHIVEESC=${ARCHIVE//+/\\+}
-      local SOURCE
-      SOURCE=$(grep -E -A 1 "install: ($CYGWINARCH|noarch)/release/[-+_/a-z0-9]*$ARCHIVEESC" $TARBALLS/setup.ini | tail -1 | cut -d " " -f 2)
-      local SOURCEFILE=${SOURCE##*/}
-
-      # Get the source file (either from the source cache or online)
-      if [ ! -f "$TARBALLS/$SOURCEFILE" ] ; then
-        if [ -f "$SOURCE_LOCAL_CACHE_CFMT/$SOURCEFILE" ] ; then
-          cp "$SOURCE_LOCAL_CACHE_CFMT/$SOURCEFILE" $TARBALLS
-        else
-          wget --progress=dot:giga "$CYGWIN_REPOSITORY/$SOURCE"
-          mv "$SOURCEFILE" "$TARBALLS"
-          # Save the source archive in the source cache
-          if [ -d "$SOURCE_LOCAL_CACHE_CFMT" ] ; then
-            cp "$TARBALLS/$SOURCEFILE" "$SOURCE_LOCAL_CACHE_CFMT"
-          fi
-        fi
-      fi
-
-    done
-
-    touch $FLAGFILES/cygwin_mingw_sources.finished
-  fi
-}
-
-##### Coq Windows Installer #####
-
-function make_coq_installer {
-  make_coq
-  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
-  # ocaml_coq: as above + coq
-  # ocaml_coq_addons: as above + lib/user-contrib/*
-
-  # Create coq file list as ocaml_coq / ocaml
-  diff_files coq ocaml_coq ocaml
-
-  # Filter out object files
-  filter_files coq_objects coq '\.(cmxa|cmi|cma|cmo|a|o)$'
-
-  # Filter out plugin object files
-  filter_files coq_objects_plugins coq_objects '/lib/coq/plugins/.*\.(cmxa|cmi|cma|cmo|a|o)$'
-
-  # Coq objects objects required for plugin development = coq objects except those for pre installed plugins
-  diff_files coq_plugindev coq_objects coq_objects_plugins
-
-  # Addons (TODO: including objects that could go to the plugindev thing, but
-  # then one would have to make that package depend on this one, so not
-  # implemented yet)
-  diff_files coq_addons ocaml_coq_addons ocaml_coq
-
-  # Coq files, except objects needed only for plugin development
-  diff_files coq_base coq coq_plugindev
-
-  # Convert section files to NSIS format
-  files_to_nsis coq_base
-  files_to_nsis coq_addons
-  files_to_nsis coq_plugindev
-  files_to_nsis ocaml
-
-  # Get and extract NSIS Binaries
-  if build_prep http://downloads.sourceforge.net/project/nsis/NSIS%202/2.51 nsis-2.51 zip ; then
-    NSIS=$(pwd)/makensis.exe
-    chmod u+x "$NSIS"
-    # Change to Coq folder
-    cd "$COQ_BUILD_PATH"
-    # Copy patched nsi file
-    cp ../patches/coq_new.nsi dev/nsis
-    cp ../patches/StrRep.nsh dev/nsis
-    cp ../patches/ReplaceInFile.nsh dev/nsis
-    VERSION=$(grep '^VERSION=' config/Makefile | cut -d = -f 2 | tr -d '\r')
-    cd dev/nsis
-    logn nsis-installer "$NSIS" -DVERSION="$VERSION" -DARCH="$ARCH" -DCOQ_SRC_PATH="$PREFIXCOQ" -DCOQ_ICON=..\\..\\ide\\coqide\\coq.ico -DCOQ_ADDONS="$COQ_ADDONS" coq_new.nsi
-
-    build_post
-  fi
-}
-
-###################### ADDON COQ LIBRARIES / PLUGINS / TOOLS #####################
-
-# The bignums library
-# Provides BigN, BigZ, BigQ that used to be part of Coq standard library
-
-function make_addon_bignums {
-  installer_addon_dependency bignums
-  if build_prep_overlay bignums; then
-    installer_addon_section bignums "Bignums" "Coq library for fast arbitrary size numbers" ""
-    # To make command lines shorter :-(
-    echo 'COQ_SRC_SUBDIRS:=$(filter-out plugins/%,$(COQ_SRC_SUBDIRS)) plugins/syntax' >> Makefile.coq.local
-    log1 make $MAKE_OPT all
-    log2 make install
-    build_post
-  fi
-}
-
-# Equations plugin
-# A function definition plugin
-
-function make_addon_equations {
-  installer_addon_dependency equations
-  if build_prep_overlay equations; then
-    installer_addon_section equations "Equations" "Coq plugin for defining functions by equations" ""
-    # Note: PATH is automatically saved/restored by build_prep / build_post
-    PATH=$COQBIN:$PATH
-    logn coq_makefile ${COQBIN}coq_makefile -f _CoqProject -o Makefile
-    log1 make $MAKE_OPT
-    log2 make install
-    build_post
-  fi
-}
-
-# mathcomp - ssreflect and mathematical components library
-
-function make_addon_mathcomp {
-  installer_addon_dependency mathcomp
-  if build_prep_overlay mathcomp; then
-    installer_addon_section mathcomp "Math-Components" "Coq library with mathematical components" ""
-    cd mathcomp
-    log1 make $MAKE_OPT
-    log2 make install
-    build_post
-  fi
-}
-
-# ssreflect part of mathcomp
-
-function make_addon_ssreflect {
-  # if mathcomp addon is requested, build this instead
-  if [[ "$COQ_ADDONS" == *mathcomp* ]]; then
-    make_addon_mathcomp
-  else
-    # Note: since either mathcomp or ssreflect is defined, it is fine to name both mathcomp
-    installer_addon_dependency ssreflect
-    if build_prep_overlay mathcomp; then
-      installer_addon_section ssreflect "SSReflect" "Coq support library for small scale reflection plugin" ""
-      cd mathcomp
-      logn make-makefile  make Makefile.coq
-      logn make-ssreflect make $MAKE_OPT -f Makefile.coq ssreflect/all_ssreflect.vo
-      logn make-install   make -f Makefile.coq install
-      build_post
-    fi
-  fi
-}
-
-# UniCoq plugin
-# An alternative unification algorithm
-function make_addon_unicoq {
-  installer_addon_dependency unicoq
-  if build_prep_overlay unicoq; then
-    installer_addon_section unicoq "Unicoq" "Coq plugin for an enhanced unification algorithm" ""
-    log1 coq_makefile -f Make -o Makefile
-    log1 make $MAKE_OPT
-    log2 make install
-    build_post
-  fi
-}
-
-# Mtac2 plugin
-# An alternative typed tactic language
-function make_addon_mtac2 {
-  installer_addon_dependency_beg mtac2
-  make_addon_unicoq
-  installer_addon_dependency_end
-  if build_prep_overlay mtac2; then
-    installer_addon_section mtac2 "Mtac-2" "Coq plugin for a typed tactic language for Coq." ""
-    log1 coq_makefile -f _CoqProject -o Makefile
-    log1 make $MAKE_OPT
-    log2 make install
-    build_post
-  fi
-}
-
-# Menhir parser generator
-
-function make_addon_menhir {
-  make_menhir
-  # If COQ and OCaml are installed to the same folder, there is nothing to do
-  installer_addon_dependency menhir
-  if [ "$PREFIXOCAML" != "$PREFIXCOQ" ] ; then
-    # Just install menhir files required for COQ to COQ target folder
-    if [ ! -f "$FLAGFILES/menhir-addon.finished" ] ; then
-      installer_addon_section menhir "Menhir" "Menhir parser generator windows executable and libraries" ""
-      LOGTARGET=menhir-addon
-      touch "$FLAGFILES/menhir-addon.started"
-      # Menhir executable
-      install_glob "$PREFIXOCAML/bin" 'menhir.exe' "$PREFIXCOQ/bin/"
-      # Menhir PDF doc
-      install_glob "$PREFIXOCAML/doc/menhir/" '*.pdf' "$PREFIXCOQ/doc/menhir/"
-      touch "$FLAGFILES/menhir-addon.finished"
-      LOGTARGET=other
-      installer_addon_end
-    fi
-  fi
-}
-
-# COQ library for Menhir
-
-function make_addon_menhirlib {
-  installer_addon_dependency menhirlib
-  if build_prep_overlay menhirlib; then
-    installer_addon_section menhirlib "Menhirlib" "Coq support library for using Menhir generated parsers in Coq" ""
-    # The supplied makefiles don't work in any way on cygwin
-    # ToDo: dune also doesn't seem to work for the coq files
-    cd coq-menhirlib/src
-    echo -R . MenhirLib > _CoqProject
-    ls -1 *.v >> _CoqProject
-    log1 coq_makefile -f _CoqProject -o Makefile.coq
-    log1 make -f Makefile.coq $MAKE_OPT all
-    logn make-install make -f Makefile.coq install
-    build_post
-  fi
-}
-
-# CompCert
-
-function make_addon_compcert {
-  installer_addon_dependency_beg compcert
-  make_menhir
-  make_addon_menhirlib
-  installer_addon_dependency_end
-  if build_prep_overlay compcert; then
-    installer_addon_section compcert "CompCert" "ATTENTION: THIS IS NOT OPEN SOURCE! CompCert verified C compiler and Clightgen (required for using VST for your own code)" "off"
-    logn configure ./configure -ignore-coq-version -clightgen -prefix "$PREFIXCOQ" -coqdevdir "$PREFIXCOQ/lib/coq/user-contrib/compcert" x86_32-cygwin -use-external-MenhirLib -use-external-Flocq
-    log1 make $MAKE_OPT
-    log2 make install
-    logn install-license-1 install -D -T  "LICENSE" "$PREFIXCOQ/lib/coq/user-contrib/compcert/LICENSE"
-    logn install-license-2 install -D -T  "LICENSE" "$PREFIXCOQ/lib/compcert/LICENSE"
-    build_post
-  fi
-}
-
-# Princeton VST
-
-function install_addon_vst {
-    VSTDEST="$PREFIXCOQ/lib/coq/user-contrib/VST"
-
-    # Install VST .v, .vo, .c and .h files
-    install_rec compcert '*.v' "$VSTDEST/compcert/"
-    install_rec compcert '*.vo' "$VSTDEST/compcert/"
-    install_glob "msl" '*.v' "$VSTDEST/msl/"
-    install_glob "msl" '*.vo' "$VSTDEST/msl/"
-    install_glob "sepcomp" '*.v' "$VSTDEST/sepcomp/"
-    install_glob "sepcomp" '*.vo' "$VSTDEST/sepcomp/"
-    install_glob "floyd" '*.v' "$VSTDEST/floyd/"
-    install_glob "floyd" '*.vo' "$VSTDEST/floyd/"
-    install_glob "progs" '*.v' "$VSTDEST/progs/"
-    install_glob "progs" '*.c' "$VSTDEST/progs/"
-    install_glob "progs" '*.h' "$VSTDEST/progs/"
-    install_glob "veric" '*.v' "$VSTDEST/veric/"
-    install_glob "veric" '*.vo' "$VSTDEST/veric/"
-
-    # Install VST documentation files
-    install_glob "." 'LICENSE' "$VSTDEST"
-    install_glob "." '*.md' "$VSTDEST"
-    install_glob "compcert" '*' "$VSTDEST/compcert"
-    install_glob "doc" '*.pdf' "$VSTDEST/doc"
-
-    # Install VST _CoqProject files
-    install_glob "." '_CoqProject*' "$VSTDEST"
-    install_glob "." '_CoqProject-export' "$VSTDEST/progs"
-}
-
-function vst_patch_compcert_refs {
-  find . -type f -name '*.v' -print0 | xargs -0 sed -E -i \
-    -e 's/(Require\s+(Import\s+|Export\s+)*)compcert\./\1VST.compcert./g' \
-    -e 's/From compcert Require/From VST.compcert Require/g'
-}
-
-function make_addon_vst {
-  installer_addon_dependency vst
-  if build_prep_overlay vst; then
-    installer_addon_section vst "VST" "ATTENTION: SOME INCLUDED COMPCERT PARTS ARE NOT OPEN SOURCE! Verified Software Toolchain for verifying C code" "off"
-    # log1 coq_set_timeouts_1000
-    log1 vst_patch_compcert_refs
-    # The usage of the shell variable ARCH in VST collides with the usage in this shellscript
-    logn make env -u ARCH make IGNORECOQVERSION=true $MAKE_OPT
-    log1 install_addon_vst
-    build_post
-  fi
-}
-
-# coquelicot Real analysis
-
-function make_addon_coquelicot {
-  installer_addon_dependency_beg coquelicot
-  make_addon_ssreflect
-  installer_addon_dependency_end
-  if build_prep_overlay coquelicot; then
-    installer_addon_section coquelicot "Coquelicot" "Coq library for real analysis" ""
-    log1 autoreconf -i -s
-    logn configure ./configure --libdir="$PREFIXCOQ/lib/coq/user-contrib/Coquelicot"
-    logn remake ./remake
-    logn remake-install ./remake install
-    build_post
-  fi
-}
-
-# AAC associative / commutative rewriting
-
-function make_addon_aactactics {
-  installer_addon_dependency aac
-  if build_prep_overlay aac_tactics; then
-    installer_addon_section aac "AAC" "Coq plugin for extensible associative and commutative rewriting" ""
-    log1 make $MAKE_OPT
-    log2 make install
-    build_post
-  fi
-}
-
-# extlib
-
-function make_addon_extlib {
-  installer_addon_dependency extlib
-  if build_prep_overlay ext_lib; then
-    installer_addon_section extlib "Ext-Lib" "Coq library with many reusable general purpose components" ""
-    log1 make $MAKE_OPT
-    log2 make install
-    build_post
-  fi
-}
-
-# SimpleIO
-
-function make_addon_simple_io {
-  installer_addon_dependency simpleIO
-  if build_prep_overlay simple_io; then
-    installer_addon_section simpleIO "SimpleIO" "Coq plugin for reading and writing files directly from Coq code" ""
-    log1 make $MAKE_OPT
-    log2 make install
-    build_post
-  fi
-}
-
-# Quickchick Randomized Property-Based Testing Plugin for Coq
-
-function make_addon_quickchick {
-  installer_addon_dependency_beg quickchick
-  make_addon_ssreflect
-  make_addon_extlib
-  make_addon_simple_io
-  make_ocamlbuild
-  installer_addon_dependency_end
-  if build_prep_overlay quickchick; then
-    installer_addon_section quickchick "QuickChick" "Coq plugin for randomized testing and counter example search" ""
-    log1 make $MAKE_OPT
-    log2 make install
-    build_post
-  fi
-}
-
-# Flocq: Floating point library
-
-function make_addon_flocq {
-  if build_prep_overlay flocq; then
-    installer_addon_section flocq "Flocq" "Coq library for floating point arithmetic" ""
-    log1 autoreconf
-    logn configure ./configure
-    logn remake ./remake --jobs=$MAKE_THREADS
-    logn install ./remake install
-    build_post
-  fi
-}
-
-# Coq-Interval: interval arithmetic and inequality proofs
-
-function make_addon_interval {
-  installer_addon_dependency_beg interval
-  make_addon_mathcomp
-  make_addon_coquelicot
-  make_addon_bignums
-  make_addon_flocq
-  installer_addon_dependency_end
-  if build_prep_overlay interval; then
-    installer_addon_section interval "Interval" "Coq library and tactic for proving real inequalities" ""
-    log1 autoreconf
-    logn configure ./configure
-    logn remake ./remake --jobs=$MAKE_THREADS
-    logn install ./remake install
-    build_post
-  fi
-}
-
-# Gappa: Automatic generation of arithmetic proofs (mostly on limited precision arithmetic)
-
-function install_boost {
-  # The extra tar parameter extracts only the boost headers, not the boost library source code (which is huge and takes a long time)
-  if build_prep https://dl.bintray.com/boostorg/release/1.69.0/source boost_1_69_0 tar.gz 1 boost_1_69_0 boost boost_1_69_0/boost; then
-    # Move extracted boost folder where mingw-gcc can find it
-    mv boost /usr/$TARGET_ARCH/sys-root/mingw/include
-    build_post
-  fi
-}
-
-function copy_gappa_dlls {
-  copy_coq_dll LIBGMP-10.DLL
-  copy_coq_dll LIBMPFR-6.DLL
-  copy_coq_dll LIBSTDC++-6.DLL
-}
-
-function make_addon_gappa_tool {
-  install_boost
-  if build_prep_overlay gappa_tool; then
-    installer_addon_section gappa_tool "Gappa tool" "Stand alone tool for automated generation of numerical arithmetic proofs" ""
-    log1 autoreconf
-    # Note: configure.in seems to reference this file
-    touch stamp-config_h.in
-    logn configure ./configure --build="$HOST" --host="$HOST" --target="$TARGET" --prefix="$PREFIXCOQ"
-    logn remake ./remake --jobs=$MAKE_THREADS
-    logn install ./remake -d install
-    log1 copy_gappa_dlls
-    build_post
-  fi
-}
-
-function make_addon_gappa {
-  make_camlp5
-  installer_addon_dependency_beg gappa
-  make_addon_gappa_tool
-  make_addon_flocq
-  installer_addon_dependency_end
-  if build_prep_overlay gappa_plugin ; then
-    installer_addon_section gappa "Gappa plugin" "Coq plugin for the Gappa tool" ""
-    log1 autoreconf
-    logn configure ./configure
-    logn remake ./remake
-    logn install ./remake install
-    build_post
-  fi
-}
-
-# Elpi: extension language for Coq based. It lets one define commands in tactics
-# in a high level programming language with support for binders and unification
-# variables.
-
-function make_addon_elpi {
-  make_elpi
-  installer_addon_dependency elpi
-  if build_prep_overlay elpi ; then
-    installer_addon_section elpi "Elpi extension language" "Coq plugin for the Elpi extension language" ""
-    logn build make
-    logn installe make install
-    build_post
-  fi
-}
-
-# Hierarchy Builder: high level language to declare a hierarchy of structures
-# compiled down to records and canonical structures.
-
-function make_addon_HB {
-  installer_addon_dependency_beg elpi_hb
-  make_addon_elpi
-  installer_addon_dependency_end
-  if build_prep_overlay elpi_hb ; then
-    installer_addon_section elpi_hb "Hierarchy Builder" "Coq library to declare algebraic hierarchies" ""
-    logn build make
-    logn install make install VFILES=structures.v
-    build_post
-  fi
-}
-
-# Main function for building addons
-
-function make_addons {
-  # Note: ':' is the empty command, which does not produce any output
-  : > "/build/filelists/addon_dependencies.nsh"
-  : > "/build/filelists/addon_strings.nsh"
-  : > "/build/filelists/addon_descriptions.nsh"
-  : > "/build/filelists/addon_sections.nsh"
-
-  for addon in $COQ_ADDONS; do
-    "make_addon_$addon"
-  done
-
-  sort -u -o "/build/filelists/addon_dependencies.nsh" "/build/filelists/addon_dependencies.nsh"
-}
-
-###################### TOP LEVEL BUILD #####################
-
-ocamlfind list || true
-
-make_sed
-make_ocaml
-make_ocaml_tools
-make_ocaml_libs
-
-list_files ocaml
-
-make_coq
-
-if [ "$INSTALLMAKE" == "Y" ] ; then
-  make_mingw_make
-fi
-
-list_files ocaml_coq
-
-make_addons
-
-list_files_always ocaml_coq_addons
-
-if [ "$MAKEINSTALLER" == "Y" ] ; then
-  make_coq_installer
-fi
diff --git a/dev/build/windows/patches_coq/ReplaceInFile.nsh b/dev/build/windows/patches_coq/ReplaceInFile.nsh
deleted file mode 100644
index 27c7eb2fd9..0000000000
--- a/dev/build/windows/patches_coq/ReplaceInFile.nsh
+++ /dev/null
@@ -1,67 +0,0 @@
-; From NSIS Wiki http://nsis.sourceforge.net/ReplaceInFile
-; Modifications:
-; - Replace only once per line
-; - Don't keep original as .old
-; - Use StrRep instead of StrReplace (seems to be cleaner)
-
-Function Func_ReplaceInFile
-  ClearErrors
-
-  Exch $0      ; REPLACEMENT
-  Exch
-  Exch $1      ; SEARCH_TEXT
-  Exch 2
-  Exch $2      ; SOURCE_FILE
-
-  Push $R0     ; SOURCE_FILE file handle
-  Push $R1     ; temporary file handle
-  Push $R2     ; unique temporary file name
-  Push $R3     ; a line to search and replace / save
-  Push $R4     ; shift puffer
-
-  IfFileExists $2 +1 error          ; Check if file exists and open it
-  FileOpen $R0 $2 "r"
-
-  GetTempFileName $R2               ; Create temporary output file
-  FileOpen $R1 $R2 "w"
-
-  loop:                             ; Loop over lines of file
-    FileRead $R0 $R3                ; Read line
-    IfErrors finished
-    Push "$R3"                      ; Replacine string in line once
-    Push "$1"
-    Push "$0"
-    Call Func_StrRep
-    Pop $R3
-    FileWrite $R1 "$R3"             ; Write result
-  Goto loop
-
-  finished:
-    FileClose $R1                   ; Close files
-    FileClose $R0
-    Delete "$2"                     ; Delete original file and rename temporary file to target
-    Rename "$R2" "$2"
-    ClearErrors
-    Goto out
-
-  error:
-    SetErrors
-
-  out:
-  Pop $R4
-  Pop $R3
-  Pop $R2
-  Pop $R1
-  Pop $R0
-  Pop $2
-  Pop $0
-  Pop $1
-FunctionEnd
-
-!macro ReplaceInFile SOURCE_FILE SEARCH_TEXT REPLACEMENT
-  Push "${SOURCE_FILE}"
-  Push "${SEARCH_TEXT}"
-  Push "${REPLACEMENT}"
-  Call Func_ReplaceInFile
-!macroend
-
diff --git a/dev/build/windows/patches_coq/StrRep.nsh b/dev/build/windows/patches_coq/StrRep.nsh
deleted file mode 100644
index d94a9f88b4..0000000000
--- a/dev/build/windows/patches_coq/StrRep.nsh
+++ /dev/null
@@ -1,60 +0,0 @@
-; From NSIS Wiki http://nsis.sourceforge.net/StrRep
-; Slightly modified
-
-Function Func_StrRep
-    Exch $R2 ;new
-    Exch 1
-    Exch $R1 ;old
-    Exch 2
-    Exch $R0 ;string
-    Push $R3
-    Push $R4
-    Push $R5
-    Push $R6
-    Push $R7
-    Push $R8
-    Push $R9
-
-    StrCpy $R3 0
-    StrLen $R4 $R1
-    StrLen $R6 $R0
-    StrLen $R9 $R2
-    loop:
-        StrCpy $R5 $R0 $R4 $R3
-        StrCmp $R5 $R1 found
-        StrCmp $R3 $R6 done
-        IntOp $R3 $R3 + 1 ;move offset by 1 to check the next character
-        Goto loop
-    found:
-        StrCpy $R5 $R0 $R3
-        IntOp $R8 $R3 + $R4
-        StrCpy $R7 $R0 "" $R8
-        StrCpy $R0 $R5$R2$R7
-        StrLen $R6 $R0
-        IntOp $R3 $R3 + $R9 ;move offset by length of the replacement string
-        Goto loop
-    done:
-
-    Pop $R9
-    Pop $R8
-    Pop $R7
-    Pop $R6
-    Pop $R5
-    Pop $R4
-    Pop $R3
-    Push $R0
-    Push $R1
-    Pop $R0
-    Pop $R1
-    Pop $R0
-    Pop $R2
-    Exch $R1
-FunctionEnd
-
-!macro StrRep output string old new
-    Push `${string}`
-    Push `${old}`
-    Push `${new}`
-    Call Func_StrRep
-    Pop ${output}
-!macroend
diff --git a/dev/build/windows/patches_coq/VST.patch b/dev/build/windows/patches_coq/VST.patch
deleted file mode 100644
index d047eb107f..0000000000
--- a/dev/build/windows/patches_coq/VST.patch
+++ /dev/null
@@ -1,14 +0,0 @@
-diff --git a/Makefile b/Makefile
---- a/Makefile
-+++ b/Makefile
-@@ -82,8 +82,8 @@ endif
-
- COMPCERTDIRS=lib common $(ARCHDIRS) cfrontend flocq exportclight $(BACKEND)
-
--COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT)/$(d) compcert.$(d))
--EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT)/$(d) compcert.$(d))
-+COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT)/$(d) VST.compcert.$(d))
-+EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT)/$(d) VST.compcert.$(d))
- # for ITrees
- ifeq ($(wildcard InteractionTrees/the?ries),"InteractionTrees/theories")
- EXTFLAGS:=$(EXTFLAGS) -Q InteractionTrees/theories ITree
diff --git a/dev/build/windows/patches_coq/coq_new.nsi b/dev/build/windows/patches_coq/coq_new.nsi
deleted file mode 100644
index 9947965c28..0000000000
--- a/dev/build/windows/patches_coq/coq_new.nsi
+++ /dev/null
@@ -1,330 +0,0 @@
-; This script is used to build the Windows install program for Coq.
-
-; NSIS Modern User Interface
-; Written by Joost Verburg
-; Modified by Julien Narboux, Pierre Letouzey, Enrico Tassi and Michael Soegtrop
-
-; The following command line defines are expected:
-; VERSION      Coq version, e.g. 8.5-pl2
-; ARCH         The target architecture, either x86_64 or i686
-; COQ_SRC_PATH path of Coq installation in Windows or MinGW format (either \\ or /, but with drive letter)
-; COQ_ICON     path of Coq icon file in Windows or MinGW format
-; COQ_ADDONS   list of addons that are shipped
-
-; Enable compression after debugging.
-; SetCompress off
-SetCompressor lzma
-
-!define MY_PRODUCT "Coq" ;Define your own software name here
-!define OUTFILE "coq-${VERSION}-installer-windows-${ARCH}.exe"
-
-!include "MUI2.nsh"
-!include "FileAssociation.nsh"
-!include "StrRep.nsh"
-!include "ReplaceInFile.nsh"
-!include "winmessages.nsh"
-
-Var COQ_SRC_PATH_BS   ; COQ_SRC_PATH with \ instead of /
-Var COQ_SRC_PATH_DBS  ; COQ_SRC_PATH with \\ instead of /
-Var INSTDIR_DBS       ; INSTDIR with \\ instead of \
-
-;--------------------------------
-;Configuration
-
-  Name "Coq"
-
-  ;General
-  OutFile "${OUTFILE}"
-
-  ;Folder selection page
-  InstallDir "C:\${MY_PRODUCT}"
-
-  ;Remember install folder
-  InstallDirRegKey HKCU "Software\${MY_PRODUCT}" ""
-
-;--------------------------------
-;Extra license pages
-
-!macro MUI_PAGE_LICENSE_EXTRA Licensefile Header Subheader Bottom SelFunc
-  !define MUI_PAGE_HEADER_TEXT "${Header}"
-  !define MUI_PAGE_HEADER_SUBTEXT "${Subheader}"
-  !define MUI_LICENSEPAGE_TEXT_BOTTOM "${Bottom}"
-  !define MUI_PAGE_CUSTOMFUNCTION_PRE ${SelFunc}
-  !insertmacro MUI_PAGE_LICENSE "${Licensefile}"
-!macroend
-
-;--------------------------------
-; Check for white spaces
-Function .onVerifyInstDir
-  StrLen $0 "$INSTDIR"
-  StrCpy $1 0
-  ${While} $1 < $0
-    StrCpy $3 $INSTDIR 1 $1
-    StrCmp $3 " " SpacesInPath
-    IntOp $1 $1 + 1
-  ${EndWhile}
-  Goto done
-  SpacesInPath:
-  Abort
-  done:
-FunctionEnd
-
-;--------------------------------
-;Installer Sections
-
-Section "Coq" Sec1
-
-  SetOutPath "$INSTDIR\"
-  !include "..\..\..\filelists\coq_base.nsh"
-
-  ${registerExtension} "$INSTDIR\bin\coqide.exe" ".v" "Coq Script File"
-
-  ;Store install folder
-  WriteRegStr HKCU "Software\${MY_PRODUCT}" "" $INSTDIR
-
-  ;Create uninstaller
-  WriteUninstaller "$INSTDIR\Uninstall.exe"
-  WriteRegStr HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
-      "DisplayName" "Coq Version ${VERSION}"
-  WriteRegStr HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
-      "UninstallString" '"$INSTDIR\Uninstall.exe"'
-  WriteRegStr HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
-      "DisplayVersion" "${VERSION}"
-  WriteRegDWORD HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
-      "NoModify" "1"
-  WriteRegDWORD HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
-      "NoRepair" "1"
-  WriteRegStr HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
-      "URLInfoAbout" "http://coq.inria.fr"
-
-  ; Create start menu entries
-  ; SetOutPath is required for the path in the .lnk files
-  SetOutPath "$INSTDIR"
-  CreateDirectory "$SMPROGRAMS\Coq"
-  ; The first shortcut set here is treated as main application by Windows 7/8.
-  ; Use CoqIDE as main application
-  CreateShortCut "$SMPROGRAMS\Coq\CoqIde.lnk" "$INSTDIR\bin\coqide.exe"
-  CreateShortCut "$SMPROGRAMS\Coq\Coq.lnk" "$INSTDIR\bin\coqtop.exe"
-  WriteINIStr "$SMPROGRAMS\Coq\The Coq HomePage.url" "InternetShortcut" "URL" "http://coq.inria.fr"
-  WriteINIStr "$SMPROGRAMS\Coq\The Coq Standard Library.url" "InternetShortcut" "URL" "http://coq.inria.fr/library"
-  CreateShortCut "$SMPROGRAMS\Coq\Uninstall.lnk" "$INSTDIR\Uninstall.exe" "" "$INSTDIR\Uninstall.exe" 0
-
-SectionEnd
-
-;OCAML Section "Ocaml for native compute and plugin development" Sec2
-;OCAML   SetOutPath "$INSTDIR\"
-;OCAML   !include "..\..\..\filelists\ocaml.nsh"
-;OCAML
-;OCAML   ; Create a few slash / backslash variants of the source and install path
-;OCAML   ; Note: NSIS has variables, written as $VAR and defines, written as ${VAR}
-;OCAML   !insertmacro StrRep $COQ_SRC_PATH_BS  ${COQ_SRC_PATH} "/" "\"
-;OCAML   !insertmacro StrRep $COQ_SRC_PATH_DBS ${COQ_SRC_PATH} "/" "\\"
-;OCAML   !insertmacro StrRep $INSTDIR_DBS      $INSTDIR        "\" "\\"
-;OCAML
-;OCAML   ; Replace absolute paths in some OCaml config files
-;OCAML   ; These are not all, see ReadMe.txt
-;OCAML   !insertmacro ReplaceInFile "$INSTDIR\libocaml\ld.conf" "/"  "\"
-;OCAML   !insertmacro ReplaceInFile "$INSTDIR\libocaml\ld.conf" "$COQ_SRC_PATH_BS"  "$INSTDIR"
-;OCAML   !insertmacro ReplaceInFile "$INSTDIR\etc\findlib.conf" "$COQ_SRC_PATH_DBS" "$INSTDIR_DBS"
-;OCAML SectionEnd
-
-SectionGroup "Coq addons" Sec2
-  !include "..\..\..\filelists\addon_sections.nsh"
-SectionGroupEnd
-
-Section "Coq files for plugin developers" Sec3
-  SetOutPath "$INSTDIR\"
-  !include "..\..\..\filelists\coq_plugindev.nsh"
-SectionEnd
-
-;OCAML Section "OCAMLLIB current user" Sec4
-;OCAML    WriteRegStr HKCU "Environment" "OCAMLLIB" "$INSTDIR\libocaml"
-;OCAML    ; This is required, so that a newly started shell gets the new environment variable
-;OCAML    ; But it really takes a few seconds
-;OCAML    DetailPrint "Broadcasting OCAMLLIB environment variable change (current user)"
-;OCAML    SendMessage ${HWND_BROADCAST} ${WM_WININICHANGE} 0 "STR:Environment" /TIMEOUT=1000
-;OCAML SectionEnd
-
-;OCAML Section "OCAMLLIB all users" Sec5
-;OCAML    WriteRegStr HKLM "SYSTEM\CurrentControlSet\Control\Session Manager\Environment" "OCAMLLIB" "$INSTDIR\libocaml"
-;OCAML    ; This is required, so that a newly started shell gets the new environment variable
-;OCAML    ; But it really takes a few seconds
-;OCAML    DetailPrint "Broadcasting OCAMLLIB environment variable change (all users)"
-;OCAML    SendMessage ${HWND_BROADCAST} ${WM_WININICHANGE} 0 "STR:Environment" /TIMEOUT=1000
-;OCAML SectionEnd
-
-;--------------------------------
-;Section dependencies
-
-; Parameters on the stack:
-; top-0 : section B on which section A dependencies
-; top-1 : section A, which depends on section B
-; top-2 : name of section B
-; top-3 : name of section A
-
-Function CheckSectionDependency
-            ; stack=nameB nameA secB secA rest
-  Exch $R3  ; stack=$R3   nameA secB secA rest; $R3=nameB
-  Exch      ; stack=nameA $R3   secB secA rest
-  Exch $R2  ; stack=$R2   $R3   secB secA rest; $R2=nameA
-  Exch 2    ; stack=secB  $R3   $R2  secA rest
-  Exch $R1  ; stack=$R1   $R3   $R2  secA rest; $R1=secB
-  Exch 3    ; stack=secA  $R3   $R2  $R1  rest;
-  Exch $R0  ; stack=$R0   $R3   $R2  $R1  rest; $R0=secA
-            ; Take care of save order when popping the stack!
-  Push $R4
-  Push $R5
-
-  SectionGetFlags $R0 $R0
-  IntOp $R0 $R0 & ${SF_SELECTED}
-
-  SectionGetFlags $R1 $R4
-  IntOp $R5 $R4 & ${SF_SELECTED}
-
-  ${If} $R0 == ${SF_SELECTED}
-  ${AndIf} $R5 != ${SF_SELECTED}
-
-  IntOp $R5 $R4 | ${SF_SELECTED}
-  SectionSetFlags $R1 $R5
-  MessageBox MB_OK '"$R3" has been selected, because "$R2" depends on it'
-
-  ${EndIf}
-
-  Pop $R5
-  Pop $R4
-  Pop $R0
-  Pop $R3
-  Pop $R2
-  Pop $R1
-FunctionEnd
-
-!macro CheckSectionDependency secA secB nameA nameB
-  Push "${secA}"
-  Push "${secB}"
-  Push "${nameA}"
-  Push "${nameB}"
-  Call CheckSectionDependency
-!macroend
-
-!define CheckSectionDependency "!insertmacro CheckSectionDependency"
-
-Function .onSelChange
-  !include "..\..\..\filelists\addon_dependencies.nsh"
-FunctionEnd
-
-;--------------------------------
-;Modern UI Configuration
-
-; Note: this must be placed after the sections, because below we need to check at compile time
-; if sections exist (by !ifdef <section_index_var>) to decide if the license page must be included.
-; The section index variables are only defined after the section definitions.
-
-  !define MUI_ICON "${COQ_ICON}"
-
-  !insertmacro MUI_PAGE_WELCOME
-  !insertmacro MUI_PAGE_LICENSE "${COQ_SRC_PATH}/license_readme/coq/License.txt"
-  !insertmacro MUI_PAGE_COMPONENTS
-
-  !ifdef Sec_compcert
-    !define LicCompCert_Title "CompCert License Agreement"
-    !define LicCompCert_SubTitle "You selected the CompCert addon. CompCert is not open source. Please review the license terms before installing CompCert!"
-    !define LicCompCert_Bottom "If you accept the terms of the agreement, click I Agree to continue. Otherwise go back and unselect the CompCert addon."
-    !insertmacro MUI_PAGE_LICENSE_EXTRA "${COQ_SRC_PATH}/lib/coq/user-contrib/compcert/LICENSE" "${LicCompCert_Title}" "${LicCompCert_SubTitle}" "${LicCompCert_Bottom}" SelFuncCompCert
-
-    Function SelFuncCompCert
-      ${Unless} ${SectionIsSelected} ${Sec_compcert}
-        Abort
-      ${EndUnless}
-    FunctionEnd
-  !endif
-
-  !ifdef Sec_vst
-    !define LicVST_Title "Princeton VST License Agreement"
-    !define LicVST_SubTitle "You selected the VST addon. VST contains parts of CompCert which are not open source. Please review the license terms before installing VST!"
-    !define LicVST_Bottom "If you accept the terms of the agreement, click I Agree to continue. Otherwise go back and unselect the VST addon."
-    !insertmacro MUI_PAGE_LICENSE_EXTRA "${COQ_SRC_PATH}/lib/coq/user-contrib/VST/LICENSE" "${LicVST_Title}" "${LicVST_SubTitle}" "${LicVST_Bottom}" SelFuncVST
-
-    Function SelFuncVST
-      ${Unless} ${SectionIsSelected} ${Sec_vst}
-        Abort
-      ${EndUnless}
-    FunctionEnd
-  !endif
-
-  !define MUI_DIRECTORYPAGE_TEXT_TOP "Select where to install Coq.  The path MUST NOT include spaces."
-  !insertmacro MUI_PAGE_DIRECTORY
-  !insertmacro MUI_PAGE_INSTFILES
-  !insertmacro MUI_PAGE_FINISH
-
-  !insertmacro MUI_UNPAGE_WELCOME
-  !insertmacro MUI_UNPAGE_CONFIRM
-  !insertmacro MUI_UNPAGE_INSTFILES
-  !insertmacro MUI_UNPAGE_FINISH
-
-;--------------------------------
-;Languages
-
-  !insertmacro MUI_LANGUAGE "English"
-
-;--------------------------------
-;Language Strings
-
-  ;Description
-  LangString DESC_1 ${LANG_ENGLISH} "This package contains Coq and CoqIDE."
-  LangString DESC_2 ${LANG_ENGLISH} "This package contains the following extra Coq packages: ${COQ_ADDONS}"
-  LangString DESC_3 ${LANG_ENGLISH} "This package contains the development files needed in order to build a plugin for Coq."
-  ; LangString DESC_4 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for the current user."
-  ; LangString DESC_5 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for all users."
-  !include "..\..\..\filelists\addon_strings.nsh"
-
-;--------------------------------
-;Descriptions
-
-!insertmacro MUI_FUNCTION_DESCRIPTION_BEGIN
-  !insertmacro MUI_DESCRIPTION_TEXT ${Sec1} $(DESC_1)
-  !insertmacro MUI_DESCRIPTION_TEXT ${Sec2} $(DESC_2)
-  !insertmacro MUI_DESCRIPTION_TEXT ${Sec3} $(DESC_3)
-  ;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec4} $(DESC_4)
-  ;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec5} $(DESC_5)
-  !include "..\..\..\filelists\addon_descriptions.nsh"
-!insertmacro MUI_FUNCTION_DESCRIPTION_END
-
-;--------------------------------
-;Uninstaller Section
-
-Section "Uninstall"
-  ; Files and folders
-  RMDir /r "$INSTDIR\bin"
-  RMDir /r "$INSTDIR\doc"
-  RMDir /r "$INSTDIR\etc"
-  RMDir /r "$INSTDIR\lib"
-  RMDir /r "$INSTDIR\libocaml"
-  RMDir /r "$INSTDIR\share"
-  RMDir /r "$INSTDIR\ide"
-  RMDir /r "$INSTDIR\gtk-2.0"
-  RMDir /r "$INSTDIR\latex"
-  RMDir /r "$INSTDIR\license_readme"
-  RMDir /r "$INSTDIR\man"
-  RMDir /r "$INSTDIR\emacs"
-
-  ; Start Menu
-  Delete "$SMPROGRAMS\Coq\Coq.lnk"
-  Delete "$SMPROGRAMS\Coq\CoqIde.lnk"
-  Delete "$SMPROGRAMS\Coq\Uninstall.lnk"
-  Delete "$SMPROGRAMS\Coq\The Coq HomePage.url"
-  Delete "$SMPROGRAMS\Coq\The Coq Standard Library.url"
-  Delete "$INSTDIR\Uninstall.exe"
-
-  ; Registry keys
-  DeleteRegKey HKCU "Software\${MY_PRODUCT}"
-  DeleteRegKey HKLM "SOFTWARE\Coq"
-  DeleteRegKey HKLM "SOFTWARE\Microsoft\Windows\CurrentVersion\Uninstall\Coq"
-  DeleteRegKey HKCU "Environment\OCAMLLIB"
-  DeleteRegKey HKLM "SYSTEM\CurrentControlSet\Control\Session Manager\Environment\OCAMLLIB"
-  ${unregisterExtension} ".v" "Coq Script File"
-
-  ; Root folders
-  RMDir "$INSTDIR"
-  RMDir "$SMPROGRAMS\Coq"
-
-SectionEnd
diff --git a/dev/build/windows/patches_coq/flexdll-0.37.patch b/dev/build/windows/patches_coq/flexdll-0.37.patch
deleted file mode 100644
index 82806f9ea4..0000000000
--- a/dev/build/windows/patches_coq/flexdll-0.37.patch
+++ /dev/null
@@ -1,19 +0,0 @@
-diff/patch file created on Tue, Feb 19, 2019  9:41:26 PM with:
-difftar-folder.sh tarballs/flexdll-0.37.tar.gz flexdll-0.37 1
-TARFILE= tarballs/flexdll-0.37.tar.gz
-FOLDER= flexdll-0.37
-TARSTRIP= 1
-TARPREFIX= flexdll-0.37/
-ORIGFOLDER= flexdll-0.37.orig
---- flexdll-0.37.orig/cmdline.ml	2017-10-25 10:40:46.000000000 +0200
-+++ flexdll-0.37/cmdline.ml	2019-02-19 21:41:18.157024900 +0100
-@@ -248,6 +248,9 @@
-         String.sub s 0 2 :: String.sub s 2 (String.length s - 2) :: tr rest
-     | s :: rest when String.length s >= 5 && String.sub s 0 5 = "/link" ->
-         "-link" :: String.sub s 5 (String.length s - 5) :: tr rest
-+    (* Convert gcc linker option prefix -Wl, to flexlink linker prefix -link *)
-+    | s :: rest when String.length s >= 6 && String.sub s 0 5 = "-Wl,-" ->
-+        "-link" :: String.sub s 4 (String.length s - 4) :: tr rest
-     | "-arg" :: x :: rest ->
-         tr (Array.to_list (Arg.read_arg x)) @ rest
-     | "-arg0" :: x :: rest ->
diff --git a/dev/build/windows/patches_coq/isl-0.14.patch b/dev/build/windows/patches_coq/isl-0.14.patch
deleted file mode 100644
index f3b8ead1ab..0000000000
--- a/dev/build/windows/patches_coq/isl-0.14.patch
+++ /dev/null
@@ -1,11 +0,0 @@
---- orig.isl-0.14/configure	2014-10-26 08:36:32.000000000 +0100
-+++ isl-0.14/configure	2016-10-10 18:16:01.430224500 +0200
-@@ -8134,7 +8134,7 @@
-      lt_sysroot=`$CC --print-sysroot 2>/dev/null`
-    fi
-    ;; #(
-- /*)
-+ /*|[A-Z]:\\*|[A-Z]:/*)
-    lt_sysroot=`echo "$with_sysroot" | sed -e "$sed_quote_subst"`
-    ;; #(
-  no|'')
diff --git a/dev/build/windows/patches_coq/lablgtk-3.0.beta5.patch b/dev/build/windows/patches_coq/lablgtk-3.0.beta5.patch
deleted file mode 100644
index 1c6a038da9..0000000000
--- a/dev/build/windows/patches_coq/lablgtk-3.0.beta5.patch
+++ /dev/null
@@ -1,76 +0,0 @@
-diff/patch file created on Wed, Feb 20, 2019 11:29:48 AM with:
-difftar-folder.sh tarballs/lablgtk-3.0.beta4.tar.gz lablgtk-3.0.beta4 1
-TARFILE= tarballs/lablgtk-3.0.beta4.tar.gz
-FOLDER= lablgtk-3.0.beta4
-TARSTRIP= 1
-TARPREFIX= lablgtk-3.0.beta4/
-ORIGFOLDER= lablgtk-3.0.beta4.orig
---- lablgtk-3.0.beta4.orig/src/glib.ml	2019-02-11 07:08:17.000000000 +0100
-+++ lablgtk-3.0.beta4/src/glib.ml	2019-02-20 11:28:28.439137100 +0100
-@@ -72,6 +72,8 @@
-   type id
-   external channel_of_descr : Unix.file_descr -> channel
-     = "ml_g_io_channel_unix_new"
-+  external channel_of_descr_socket : Unix.file_descr -> channel
-+    = "ml_g_io_channel_unix_new_socket"
-   external remove : id -> unit = "ml_g_source_remove"
-   external add_watch :
-     cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id
---- lablgtk-3.0.beta4.orig/src/glib.mli	2019-02-11 07:08:17.000000000 +0100
-+++ lablgtk-3.0.beta4/src/glib.mli	2019-02-20 11:28:28.423592200 +0100
-@@ -75,6 +75,7 @@
-   type condition = [ `ERR | `HUP | `IN | `NVAL | `OUT | `PRI]
-   type id
-   val channel_of_descr : Unix.file_descr -> channel
-+  val channel_of_descr_socket : Unix.file_descr -> channel
-   val add_watch :
-     cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id
-   val remove : id -> unit
---- lablgtk-3.0.beta4.orig/src/ml_glib.c	2019-02-11 07:08:17.000000000 +0100
-+++ lablgtk-3.0.beta4/src/ml_glib.c	2019-02-20 11:28:28.455395900 +0100
-@@ -25,6 +25,8 @@
- #include <string.h>
- #include <locale.h>
- #ifdef _WIN32
-+/* to kill a #warning: include winsock2.h before windows.h */
-+#include <winsock2.h>
- #include "win32.h"
- #include <wtypes.h>
- #include <io.h>
-@@ -38,6 +40,11 @@
- #include <caml/callback.h>
- #include <caml/threads.h>
- 
-+#ifdef _WIN32
-+/* for Socket_val */
-+#include <caml/unixsupport.h>
-+#endif
-+
- #include "wrappers.h"
- #include "ml_glib.h"
- #include "glib_tags.h"
-@@ -326,14 +333,23 @@
- 
- #ifndef _WIN32
- ML_1 (g_io_channel_unix_new, Int_val, Val_GIOChannel_noref)
-+CAMLprim value ml_g_io_channel_unix_new_socket (value arg1) {
-+  return Val_GIOChannel_noref (g_io_channel_unix_new (Int_val (arg1))); 
-+}
- 
- #else
- CAMLprim value ml_g_io_channel_unix_new(value wh)
- {
-   return Val_GIOChannel_noref
--    (g_io_channel_unix_new
-+    (g_io_channel_win32_new_fd
-      (_open_osfhandle((long)*(HANDLE*)Data_custom_val(wh), O_BINARY)));
- }
-+
-+CAMLprim value ml_g_io_channel_unix_new_socket(value wh)
-+{
-+  return Val_GIOChannel_noref
-+    (g_io_channel_win32_new_socket(Socket_val(wh)));
-+}
- #endif
- 
- static gboolean ml_g_io_channel_watch(GIOChannel *s, GIOCondition c,
diff --git a/dev/build/windows/patches_coq/ln.c b/dev/build/windows/patches_coq/ln.c
deleted file mode 100644
index 41f64f98b2..0000000000
--- a/dev/build/windows/patches_coq/ln.c
+++ /dev/null
@@ -1,137 +0,0 @@
-// (C) 2016 Intel Deutschland GmbH
-// Author: Michael Soegtrop
-// Released to the public under CC0
-// See https://creativecommons.org/publicdomain/zero/1.0/
-
-// Windows drop in repacement for Linux ln
-// Supports command form "ln TARGET LINK_NAME"
-// Supports -s and -f options
-// Does not support hard links to folders (but symlinks are ok)
-
-#include <windows.h>
-#include <stdio.h>
-#include <tchar.h>
-
-// Cygwin MinGW doesn't have this Vista++ function in windows.h
-#ifdef UNICODE
-    WINBASEAPI BOOLEAN APIENTRY CreateSymbolicLinkW ( LPCWSTR, LPCWSTR, DWORD );
-    #define CreateSymbolicLink  CreateSymbolicLinkW
-    #define CommandLineToArgv CommandLineToArgvW
-#else
-    WINBASEAPI BOOLEAN APIENTRY CreateSymbolicLinkA ( LPCSTR, LPCSTR, DWORD );
-    #define CreateSymbolicLink  CreateSymbolicLinkA
-    #define CommandLineToArgv CommandLineToArgvA
-#endif
-#define SYMBOLIC_LINK_FLAG_DIRECTORY 1
-
-int WINAPI WinMain( HINSTANCE hInstance, HINSTANCE hPrevInstance, LPSTR lpCmdLineA, int nShowCmd )
-{
-    int iarg;
-    BOOL symbolic = FALSE;
-    BOOL force = FALSE;
-    BOOL folder;
-    const _TCHAR *target;
-    const _TCHAR *link;
-    LPTSTR lpCmdLine; 
-    int argc;
-    LPTSTR *argv;
-
-    // Parse command line
-    // This is done explicitly here for two reasons
-    // 1.) MinGW doesn't seem to support _tmain, wWinMain and the like
-    // 2.) We want to make sure that CommandLineToArgv is used
-    lpCmdLine = GetCommandLine();
-    argv = CommandLineToArgv( lpCmdLine, &argc );
-    
-    // Get target and link name
-    if( argc<3 )
-    {
-        _ftprintf( stderr, _T("Expecting at least 2 arguments, got %d\n"), argc-1 );
-        return 1;
-    }
-    target = argv[argc-2];
-    link = argv[argc-1];
-
-    // Parse options
-    // The last two arguments are interpreted as file names
-    // All other arguments must be -s or -f os multi letter options like -sf
-    for(iarg=1; iarg<argc-2; iarg++ )
-    {
-        const _TCHAR *pos = argv[iarg]; 
-        if( *pos != _T('-') )
-        {
-            _ftprintf( stderr, _T("Command line option expected in argument %d\n"), iarg );
-            return 1;
-        }
-        pos ++;
-
-        while( *pos )
-        {
-            switch( *pos )
-            {
-                case _T('s') : symbolic = TRUE; break;
-                case _T('f') : force = TRUE; break;
-                default : 
-                    _ftprintf( stderr, _T("Unknown option '%c'\n"), *pos );
-                    return 1;
-            }
-            pos ++;
-        }
-    }
-    
-    #ifdef IGNORE_SYMBOLIC
-        symbolic = FALSE;
-    #endif
-    
-    // Check if link already exists - delete it if force is given or abort
-    {
-        if( GetFileAttributes(link) != INVALID_FILE_ATTRIBUTES )
-        {
-            if( force )
-            {
-                if( !DeleteFile( link ) )
-                {
-                    _ftprintf( stderr, _T("Error deleting file '%s'\n"), link );
-                    return 1;
-                }
-            }
-            else
-            {
-                _ftprintf( stderr, _T("File '%s' exists!\n"), link );
-                return 1;
-            }
-        }
-    }
-    
-    // Check if target is a folder
-    folder = ( (GetFileAttributes(target) & FILE_ATTRIBUTE_DIRECTORY) ) != 0;
-    
-    // Create link
-    if(symbolic)
-    {
-        if( !CreateSymbolicLink( link, target, folder ? SYMBOLIC_LINK_FLAG_DIRECTORY : 0 ) )
-        {
-            _ftprintf( stderr, _T("Error creating symbolic link '%s' -> '%s'!\n"), link, target );
-            return 1;
-        }
-    }
-    else
-    {
-        if( folder )
-        {
-            _ftprintf( stderr, _T("Cannot create hard link to folder") );
-            return 1;
-        }
-        else
-        {
-            if( !CreateHardLink( link, target, NULL ) )
-            {
-                _ftprintf( stderr, _T("Error creating hard link '%s' -> '%s'!\n"), link, target );
-                return 1;
-            }
-        }
-    }
-    
-    // Everything is fine
-    return 0;
-}
diff --git a/dev/build/windows/patches_coq/ocaml-4.07.1.patch b/dev/build/windows/patches_coq/ocaml-4.07.1.patch
deleted file mode 100644
index 2d61b5b838..0000000000
--- a/dev/build/windows/patches_coq/ocaml-4.07.1.patch
+++ /dev/null
@@ -1,97 +0,0 @@
-diff/patch file created on Tue, Jun 11, 2019 10:15:38 AM with:
-difftar-folder.sh tarballs/ocaml-4.07.1.tar.gz ocaml-4.07.1 1
-TARFILE= tarballs/ocaml-4.07.1.tar.gz
-FOLDER= ocaml-4.07.1/
-TARSTRIP= 1
-TARPREFIX= ocaml-4.07.1/
-ORIGFOLDER= ocaml-4.07.1.orig
---- ocaml-4.07.1.orig/byterun/caml/osdeps.h	2018-10-04 15:38:56.000000000 +0200
-+++ ocaml-4.07.1/byterun/caml/osdeps.h	2019-06-11 10:13:50.766997600 +0200
-@@ -98,6 +98,11 @@
- */
- extern char_os *caml_secure_getenv(char_os const *var);
-
-+/* Modify or delete environment variable.
-+   Returns 0 on success or an error code.
-+*/
-+extern int caml_putenv(char_os const *var, char_os const *value);
-+
- /* If [fd] refers to a terminal or console, return the number of rows
-    (lines) that it displays.  Otherwise, or if the number of rows
-    cannot be determined, return -1. */
---- ocaml-4.07.1.orig/byterun/debugger.c	2018-10-04 15:38:56.000000000 +0200
-+++ ocaml-4.07.1/byterun/debugger.c	2019-06-11 10:14:02.706013700 +0200
-@@ -180,6 +180,7 @@
-   if (address == NULL) return;
-   if (dbg_addr != NULL) caml_stat_free(dbg_addr);
-   dbg_addr = address;
-+  caml_putenv(_T("CAML_DEBUG_SOCKET"),_T(""));
-
- #ifdef _WIN32
-   winsock_startup();
---- ocaml-4.07.1.orig/byterun/unix.c	2018-10-04 15:38:56.000000000 +0200
-+++ ocaml-4.07.1/byterun/unix.c	2019-06-11 10:14:11.252438800 +0200
-@@ -430,6 +430,19 @@
- #endif
- }
-
-+int caml_putenv(char_os const *var, char_os const *value)
-+{
-+  char_os * s;
-+  int ret;
-+
-+  s = caml_stat_strconcat_os(3, var, _T("="), value);
-+  ret = putenv_os(s);
-+  if (ret == -1) {
-+    caml_stat_free(s);
-+  }
-+  return ret;
-+}
-+
- int caml_num_rows_fd(int fd)
- {
- #ifdef TIOCGWINSZ
---- ocaml-4.07.1.orig/byterun/win32.c	2018-10-04 15:38:56.000000000 +0200
-+++ ocaml-4.07.1/byterun/win32.c	2019-06-11 10:14:19.485640700 +0200
-@@ -727,6 +727,19 @@
-   return _wgetenv(var);
- }
-
-+int caml_putenv(char_os const *var, char_os const *value)
-+{
-+  char_os * s;
-+  int ret;
-+
-+  s = caml_stat_strconcat_os(3, var, _T("="), value);
-+  ret = putenv_os(s);
-+  if (ret == -1) {
-+    caml_stat_free(s);
-+  }
-+  return ret;
-+}
-+
- /* caml_win32_getenv is used to implement Sys.getenv and Unix.getenv in such a
-    way that they get direct access to the Win32 environment rather than to the
-    copy that is cached by the C runtime system. The result of caml_win32_getenv
---- ocaml-4.07.1.orig/config/Makefile.mingw	2018-10-04 15:38:56.000000000 +0200
-+++ ocaml-4.07.1//config/Makefile.mingw	2019-06-11 10:14:44.492969800 +0200
-@@ -89,7 +89,7 @@
- NATDYNLINK=true
- NATDYNLINKOPTS=
- CMXS=cmxs
--RUNTIMED=false
-+RUNTIMED=true
- ASM_CFI_SUPPORTED=false
- WITH_FRAME_POINTERS=false
- UNIX_OR_WIN32=win32
---- ocaml-4.07.1.orig/config/Makefile.mingw64	2018-10-04 15:38:56.000000000 +0200
-+++ ocaml-4.07.1//config/Makefile.mingw64	2019-06-11 10:14:53.664784900 +0200
-@@ -89,7 +89,7 @@
- NATDYNLINK=true
- NATDYNLINKOPTS=
- CMXS=cmxs
--RUNTIMED=false
-+RUNTIMED=true
- ASM_CFI_SUPPORTED=false
- WITH_FRAME_POINTERS=false
- UNIX_OR_WIN32=win32
diff --git a/dev/build/windows/patches_coq/ocaml-4.08.1.patch b/dev/build/windows/patches_coq/ocaml-4.08.1.patch
deleted file mode 100644
index a79033a061..0000000000
--- a/dev/build/windows/patches_coq/ocaml-4.08.1.patch
+++ /dev/null
@@ -1,25 +0,0 @@
-diff --git a/runtime/caml/misc.h b/runtime/caml/misc.h
-index 6aa98516b..8184c2797 100644
---- a/runtime/caml/misc.h
-+++ b/runtime/caml/misc.h
-@@ -327,7 +327,6 @@ extern void caml_set_fields (intnat v, uintnat, uintnat);
- 
- #if defined(_WIN32) && !defined(_UCRT)
- extern int caml_snprintf(char * buf, size_t size, const char * format, ...);
--#define snprintf caml_snprintf
- #endif
- 
- #ifdef CAML_INSTR
-@@ -336,6 +335,12 @@ extern int caml_snprintf(char * buf, size_t size, const char * format, ...);
- #include <time.h>
- #include <stdio.h>
- 
-+/* snprintf emulation for Win32 - do define after stdio.h, in case snprintf is defined */
-+
-+#if defined(_WIN32) && !defined(_UCRT)
-+#define snprintf caml_snprintf
-+#endif
-+
- extern intnat caml_stat_minor_collections;
- extern intnat caml_instr_starttime, caml_instr_stoptime;
- 
diff --git a/dev/build/windows/patches_coq/pkg-config.c b/dev/build/windows/patches_coq/pkg-config.c
deleted file mode 100644
index c4c7ec2bff..0000000000
--- a/dev/build/windows/patches_coq/pkg-config.c
+++ /dev/null
@@ -1,29 +0,0 @@
-// MinGW personality wrapper for pkgconf
-// This is an executable replacement for the shell scripts /bin/ARCH-pkg-config
-// Compile with e.g.
-// gcc pkg-config.c -DARCH=x86_64-w64-mingw32 -o pkg-config.exe
-// gcc pkg-config.c -DARCH=i686-w64-mingw32 -o pkg-config.exe
-// ATTENTION: Do not compile with MinGW-gcc, compile with cygwin gcc!
-//
-// To test it execute e.g.
-// $ ./pkg-config --path zlib
-// /usr/x86_64-w64-mingw32/sys-root/mingw/lib/pkgconfig/zlib.pc
-
-#include <unistd.h>
-
-#define STRINGIFY1(arg) #arg
-#define STRINGIFY(arg) STRINGIFY1(arg)
-
-int main(int argc, char *argv[])
-{
-    // +1 for extra argument, +1 for trailing NULL
-    char * argvnew[argc+2];
-    int id=0, is=0;
-
-    argvnew[id++] = argv[is++];
-    argvnew[id++] = "--personality="STRINGIFY(ARCH);
-    while( is<argc ) argvnew[id++] = argv[is++];
-    argvnew[id++] = 0;
-
-    return execv("/usr/bin/pkgconf", argvnew);
-}
diff --git a/dev/build/windows/patches_coq/quickchick.patch b/dev/build/windows/patches_coq/quickchick.patch
deleted file mode 100644
index 4b7b86ff05..0000000000
--- a/dev/build/windows/patches_coq/quickchick.patch
+++ /dev/null
@@ -1,47 +0,0 @@
-diff/patch file created on Wed, Jul 17, 2019  8:06:45 PM with:
-difftar-folder.sh tarballs/quickchick-741fb98eb865129a70c4ef7a64db2739c4a5eab0.tar.gz quickchick-741fb98eb865129a70c4ef7a64db2739c4a5eab0 1
-TARFILE= tarballs/quickchick-741fb98eb865129a70c4ef7a64db2739c4a5eab0.tar.gz
-FOLDER= quickchick-741fb98eb865129a70c4ef7a64db2739c4a5eab0
-TARSTRIP= 1
-TARPREFIX= QuickChick-741fb98eb865129a70c4ef7a64db2739c4a5eab0/
-ORIGFOLDER= quickchick-741fb98eb865129a70c4ef7a64db2739c4a5eab0.orig
---- quickchick-741fb98eb865129a70c4ef7a64db2739c4a5eab0.orig/Makefile	2019-06-26 12:09:01.000000000 +0200
-+++ quickchick-741fb98eb865129a70c4ef7a64db2739c4a5eab0/Makefile	2019-07-17 20:05:44.322251200 +0200
-@@ -2,7 +2,7 @@
- .PHONY: plugin install install-plugin clean quickChickTool
- 
- QCTOOL_DIR=quickChickTool
--QCTOOL_EXE=quickChickTool.byte
-+QCTOOL_EXE=quickChickTool.native
- QCTOOL_SRC=$(QCTOOL_DIR)/quickChickTool.ml \
- 		   $(QCTOOL_DIR)/quickChickToolTypes.ml \
- 		   $(QCTOOL_DIR)/quickChickToolLexer.mll \
-@@ -20,8 +20,8 @@
- 
- all: quickChickTool plugin documentation-check
- 
--plugin: Makefile.coq 
--	$(MAKE) -f Makefile.coq 
-+plugin: Makefile.coq
-+	$(MAKE) -f Makefile.coq
- 
- documentation-check: plugin
- 	coqc -R src QuickChick -I src QuickChickInterface.v
-@@ -32,7 +32,7 @@
- install: all
- 	$(V)$(MAKE) -f Makefile.coq install > $(TEMPFILE)
- # Manually copying the remaining files
--	$(V)cp $(QCTOOL_DIR)/$(QCTOOL_EXE) $(shell opam config var bin)/quickChick
-+	$(V)cp $(QCTOOL_DIR)/$(QCTOOL_EXE) "$(COQBIN)/quickChick"
- #	 $(V)cp src/quickChickLib.cmx $(COQLIB)/user-contrib/QuickChick
- #	 $(V)cp src/quickChickLib.o $(COQLIB)/user-contrib/QuickChick
- 
-@@ -56,7 +56,7 @@
- 	$(MAKE) -C examples/RedBlack test
- #	cd examples/stlc; make clean && make
- 	$(MAKE) -C examples/multifile-mutation test
--# This takes too long. 
-+# This takes too long.
- #	$(MAKE) -C examples/c-mutation test
- #	coqc examples/BSTTest.v
- 	coqc examples/DependentTest.v
diff --git a/dev/build/windows/patches_coq/sed-4.2.2-3.src.patch b/dev/build/windows/patches_coq/sed-4.2.2-3.src.patch
deleted file mode 100644
index d210a04153..0000000000
--- a/dev/build/windows/patches_coq/sed-4.2.2-3.src.patch
+++ /dev/null
@@ -1,1301 +0,0 @@
---- origsrc/sed-4.2.2/doc/sed.1	2012-12-22 15:27:13.000000000 +0100
-+++ src/sed-4.2.2/doc/sed.1	2013-06-27 18:10:47.974060492 +0200
-@@ -1,5 +1,5 @@
- .\" DO NOT MODIFY THIS FILE!  It was generated by help2man 1.28.
--.TH SED "1" "December 2012" "sed 4.2.2" "User Commands"
-+.TH SED "1" "June 2013" "sed 4.2.2" "User Commands"
- .SH NAME
- sed \- stream editor for filtering and transforming text
- .SH SYNOPSIS
-@@ -40,6 +40,10 @@ follow symlinks when processing in place
- .IP
- edit files in place (makes backup if SUFFIX supplied)
- .HP
-+\fB\-b\fR, \fB\-\-binary\fR
-+.IP
-+open files in binary mode (CR+LFs are not processed specially)
-+.HP
- \fB\-l\fR N, \fB\-\-line\-length\fR=\fIN\fR
- .IP
- specify the desired line-wrap length for the `l' command
---- origsrc/sed-4.2.2/lib/regcomp.c	2012-12-22 14:21:52.000000000 +0100
-+++ src/sed-4.2.2/lib/regcomp.c	2013-06-27 18:05:27.044448044 +0200
-@@ -1,22 +1,21 @@
--/* -*- buffer-read-only: t -*- vi: set ro: */
--/* DO NOT EDIT! GENERATED AUTOMATICALLY! */
- /* Extended regular expression matching and search library.
--   Copyright (C) 2002-2012 Free Software Foundation, Inc.
-+   Copyright (C) 2002-2013 Free Software Foundation, Inc.
-    This file is part of the GNU C Library.
-    Contributed by Isamu Hasegawa <isamu@yamato.ibm.com>.
- 
--   This program is free software; you can redistribute it and/or modify
--   it under the terms of the GNU General Public License as published by
--   the Free Software Foundation; either version 3, or (at your option)
--   any later version.
-+   The GNU C Library is free software; you can redistribute it and/or
-+   modify it under the terms of the GNU Lesser General Public
-+   License as published by the Free Software Foundation; either
-+   version 2.1 of the License, or (at your option) any later version.
- 
--   This program is distributed in the hope that it will be useful,
-+   The GNU C Library is distributed in the hope that it will be useful,
-    but WITHOUT ANY WARRANTY; without even the implied warranty of
--   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
--   GNU General Public License for more details.
-+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
-+   Lesser General Public License for more details.
- 
--   You should have received a copy of the GNU General Public License along
--   with this program; if not, see <http://www.gnu.org/licenses/>.  */
-+   You should have received a copy of the GNU Lesser General Public
-+   License along with the GNU C Library; if not, see
-+   <http://www.gnu.org/licenses/>.  */
- 
- static reg_errcode_t re_compile_internal (regex_t *preg, const char * pattern,
- 					  size_t length, reg_syntax_t syntax);
-@@ -95,20 +94,20 @@ static reg_errcode_t build_charclass (RE
- 				      bitset_t sbcset,
- 				      re_charset_t *mbcset,
- 				      Idx *char_class_alloc,
--				      const unsigned char *class_name,
-+				      const char *class_name,
- 				      reg_syntax_t syntax);
- #else  /* not RE_ENABLE_I18N */
- static reg_errcode_t build_equiv_class (bitset_t sbcset,
- 					const unsigned char *name);
- static reg_errcode_t build_charclass (RE_TRANSLATE_TYPE trans,
- 				      bitset_t sbcset,
--				      const unsigned char *class_name,
-+				      const char *class_name,
- 				      reg_syntax_t syntax);
- #endif /* not RE_ENABLE_I18N */
- static bin_tree_t *build_charclass_op (re_dfa_t *dfa,
- 				       RE_TRANSLATE_TYPE trans,
--				       const unsigned char *class_name,
--				       const unsigned char *extra,
-+				       const char *class_name,
-+				       const char *extra,
- 				       bool non_match, reg_errcode_t *err);
- static bin_tree_t *create_tree (re_dfa_t *dfa,
- 				bin_tree_t *left, bin_tree_t *right,
-@@ -293,7 +292,7 @@ weak_alias (__re_compile_fastmap, re_com
- #endif
- 
- static inline void
--__attribute ((always_inline))
-+__attribute__ ((always_inline))
- re_set_fastmap (char *fastmap, bool icase, int ch)
- {
-   fastmap[ch] = 1;
-@@ -587,7 +586,7 @@ weak_alias (__regerror, regerror)
- static const bitset_t utf8_sb_map =
- {
-   /* Set the first 128 bits.  */
--# ifdef __GNUC__
-+# if defined __GNUC__ && !defined __STRICT_ANSI__
-   [0 ... 0x80 / BITSET_WORD_BITS - 1] = BITSET_WORD_MAX
- # else
- #  if 4 * BITSET_WORD_BITS < ASCII_CHARS
-@@ -664,7 +663,10 @@ regfree (preg)
- {
-   re_dfa_t *dfa = preg->buffer;
-   if (BE (dfa != NULL, 1))
--    free_dfa_content (dfa);
-+    {
-+      lock_fini (dfa->lock);
-+      free_dfa_content (dfa);
-+    }
-   preg->buffer = NULL;
-   preg->allocated = 0;
- 
-@@ -785,6 +787,8 @@ re_compile_internal (regex_t *preg, cons
-   preg->used = sizeof (re_dfa_t);
- 
-   err = init_dfa (dfa, length);
-+  if (BE (err == REG_NOERROR && lock_init (dfa->lock) != 0, 0))
-+    err = REG_ESPACE;
-   if (BE (err != REG_NOERROR, 0))
-     {
-       free_dfa_content (dfa);
-@@ -798,8 +802,6 @@ re_compile_internal (regex_t *preg, cons
-   strncpy (dfa->re_str, pattern, length + 1);
- #endif
- 
--  __libc_lock_init (dfa->lock);
--
-   err = re_string_construct (&regexp, pattern, length, preg->translate,
- 			     (syntax & RE_ICASE) != 0, dfa);
-   if (BE (err != REG_NOERROR, 0))
-@@ -807,6 +809,7 @@ re_compile_internal (regex_t *preg, cons
-     re_compile_internal_free_return:
-       free_workarea_compile (preg);
-       re_string_destruct (&regexp);
-+      lock_fini (dfa->lock);
-       free_dfa_content (dfa);
-       preg->buffer = NULL;
-       preg->allocated = 0;
-@@ -839,6 +842,7 @@ re_compile_internal (regex_t *preg, cons
- 
-   if (BE (err != REG_NOERROR, 0))
-     {
-+      lock_fini (dfa->lock);
-       free_dfa_content (dfa);
-       preg->buffer = NULL;
-       preg->allocated = 0;
-@@ -954,10 +958,10 @@ static void
- internal_function
- init_word_char (re_dfa_t *dfa)
- {
--  dfa->word_ops_used = 1;
-   int i = 0;
-   int j;
-   int ch = 0;
-+  dfa->word_ops_used = 1;
-   if (BE (dfa->map_notascii == 0, 1))
-     {
-       bitset_word_t bits0 = 0x00000000;
-@@ -2423,8 +2427,8 @@ parse_expression (re_string_t *regexp, r
-     case OP_WORD:
-     case OP_NOTWORD:
-       tree = build_charclass_op (dfa, regexp->trans,
--				 (const unsigned char *) "alnum",
--				 (const unsigned char *) "_",
-+				 "alnum",
-+				 "_",
- 				 token->type == OP_NOTWORD, err);
-       if (BE (*err != REG_NOERROR && tree == NULL, 0))
- 	return NULL;
-@@ -2432,8 +2436,8 @@ parse_expression (re_string_t *regexp, r
-     case OP_SPACE:
-     case OP_NOTSPACE:
-       tree = build_charclass_op (dfa, regexp->trans,
--				 (const unsigned char *) "space",
--				 (const unsigned char *) "",
-+				 "space",
-+				 "",
- 				 token->type == OP_NOTSPACE, err);
-       if (BE (*err != REG_NOERROR && tree == NULL, 0))
- 	return NULL;
-@@ -2713,7 +2717,6 @@ build_range_exp (const reg_syntax_t synt
-     wchar_t wc;
-     wint_t start_wc;
-     wint_t end_wc;
--    wchar_t cmp_buf[6] = {L'\0', L'\0', L'\0', L'\0', L'\0', L'\0'};
- 
-     start_ch = ((start_elem->type == SB_CHAR) ? start_elem->opr.ch
- 		: ((start_elem->type == COLL_SYM) ? start_elem->opr.name[0]
-@@ -2727,11 +2730,7 @@ build_range_exp (const reg_syntax_t synt
- 	      ? __btowc (end_ch) : end_elem->opr.wch);
-     if (start_wc == WEOF || end_wc == WEOF)
-       return REG_ECOLLATE;
--    cmp_buf[0] = start_wc;
--    cmp_buf[4] = end_wc;
--
--    if (BE ((syntax & RE_NO_EMPTY_RANGES)
--            && wcscoll (cmp_buf, cmp_buf + 4) > 0, 0))
-+    else if (BE ((syntax & RE_NO_EMPTY_RANGES) && start_wc > end_wc, 0))
-       return REG_ERANGE;
- 
-     /* Got valid collation sequence values, add them as a new entry.
-@@ -2772,9 +2771,7 @@ build_range_exp (const reg_syntax_t synt
-     /* Build the table for single byte characters.  */
-     for (wc = 0; wc < SBC_MAX; ++wc)
-       {
--	cmp_buf[2] = wc;
--	if (wcscoll (cmp_buf, cmp_buf + 2) <= 0
--	    && wcscoll (cmp_buf + 2, cmp_buf + 4) <= 0)
-+	if (start_wc <= wc && wc <= end_wc)
- 	  bitset_set (sbcset, wc);
-       }
-   }
-@@ -2843,40 +2840,29 @@ parse_bracket_exp (re_string_t *regexp,
- 
-   /* Local function for parse_bracket_exp used in _LIBC environment.
-      Seek the collating symbol entry corresponding to NAME.
--     Return the index of the symbol in the SYMB_TABLE.  */
-+     Return the index of the symbol in the SYMB_TABLE,
-+     or -1 if not found.  */
- 
-   auto inline int32_t
--  __attribute ((always_inline))
--  seek_collating_symbol_entry (name, name_len)
--	 const unsigned char *name;
--	 size_t name_len;
--    {
--      int32_t hash = elem_hash ((const char *) name, name_len);
--      int32_t elem = hash % table_size;
--      if (symb_table[2 * elem] != 0)
--	{
--	  int32_t second = hash % (table_size - 2) + 1;
--
--	  do
--	    {
--	      /* First compare the hashing value.  */
--	      if (symb_table[2 * elem] == hash
--		  /* Compare the length of the name.  */
--		  && name_len == extra[symb_table[2 * elem + 1]]
--		  /* Compare the name.  */
--		  && memcmp (name, &extra[symb_table[2 * elem + 1] + 1],
--			     name_len) == 0)
--		{
--		  /* Yep, this is the entry.  */
--		  break;
--		}
-+  __attribute__ ((always_inline))
-+  seek_collating_symbol_entry (const unsigned char *name, size_t name_len)
-+    {
-+      int32_t elem;
- 
--	      /* Next entry.  */
--	      elem += second;
--	    }
--	  while (symb_table[2 * elem] != 0);
--	}
--      return elem;
-+      for (elem = 0; elem < table_size; elem++)
-+	if (symb_table[2 * elem] != 0)
-+	  {
-+	    int32_t idx = symb_table[2 * elem + 1];
-+	    /* Skip the name of collating element name.  */
-+	    idx += 1 + extra[idx];
-+	    if (/* Compare the length of the name.  */
-+		name_len == extra[idx]
-+		/* Compare the name.  */
-+		&& memcmp (name, &extra[idx + 1], name_len) == 0)
-+	      /* Yep, this is the entry.  */
-+	      return elem;
-+	  }
-+      return -1;
-     }
- 
-   /* Local function for parse_bracket_exp used in _LIBC environment.
-@@ -2884,9 +2870,8 @@ parse_bracket_exp (re_string_t *regexp,
-      Return the value if succeeded, UINT_MAX otherwise.  */
- 
-   auto inline unsigned int
--  __attribute ((always_inline))
--  lookup_collation_sequence_value (br_elem)
--	 bracket_elem_t *br_elem;
-+  __attribute__ ((always_inline))
-+  lookup_collation_sequence_value (bracket_elem_t *br_elem)
-     {
-       if (br_elem->type == SB_CHAR)
- 	{
-@@ -2914,7 +2899,7 @@ parse_bracket_exp (re_string_t *regexp,
- 	      int32_t elem, idx;
- 	      elem = seek_collating_symbol_entry (br_elem->opr.name,
- 						  sym_name_len);
--	      if (symb_table[2 * elem] != 0)
-+	      if (elem != -1)
- 		{
- 		  /* We found the entry.  */
- 		  idx = symb_table[2 * elem + 1];
-@@ -2932,7 +2917,7 @@ parse_bracket_exp (re_string_t *regexp,
- 		  /* Return the collation sequence value.  */
- 		  return *(unsigned int *) (extra + idx);
- 		}
--	      else if (symb_table[2 * elem] == 0 && sym_name_len == 1)
-+	      else if (sym_name_len == 1)
- 		{
- 		  /* No valid character.  Match it as a single byte
- 		     character.  */
-@@ -2953,12 +2938,9 @@ parse_bracket_exp (re_string_t *regexp,
-      update it.  */
- 
-   auto inline reg_errcode_t
--  __attribute ((always_inline))
--  build_range_exp (sbcset, mbcset, range_alloc, start_elem, end_elem)
--	 re_charset_t *mbcset;
--	 Idx *range_alloc;
--	 bitset_t sbcset;
--	 bracket_elem_t *start_elem, *end_elem;
-+  __attribute__ ((always_inline))
-+  build_range_exp (bitset_t sbcset, re_charset_t *mbcset, int *range_alloc,
-+		   bracket_elem_t *start_elem, bracket_elem_t *end_elem)
-     {
-       unsigned int ch;
-       uint32_t start_collseq;
-@@ -2971,6 +2953,7 @@ parse_bracket_exp (re_string_t *regexp,
- 	      0))
- 	return REG_ERANGE;
- 
-+      /* FIXME: Implement rational ranges here, too.  */
-       start_collseq = lookup_collation_sequence_value (start_elem);
-       end_collseq = lookup_collation_sequence_value (end_elem);
-       /* Check start/end collation sequence values.  */
-@@ -3036,26 +3019,23 @@ parse_bracket_exp (re_string_t *regexp,
-      pointer argument since we may update it.  */
- 
-   auto inline reg_errcode_t
--  __attribute ((always_inline))
--  build_collating_symbol (sbcset, mbcset, coll_sym_alloc, name)
--	 re_charset_t *mbcset;
--	 Idx *coll_sym_alloc;
--	 bitset_t sbcset;
--	 const unsigned char *name;
-+  __attribute__ ((always_inline))
-+  build_collating_symbol (bitset_t sbcset, re_charset_t *mbcset,
-+			  Idx *coll_sym_alloc, const unsigned char *name)
-     {
-       int32_t elem, idx;
-       size_t name_len = strlen ((const char *) name);
-       if (nrules != 0)
- 	{
- 	  elem = seek_collating_symbol_entry (name, name_len);
--	  if (symb_table[2 * elem] != 0)
-+	  if (elem != -1)
- 	    {
- 	      /* We found the entry.  */
- 	      idx = symb_table[2 * elem + 1];
- 	      /* Skip the name of collating element name.  */
- 	      idx += 1 + extra[idx];
- 	    }
--	  else if (symb_table[2 * elem] == 0 && name_len == 1)
-+	  else if (name_len == 1)
- 	    {
- 	      /* No valid character, treat it as a normal
- 		 character.  */
-@@ -3298,7 +3278,8 @@ parse_bracket_exp (re_string_t *regexp,
- #ifdef RE_ENABLE_I18N
- 				      mbcset, &char_class_alloc,
- #endif /* RE_ENABLE_I18N */
--				      start_elem.opr.name, syntax);
-+				      (const char *) start_elem.opr.name,
-+				      syntax);
- 	      if (BE (*err != REG_NOERROR, 0))
- 	       goto parse_bracket_exp_free_return;
- 	      break;
-@@ -3578,14 +3559,14 @@ static reg_errcode_t
- #ifdef RE_ENABLE_I18N
- build_charclass (RE_TRANSLATE_TYPE trans, bitset_t sbcset,
- 		 re_charset_t *mbcset, Idx *char_class_alloc,
--		 const unsigned char *class_name, reg_syntax_t syntax)
-+		 const char *class_name, reg_syntax_t syntax)
- #else /* not RE_ENABLE_I18N */
- build_charclass (RE_TRANSLATE_TYPE trans, bitset_t sbcset,
--		 const unsigned char *class_name, reg_syntax_t syntax)
-+		 const char *class_name, reg_syntax_t syntax)
- #endif /* not RE_ENABLE_I18N */
- {
-   int i;
--  const char *name = (const char *) class_name;
-+  const char *name = class_name;
- 
-   /* In case of REG_ICASE "upper" and "lower" match the both of
-      upper and lower cases.  */
-@@ -3659,8 +3640,8 @@ build_charclass (RE_TRANSLATE_TYPE trans
- 
- static bin_tree_t *
- build_charclass_op (re_dfa_t *dfa, RE_TRANSLATE_TYPE trans,
--		    const unsigned char *class_name,
--		    const unsigned char *extra, bool non_match,
-+		    const char *class_name,
-+		    const char *extra, bool non_match,
- 		    reg_errcode_t *err)
- {
-   re_bitset_ptr_t sbcset;
---- origsrc/sed-4.2.2/lib/regex-quote.c	1970-01-01 01:00:00.000000000 +0100
-+++ src/sed-4.2.2/lib/regex-quote.c	2013-06-27 18:05:27.081447884 +0200
-@@ -0,0 +1,216 @@
-+/* Construct a regular expression from a literal string.
-+   Copyright (C) 1995, 2010-2013 Free Software Foundation, Inc.
-+   Written by Bruno Haible <haible@clisp.cons.org>, 2010.
-+
-+   This program is free software: you can redistribute it and/or modify
-+   it under the terms of the GNU General Public License as published by
-+   the Free Software Foundation; either version 3 of the License, or
-+   (at your option) any later version.
-+
-+   This program is distributed in the hope that it will be useful,
-+   but WITHOUT ANY WARRANTY; without even the implied warranty of
-+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-+   GNU General Public License for more details.
-+
-+   You should have received a copy of the GNU General Public License
-+   along with this program.  If not, see <http://www.gnu.org/licenses/>.  */
-+
-+#include <config.h>
-+
-+/* Specification.  */
-+#include "regex-quote.h"
-+
-+#include <string.h>
-+
-+#include "mbuiter.h"
-+#include "xalloc.h"
-+
-+/* Characters that are special in a BRE.  */
-+static const char bre_special[] = "$^.*[]\\";
-+
-+/* Characters that are special in an ERE.  */
-+static const char ere_special[] = "$^.*[]\\+?{}()|";
-+
-+struct regex_quote_spec
-+regex_quote_spec_posix (int cflags, bool anchored)
-+{
-+  struct regex_quote_spec result;
-+
-+  strcpy (result.special, cflags != 0 ? ere_special : bre_special);
-+  result.multibyte = true;
-+  result.anchored = anchored;
-+
-+  return result;
-+}
-+
-+/* Syntax bit values, defined in GNU <regex.h>.  We don't include it here,
-+   otherwise this module would need to depend on gnulib module 'regex'.  */
-+#define RE_BK_PLUS_QM    0x00000002
-+#define RE_INTERVALS     0x00000200
-+#define RE_LIMITED_OPS   0x00000400
-+#define RE_NEWLINE_ALT   0x00000800
-+#define RE_NO_BK_BRACES  0x00001000
-+#define RE_NO_BK_PARENS  0x00002000
-+#define RE_NO_BK_VBAR    0x00008000
-+
-+struct regex_quote_spec
-+regex_quote_spec_gnu (unsigned long /*reg_syntax_t*/ syntax, bool anchored)
-+{
-+  struct regex_quote_spec result;
-+  char *p;
-+
-+  p = result.special;
-+  memcpy (p, bre_special, sizeof (bre_special) - 1);
-+  p += sizeof (bre_special) - 1;
-+  if ((syntax & RE_LIMITED_OPS) == 0 && (syntax & RE_BK_PLUS_QM) == 0)
-+    {
-+      *p++ = '+';
-+      *p++ = '?';
-+    }
-+  if ((syntax & RE_INTERVALS) != 0 && (syntax & RE_NO_BK_BRACES) != 0)
-+    {
-+      *p++ = '{';
-+      *p++ = '}';
-+    }
-+  if ((syntax & RE_NO_BK_PARENS) != 0)
-+    {
-+      *p++ = '(';
-+      *p++ = ')';
-+    }
-+  if ((syntax & RE_LIMITED_OPS) == 0 && (syntax & RE_NO_BK_VBAR) != 0)
-+    *p++ = '|';
-+  if ((syntax & RE_NEWLINE_ALT) != 0)
-+    *p++ = '\n';
-+  *p = '\0';
-+
-+  result.multibyte = true;
-+  result.anchored = anchored;
-+
-+  return result;
-+}
-+
-+/* Characters that are special in a PCRE.  */
-+static const char pcre_special[] = "$^.*[]\\+?{}()|";
-+
-+/* Options bit values, defined in <pcre.h>.  We don't include it here, because
-+   it is not a standard header.  */
-+#define PCRE_ANCHORED 0x00000010
-+#define PCRE_EXTENDED 0x00000008
-+
-+struct regex_quote_spec
-+regex_quote_spec_pcre (int options, bool anchored)
-+{
-+  struct regex_quote_spec result;
-+  char *p;
-+
-+  p = result.special;
-+  memcpy (p, bre_special, sizeof (pcre_special) - 1);
-+  p += sizeof (pcre_special) - 1;
-+  if (options & PCRE_EXTENDED)
-+    {
-+      *p++ = ' ';
-+      *p++ = '\t';
-+      *p++ = '\n';
-+      *p++ = '\v';
-+      *p++ = '\f';
-+      *p++ = '\r';
-+      *p++ = '#';
-+    }
-+  *p = '\0';
-+
-+  /* PCRE regular expressions consist of UTF-8 characters of options contains
-+     PCRE_UTF8 and of single bytes otherwise.  */
-+  result.multibyte = false;
-+  /* If options contains PCRE_ANCHORED, the anchoring is implicit.  */
-+  result.anchored = (options & PCRE_ANCHORED ? 0 : anchored);
-+
-+  return result;
-+}
-+
-+size_t
-+regex_quote_length (const char *string, const struct regex_quote_spec *spec)
-+{
-+  const char *special = spec->special;
-+  size_t length;
-+
-+  length = 0;
-+  if (spec->anchored)
-+    length += 2; /* for '^' at the beginning and '$' at the end */
-+  if (spec->multibyte)
-+    {
-+      mbui_iterator_t iter;
-+
-+      for (mbui_init (iter, string); mbui_avail (iter); mbui_advance (iter))
-+        {
-+          /* We know that special contains only ASCII characters.  */
-+          if (mb_len (mbui_cur (iter)) == 1
-+              && strchr (special, * mbui_cur_ptr (iter)))
-+            length += 1;
-+          length += mb_len (mbui_cur (iter));
-+        }
-+    }
-+  else
-+    {
-+      const char *iter;
-+
-+      for (iter = string; *iter != '\0'; iter++)
-+        {
-+          if (strchr (special, *iter))
-+            length += 1;
-+          length += 1;
-+        }
-+    }
-+
-+  return length;
-+}
-+
-+char *
-+regex_quote_copy (char *p, const char *string, const struct regex_quote_spec *spec)
-+{
-+  const char *special = spec->special;
-+
-+  if (spec->anchored)
-+    *p++ = '^';
-+  if (spec->multibyte)
-+    {
-+      mbui_iterator_t iter;
-+
-+      for (mbui_init (iter, string); mbui_avail (iter); mbui_advance (iter))
-+        {
-+          /* We know that special contains only ASCII characters.  */
-+          if (mb_len (mbui_cur (iter)) == 1
-+              && strchr (special, * mbui_cur_ptr (iter)))
-+            *p++ = '\\';
-+          memcpy (p, mbui_cur_ptr (iter), mb_len (mbui_cur (iter)));
-+          p += mb_len (mbui_cur (iter));
-+        }
-+    }
-+  else
-+    {
-+      const char *iter;
-+
-+      for (iter = string; *iter != '\0'; iter++)
-+        {
-+          if (strchr (special, *iter))
-+            *p++ = '\\';
-+          *p++ = *iter++;
-+        }
-+    }
-+  if (spec->anchored)
-+    *p++ = '$';
-+
-+  return p;
-+}
-+
-+char *
-+regex_quote (const char *string, const struct regex_quote_spec *spec)
-+{
-+  size_t length = regex_quote_length (string, spec);
-+  char *result = XNMALLOC (length + 1, char);
-+  char *p;
-+
-+  p = result;
-+  p = regex_quote_copy (p, string, spec);
-+  *p = '\0';
-+  return result;
-+}
---- origsrc/sed-4.2.2/lib/regex-quote.h	1970-01-01 01:00:00.000000000 +0100
-+++ src/sed-4.2.2/lib/regex-quote.h	2013-06-27 18:05:27.112447751 +0200
-@@ -0,0 +1,88 @@
-+/* Construct a regular expression from a literal string.
-+   Copyright (C) 1995, 2010-2013 Free Software Foundation, Inc.
-+   Written by Bruno Haible <haible@clisp.cons.org>, 2010.
-+
-+   This program is free software: you can redistribute it and/or modify
-+   it under the terms of the GNU General Public License as published by
-+   the Free Software Foundation; either version 3 of the License, or
-+   (at your option) any later version.
-+
-+   This program is distributed in the hope that it will be useful,
-+   but WITHOUT ANY WARRANTY; without even the implied warranty of
-+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-+   GNU General Public License for more details.
-+
-+   You should have received a copy of the GNU General Public License
-+   along with this program.  If not, see <http://www.gnu.org/licenses/>.  */
-+
-+#ifndef _REGEX_QUOTE_H
-+#define _REGEX_QUOTE_H
-+
-+#include <stddef.h>
-+#include <stdbool.h>
-+
-+
-+/* Specifies a quotation task for converting a fixed string to a regular
-+   expression pattern.  */
-+struct regex_quote_spec
-+{
-+  /* True if the regular expression pattern consists of multibyte characters
-+     (in the encoding given by the LC_CTYPE category of the locale),
-+     false if it consists of single bytes or UTF-8 characters.  */
-+  unsigned int /*bool*/ multibyte : 1;
-+  /* True if the regular expression pattern shall match only entire lines.  */
-+  unsigned int /*bool*/ anchored : 1;
-+  /* Set of characters that need to be escaped (all ASCII), as a
-+     NUL-terminated string.  */
-+  char special[30 + 1];
-+};
-+
-+
-+/* Creates a quotation task that produces a POSIX regular expression, that is,
-+   a pattern that can be compiled with regcomp().
-+   CFLAGS can be 0 or REG_EXTENDED.
-+   If it is 0, the result is a Basic Regular Expression (BRE)
-+   <http://www.opengroup.org/onlinepubs/9699919799/basedefs/V1_chap09.html#tag_09_03>.
-+   If it is REG_EXTENDED, the result is an Extended Regular Expression (ERE)
-+   <http://www.opengroup.org/onlinepubs/9699919799/basedefs/V1_chap09.html#tag_09_04>.
-+   If ANCHORED is false, the regular expression will match substrings of lines.
-+   If ANCHORED is true, it will match only complete lines,  */
-+extern struct regex_quote_spec
-+       regex_quote_spec_posix (int cflags, bool anchored);
-+
-+/* Creates a quotation task that produces a regular expression that can be
-+   compiled with the GNU API function re_compile_pattern().
-+   SYNTAX describes the syntax of the regular expression (such as
-+   RE_SYNTAX_POSIX_BASIC, RE_SYNTAX_POSIX_EXTENDED, RE_SYNTAX_EMACS, all
-+   defined in <regex.h>).  It must be the same value as 're_syntax_options'
-+   at the moment of the re_compile_pattern() call.
-+   If ANCHORED is false, the regular expression will match substrings of lines.
-+   If ANCHORED is true, it will match only complete lines,  */
-+extern struct regex_quote_spec
-+       regex_quote_spec_gnu (unsigned long /*reg_syntax_t*/ syntax, bool anchored);
-+
-+/* Creates a quotation task that produces a PCRE regular expression, that is,
-+   a pattern that can be compiled with pcre_compile().
-+   OPTIONS is the same value as the second argument passed to pcre_compile().
-+   If ANCHORED is false, the regular expression will match substrings of lines.
-+   If ANCHORED is true, it will match only complete lines,  */
-+extern struct regex_quote_spec
-+       regex_quote_spec_pcre (int options, bool anchored);
-+
-+
-+/* Returns the number of bytes needed for the quoted string.  */
-+extern size_t
-+       regex_quote_length (const char *string, const struct regex_quote_spec *spec);
-+
-+/* Copies the quoted string to p and returns the incremented p.
-+   There must be room for regex_quote_length (string, spec) + 1 bytes at p.  */
-+extern char *
-+       regex_quote_copy (char *p,
-+                         const char *string, const struct regex_quote_spec *spec);
-+
-+/* Returns the freshly allocated quoted string.  */
-+extern char *
-+       regex_quote (const char *string, const struct regex_quote_spec *spec);
-+
-+
-+#endif /* _REGEX_QUOTE_H */
---- origsrc/sed-4.2.2/lib/regex.c	2012-12-22 14:21:52.000000000 +0100
-+++ src/sed-4.2.2/lib/regex.c	2013-06-27 18:05:27.138447639 +0200
-@@ -1,22 +1,21 @@
--/* -*- buffer-read-only: t -*- vi: set ro: */
--/* DO NOT EDIT! GENERATED AUTOMATICALLY! */
- /* Extended regular expression matching and search library.
--   Copyright (C) 2002-2003, 2005-2006, 2009-2012 Free Software Foundation, Inc.
-+   Copyright (C) 2002-2013 Free Software Foundation, Inc.
-    This file is part of the GNU C Library.
-    Contributed by Isamu Hasegawa <isamu@yamato.ibm.com>.
- 
--   This program is free software; you can redistribute it and/or modify
--   it under the terms of the GNU General Public License as published by
--   the Free Software Foundation; either version 3, or (at your option)
--   any later version.
-+   The GNU C Library is free software; you can redistribute it and/or
-+   modify it under the terms of the GNU Lesser General Public
-+   License as published by the Free Software Foundation; either
-+   version 2.1 of the License, or (at your option) any later version.
- 
--   This program is distributed in the hope that it will be useful,
-+   The GNU C Library is distributed in the hope that it will be useful,
-    but WITHOUT ANY WARRANTY; without even the implied warranty of
--   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
--   GNU General Public License for more details.
-+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
-+   Lesser General Public License for more details.
- 
--   You should have received a copy of the GNU General Public License along
--   with this program; if not, see <http://www.gnu.org/licenses/>.  */
-+   You should have received a copy of the GNU Lesser General Public
-+   License along with the GNU C Library; if not, see
-+   <http://www.gnu.org/licenses/>.  */
- 
- #ifndef _LIBC
- # include <config.h>
-@@ -25,6 +24,7 @@
- #  pragma GCC diagnostic ignored "-Wsuggest-attribute=pure"
- # endif
- # if (__GNUC__ == 4 && 3 <= __GNUC_MINOR__) || 4 < __GNUC__
-+#  pragma GCC diagnostic ignored "-Wold-style-definition"
- #  pragma GCC diagnostic ignored "-Wtype-limits"
- # endif
- #endif
---- origsrc/sed-4.2.2/lib/regex.h	2012-12-22 14:21:52.000000000 +0100
-+++ src/sed-4.2.2/lib/regex.h	2013-06-27 18:05:27.168447509 +0200
-@@ -1,23 +1,22 @@
--/* -*- buffer-read-only: t -*- vi: set ro: */
--/* DO NOT EDIT! GENERATED AUTOMATICALLY! */
- /* Definitions for data structures and routines for the regular
-    expression library.
--   Copyright (C) 1985, 1989-1993, 1995-1998, 2000-2003, 2005-2012
--   Free Software Foundation, Inc.
-+   Copyright (C) 1985, 1989-1993, 1995-1998, 2000-2003, 2005-2013 Free Software
-+   Foundation, Inc.
-    This file is part of the GNU C Library.
- 
--   This program is free software; you can redistribute it and/or modify
--   it under the terms of the GNU General Public License as published by
--   the Free Software Foundation; either version 3, or (at your option)
--   any later version.
-+   The GNU C Library is free software; you can redistribute it and/or
-+   modify it under the terms of the GNU Lesser General Public
-+   License as published by the Free Software Foundation; either
-+   version 2.1 of the License, or (at your option) any later version.
- 
--   This program is distributed in the hope that it will be useful,
-+   The GNU C Library is distributed in the hope that it will be useful,
-    but WITHOUT ANY WARRANTY; without even the implied warranty of
--   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
--   GNU General Public License for more details.
-+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
-+   Lesser General Public License for more details.
- 
--   You should have received a copy of the GNU General Public License along
--   with this program; if not, see <http://www.gnu.org/licenses/>.  */
-+   You should have received a copy of the GNU Lesser General Public
-+   License along with the GNU C Library; if not, see
-+   <http://www.gnu.org/licenses/>.  */
- 
- #ifndef _REGEX_H
- #define _REGEX_H 1
---- origsrc/sed-4.2.2/lib/regex_internal.c	2012-12-22 14:21:52.000000000 +0100
-+++ src/sed-4.2.2/lib/regex_internal.c	2013-06-27 18:05:27.199447375 +0200
-@@ -1,22 +1,21 @@
--/* -*- buffer-read-only: t -*- vi: set ro: */
--/* DO NOT EDIT! GENERATED AUTOMATICALLY! */
- /* Extended regular expression matching and search library.
--   Copyright (C) 2002-2012 Free Software Foundation, Inc.
-+   Copyright (C) 2002-2013 Free Software Foundation, Inc.
-    This file is part of the GNU C Library.
-    Contributed by Isamu Hasegawa <isamu@yamato.ibm.com>.
- 
--   This program is free software; you can redistribute it and/or modify
--   it under the terms of the GNU General Public License as published by
--   the Free Software Foundation; either version 3, or (at your option)
--   any later version.
-+   The GNU C Library is free software; you can redistribute it and/or
-+   modify it under the terms of the GNU Lesser General Public
-+   License as published by the Free Software Foundation; either
-+   version 2.1 of the License, or (at your option) any later version.
- 
--   This program is distributed in the hope that it will be useful,
-+   The GNU C Library is distributed in the hope that it will be useful,
-    but WITHOUT ANY WARRANTY; without even the implied warranty of
--   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
--   GNU General Public License for more details.
-+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
-+   Lesser General Public License for more details.
- 
--   You should have received a copy of the GNU General Public License along
--   with this program; if not, see <http://www.gnu.org/licenses/>.  */
-+   You should have received a copy of the GNU Lesser General Public
-+   License along with the GNU C Library; if not, see
-+   <http://www.gnu.org/licenses/>.  */
- 
- static void re_string_construct_common (const char *str, Idx len,
- 					re_string_t *pstr,
-@@ -835,7 +834,7 @@ re_string_reconstruct (re_string_t *pstr
- }
- 
- static unsigned char
--internal_function __attribute ((pure))
-+internal_function __attribute__ ((pure))
- re_string_peek_byte_case (const re_string_t *pstr, Idx idx)
- {
-   int ch;
-@@ -975,7 +974,7 @@ re_node_set_alloc (re_node_set *set, Idx
-   set->alloc = size;
-   set->nelem = 0;
-   set->elems = re_malloc (Idx, size);
--  if (BE (set->elems == NULL, 0))
-+  if (BE (set->elems == NULL, 0) && (MALLOC_0_IS_NONNULL || size != 0))
-     return REG_ESPACE;
-   return REG_NOERROR;
- }
-@@ -1355,7 +1354,7 @@ re_node_set_insert_last (re_node_set *se
-    Return true if SET1 and SET2 are equivalent.  */
- 
- static bool
--internal_function __attribute ((pure))
-+internal_function __attribute__ ((pure))
- re_node_set_compare (const re_node_set *set1, const re_node_set *set2)
- {
-   Idx i;
-@@ -1370,7 +1369,7 @@ re_node_set_compare (const re_node_set *
- /* Return (idx + 1) if SET contains the element ELEM, return 0 otherwise.  */
- 
- static Idx
--internal_function __attribute ((pure))
-+internal_function __attribute__ ((pure))
- re_node_set_contains (const re_node_set *set, Idx elem)
- {
-   __re_size_t idx, right, mid;
-@@ -1444,11 +1443,9 @@ re_dfa_add_node (re_dfa_t *dfa, re_token
-   dfa->nodes[dfa->nodes_len] = token;
-   dfa->nodes[dfa->nodes_len].constraint = 0;
- #ifdef RE_ENABLE_I18N
--  {
--  int type = token.type;
-   dfa->nodes[dfa->nodes_len].accept_mb =
--    (type == OP_PERIOD && dfa->mb_cur_max > 1) || type == COMPLEX_BRACKET;
--  }
-+    ((token.type == OP_PERIOD && dfa->mb_cur_max > 1)
-+     || token.type == COMPLEX_BRACKET);
- #endif
-   dfa->nexts[dfa->nodes_len] = REG_MISSING;
-   re_node_set_init_empty (dfa->edests + dfa->nodes_len);
---- origsrc/sed-4.2.2/lib/regex_internal.h	2012-12-22 14:21:52.000000000 +0100
-+++ src/sed-4.2.2/lib/regex_internal.h	2013-06-27 18:05:27.230447242 +0200
-@@ -1,22 +1,21 @@
--/* -*- buffer-read-only: t -*- vi: set ro: */
--/* DO NOT EDIT! GENERATED AUTOMATICALLY! */
- /* Extended regular expression matching and search library.
--   Copyright (C) 2002-2012 Free Software Foundation, Inc.
-+   Copyright (C) 2002-2013 Free Software Foundation, Inc.
-    This file is part of the GNU C Library.
-    Contributed by Isamu Hasegawa <isamu@yamato.ibm.com>.
- 
--   This program is free software; you can redistribute it and/or modify
--   it under the terms of the GNU General Public License as published by
--   the Free Software Foundation; either version 3, or (at your option)
--   any later version.
-+   The GNU C Library is free software; you can redistribute it and/or
-+   modify it under the terms of the GNU Lesser General Public
-+   License as published by the Free Software Foundation; either
-+   version 2.1 of the License, or (at your option) any later version.
- 
--   This program is distributed in the hope that it will be useful,
-+   The GNU C Library is distributed in the hope that it will be useful,
-    but WITHOUT ANY WARRANTY; without even the implied warranty of
--   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
--   GNU General Public License for more details.
-+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
-+   Lesser General Public License for more details.
- 
--   You should have received a copy of the GNU General Public License along
--   with this program; if not, see <http://www.gnu.org/licenses/>.  */
-+   You should have received a copy of the GNU Lesser General Public
-+   License along with the GNU C Library; if not, see
-+   <http://www.gnu.org/licenses/>.  */
- 
- #ifndef _REGEX_INTERNAL_H
- #define _REGEX_INTERNAL_H 1
-@@ -28,21 +27,54 @@
- #include <string.h>
- 
- #include <langinfo.h>
--#ifndef _LIBC
--# include "localcharset.h"
--#endif
- #include <locale.h>
- #include <wchar.h>
- #include <wctype.h>
- #include <stdbool.h>
- #include <stdint.h>
--#if defined _LIBC
-+
-+#ifdef _LIBC
- # include <bits/libc-lock.h>
-+# define lock_define(name) __libc_lock_define (, name)
-+# define lock_init(lock) (__libc_lock_init (lock), 0)
-+# define lock_fini(lock) 0
-+# define lock_lock(lock) __libc_lock_lock (lock)
-+# define lock_unlock(lock) __libc_lock_unlock (lock)
-+#elif defined GNULIB_LOCK
-+# include "glthread/lock.h"
-+  /* Use gl_lock_define if empty macro arguments are known to work.
-+     Otherwise, fall back on less-portable substitutes.  */
-+# if ((defined __GNUC__ && !defined __STRICT_ANSI__) \
-+      || (defined __STDC_VERSION__ && 199901L <= __STDC_VERSION__))
-+#  define lock_define(name) gl_lock_define (, name)
-+# elif USE_POSIX_THREADS
-+#  define lock_define(name) pthread_mutex_t name;
-+# elif USE_PTH_THREADS
-+#  define lock_define(name) pth_mutex_t name;
-+# elif USE_SOLARIS_THREADS
-+#  define lock_define(name) mutex_t name;
-+# elif USE_WINDOWS_THREADS
-+#  define lock_define(name) gl_lock_t name;
-+# else
-+#  define lock_define(name)
-+# endif
-+# define lock_init(lock) glthread_lock_init (&(lock))
-+# define lock_fini(lock) glthread_lock_destroy (&(lock))
-+# define lock_lock(lock) glthread_lock_lock (&(lock))
-+# define lock_unlock(lock) glthread_lock_unlock (&(lock))
-+#elif defined GNULIB_PTHREAD
-+# include <pthread.h>
-+# define lock_define(name) pthread_mutex_t name;
-+# define lock_init(lock) pthread_mutex_init (&(lock), 0)
-+# define lock_fini(lock) pthread_mutex_destroy (&(lock))
-+# define lock_lock(lock) pthread_mutex_lock (&(lock))
-+# define lock_unlock(lock) pthread_mutex_unlock (&(lock))
- #else
--# define __libc_lock_define(CLASS,NAME)
--# define __libc_lock_init(NAME) do { } while (0)
--# define __libc_lock_lock(NAME) do { } while (0)
--# define __libc_lock_unlock(NAME) do { } while (0)
-+# define lock_define(name)
-+# define lock_init(lock) 0
-+# define lock_fini(lock) 0
-+# define lock_lock(lock) ((void) 0)
-+# define lock_unlock(lock) ((void) 0)
- #endif
- 
- /* In case that the system doesn't have isblank().  */
-@@ -65,7 +97,7 @@
- # ifdef _LIBC
- #  undef gettext
- #  define gettext(msgid) \
--  INTUSE(__dcgettext) (_libc_intl_domainname, msgid, LC_MESSAGES)
-+  __dcgettext (_libc_intl_domainname, msgid, LC_MESSAGES)
- # endif
- #else
- # define gettext(msgid) (msgid)
-@@ -101,6 +133,8 @@
- 
- /* Rename to standard API for using out of glibc.  */
- #ifndef _LIBC
-+# undef __wctype
-+# undef __iswctype
- # define __wctype wctype
- # define __iswctype iswctype
- # define __btowc btowc
-@@ -110,10 +144,8 @@
- # define attribute_hidden
- #endif /* not _LIBC */
- 
--#if __GNUC__ >= 4 || (__GNUC__ == 3 && __GNUC_MINOR__ >= 1)
--# define __attribute(arg) __attribute__ (arg)
--#else
--# define __attribute(arg)
-+#if __GNUC__ < 3 + (__GNUC_MINOR__ < 1)
-+# define __attribute__(arg)
- #endif
- 
- typedef __re_idx_t Idx;
-@@ -429,7 +461,7 @@ static void build_upper_buffer (re_strin
- static void re_string_translate_buffer (re_string_t *pstr) internal_function;
- static unsigned int re_string_context_at (const re_string_t *input, Idx idx,
- 					  int eflags)
--     internal_function __attribute ((pure));
-+     internal_function __attribute__ ((pure));
- #endif
- #define re_string_peek_byte(pstr, offset) \
-   ((pstr)->mbs[(pstr)->cur_idx + offset])
-@@ -448,7 +480,9 @@ static unsigned int re_string_context_at
- #define re_string_skip_bytes(pstr,idx) ((pstr)->cur_idx += (idx))
- #define re_string_set_index(pstr,idx) ((pstr)->cur_idx = (idx))
- 
--#include <alloca.h>
-+#if defined _LIBC || HAVE_ALLOCA
-+# include <alloca.h>
-+#endif
- 
- #ifndef _LIBC
- # if HAVE_ALLOCA
-@@ -465,6 +499,12 @@ static unsigned int re_string_context_at
- # endif
- #endif
- 
-+#ifdef _LIBC
-+# define MALLOC_0_IS_NONNULL 1
-+#elif !defined MALLOC_0_IS_NONNULL
-+# define MALLOC_0_IS_NONNULL 0
-+#endif
-+
- #ifndef MAX
- # define MAX(a,b) ((a) < (b) ? (b) : (a))
- #endif
-@@ -695,7 +735,7 @@ struct re_dfa_t
- #ifdef DEBUG
-   char* re_str;
- #endif
--  __libc_lock_define (, lock)
-+  lock_define (lock)
- };
- 
- #define re_node_set_init_empty(set) memset (set, '\0', sizeof (re_node_set))
-@@ -767,7 +807,7 @@ bitset_copy (bitset_t dest, const bitset
-   memcpy (dest, src, sizeof (bitset_t));
- }
- 
--static void
-+static void __attribute__ ((unused))
- bitset_not (bitset_t set)
- {
-   int bitset_i;
-@@ -779,7 +819,7 @@ bitset_not (bitset_t set)
-        & ~set[BITSET_WORDS - 1]);
- }
- 
--static void
-+static void __attribute__ ((unused))
- bitset_merge (bitset_t dest, const bitset_t src)
- {
-   int bitset_i;
-@@ -787,7 +827,7 @@ bitset_merge (bitset_t dest, const bitse
-     dest[bitset_i] |= src[bitset_i];
- }
- 
--static void
-+static void __attribute__ ((unused))
- bitset_mask (bitset_t dest, const bitset_t src)
- {
-   int bitset_i;
-@@ -798,7 +838,7 @@ bitset_mask (bitset_t dest, const bitset
- #ifdef RE_ENABLE_I18N
- /* Functions for re_string.  */
- static int
--internal_function __attribute ((pure))
-+internal_function __attribute__ ((pure, unused))
- re_string_char_size_at (const re_string_t *pstr, Idx idx)
- {
-   int byte_idx;
-@@ -811,7 +851,7 @@ re_string_char_size_at (const re_string_
- }
- 
- static wint_t
--internal_function __attribute ((pure))
-+internal_function __attribute__ ((pure, unused))
- re_string_wchar_at (const re_string_t *pstr, Idx idx)
- {
-   if (pstr->mb_cur_max == 1)
-@@ -821,7 +861,7 @@ re_string_wchar_at (const re_string_t *p
- 
- # ifndef NOT_IN_libc
- static int
--internal_function __attribute ((pure))
-+internal_function __attribute__ ((pure, unused))
- re_string_elem_size_at (const re_string_t *pstr, Idx idx)
- {
- #  ifdef _LIBC
---- origsrc/sed-4.2.2/lib/regexec.c	2012-12-22 14:21:52.000000000 +0100
-+++ src/sed-4.2.2/lib/regexec.c	2013-06-27 18:05:27.268447078 +0200
-@@ -1,22 +1,21 @@
--/* -*- buffer-read-only: t -*- vi: set ro: */
--/* DO NOT EDIT! GENERATED AUTOMATICALLY! */
- /* Extended regular expression matching and search library.
--   Copyright (C) 2002-2012 Free Software Foundation, Inc.
-+   Copyright (C) 2002-2013 Free Software Foundation, Inc.
-    This file is part of the GNU C Library.
-    Contributed by Isamu Hasegawa <isamu@yamato.ibm.com>.
- 
--   This program is free software; you can redistribute it and/or modify
--   it under the terms of the GNU General Public License as published by
--   the Free Software Foundation; either version 3, or (at your option)
--   any later version.
-+   The GNU C Library is free software; you can redistribute it and/or
-+   modify it under the terms of the GNU Lesser General Public
-+   License as published by the Free Software Foundation; either
-+   version 2.1 of the License, or (at your option) any later version.
- 
--   This program is distributed in the hope that it will be useful,
-+   The GNU C Library is distributed in the hope that it will be useful,
-    but WITHOUT ANY WARRANTY; without even the implied warranty of
--   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
--   GNU General Public License for more details.
-+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
-+   Lesser General Public License for more details.
- 
--   You should have received a copy of the GNU General Public License along
--   with this program; if not, see <http://www.gnu.org/licenses/>.  */
-+   You should have received a copy of the GNU Lesser General Public
-+   License along with the GNU C Library; if not, see
-+   <http://www.gnu.org/licenses/>.  */
- 
- static reg_errcode_t match_ctx_init (re_match_context_t *cache, int eflags,
- 				     Idx n) internal_function;
-@@ -200,7 +199,7 @@ static Idx group_nodes_into_DFAstates (c
- static bool check_node_accept (const re_match_context_t *mctx,
- 			       const re_token_t *node, Idx idx)
-      internal_function;
--static reg_errcode_t extend_buffers (re_match_context_t *mctx)
-+static reg_errcode_t extend_buffers (re_match_context_t *mctx, int min_len)
-      internal_function;
- 
- /* Entry point for POSIX code.  */
-@@ -229,9 +228,7 @@ regexec (preg, string, nmatch, pmatch, e
- {
-   reg_errcode_t err;
-   Idx start, length;
--#ifdef _LIBC
-   re_dfa_t *dfa = preg->buffer;
--#endif
- 
-   if (eflags & ~(REG_NOTBOL | REG_NOTEOL | REG_STARTEND))
-     return REG_BADPAT;
-@@ -247,14 +244,14 @@ regexec (preg, string, nmatch, pmatch, e
-       length = strlen (string);
-     }
- 
--  __libc_lock_lock (dfa->lock);
-+  lock_lock (dfa->lock);
-   if (preg->no_sub)
-     err = re_search_internal (preg, string, length, start, length,
- 			      length, 0, NULL, eflags);
-   else
-     err = re_search_internal (preg, string, length, start, length,
- 			      length, nmatch, pmatch, eflags);
--  __libc_lock_unlock (dfa->lock);
-+  lock_unlock (dfa->lock);
-   return err != REG_NOERROR;
- }
- 
-@@ -422,9 +419,7 @@ re_search_stub (struct re_pattern_buffer
-   Idx nregs;
-   regoff_t rval;
-   int eflags = 0;
--#ifdef _LIBC
-   re_dfa_t *dfa = bufp->buffer;
--#endif
-   Idx last_start = start + range;
- 
-   /* Check for out-of-range.  */
-@@ -435,7 +430,7 @@ re_search_stub (struct re_pattern_buffer
-   else if (BE (last_start < 0 || (range < 0 && start <= last_start), 0))
-     last_start = 0;
- 
--  __libc_lock_lock (dfa->lock);
-+  lock_lock (dfa->lock);
- 
-   eflags |= (bufp->not_bol) ? REG_NOTBOL : 0;
-   eflags |= (bufp->not_eol) ? REG_NOTEOL : 0;
-@@ -499,7 +494,7 @@ re_search_stub (struct re_pattern_buffer
-     }
-   re_free (pmatch);
-  out:
--  __libc_lock_unlock (dfa->lock);
-+  lock_unlock (dfa->lock);
-   return rval;
- }
- 
-@@ -1065,7 +1060,7 @@ prune_impossible_nodes (re_match_context
-    since initial states may have constraints like "\<", "^", etc..  */
- 
- static inline re_dfastate_t *
--__attribute ((always_inline)) internal_function
-+__attribute__ ((always_inline)) internal_function
- acquire_init_state_context (reg_errcode_t *err, const re_match_context_t *mctx,
- 			    Idx idx)
- {
-@@ -1177,7 +1172,7 @@ check_matching (re_match_context_t *mctx
- 	  || (BE (next_char_idx >= mctx->input.valid_len, 0)
- 	      && mctx->input.valid_len < mctx->input.len))
- 	{
--	  err = extend_buffers (mctx);
-+	  err = extend_buffers (mctx, next_char_idx + 1);
- 	  if (BE (err != REG_NOERROR, 0))
- 	    {
- 	      assert (err == REG_ESPACE);
-@@ -1757,7 +1752,7 @@ clean_state_log_if_needed (re_match_cont
- 	  && mctx->input.valid_len < mctx->input.len))
-     {
-       reg_errcode_t err;
--      err = extend_buffers (mctx);
-+      err = extend_buffers (mctx, next_state_log_idx + 1);
-       if (BE (err != REG_NOERROR, 0))
- 	return err;
-     }
-@@ -2814,7 +2809,7 @@ get_subexp (re_match_context_t *mctx, Id
- 		  if (bkref_str_off >= mctx->input.len)
- 		    break;
- 
--		  err = extend_buffers (mctx);
-+		  err = extend_buffers (mctx, bkref_str_off + 1);
- 		  if (BE (err != REG_NOERROR, 0))
- 		    return err;
- 
-@@ -3937,6 +3932,7 @@ check_node_accept_bytes (const re_dfa_t
- 		in_collseq = find_collation_sequence_value (pin, elem_len);
- 	    }
- 	  /* match with range expression?  */
-+	  /* FIXME: Implement rational ranges here, too.  */
- 	  for (i = 0; i < cset->nranges; ++i)
- 	    if (cset->range_starts[i] <= in_collseq
- 		&& in_collseq <= cset->range_ends[i])
-@@ -3988,18 +3984,9 @@ check_node_accept_bytes (const re_dfa_t
- # endif /* _LIBC */
- 	{
- 	  /* match with range expression?  */
--#if __GNUC__ >= 2 && ! (__STDC_VERSION__ < 199901L && defined __STRICT_ANSI__)
--	  wchar_t cmp_buf[] = {L'\0', L'\0', wc, L'\0', L'\0', L'\0'};
--#else
--	  wchar_t cmp_buf[] = {L'\0', L'\0', L'\0', L'\0', L'\0', L'\0'};
--	  cmp_buf[2] = wc;
--#endif
- 	  for (i = 0; i < cset->nranges; ++i)
- 	    {
--	      cmp_buf[0] = cset->range_starts[i];
--	      cmp_buf[4] = cset->range_ends[i];
--	      if (wcscoll (cmp_buf, cmp_buf + 2) <= 0
--		  && wcscoll (cmp_buf + 2, cmp_buf + 4) <= 0)
-+	      if (cset->range_starts[i] <= wc && wc <= cset->range_ends[i])
- 		{
- 		  match_len = char_len;
- 		  goto check_node_accept_bytes_match;
-@@ -4137,7 +4124,7 @@ check_node_accept (const re_match_contex
- 
- static reg_errcode_t
- internal_function __attribute_warn_unused_result__
--extend_buffers (re_match_context_t *mctx)
-+extend_buffers (re_match_context_t *mctx, int min_len)
- {
-   reg_errcode_t ret;
-   re_string_t *pstr = &mctx->input;
-@@ -4147,8 +4134,10 @@ extend_buffers (re_match_context_t *mctx
-           <= pstr->bufs_len, 0))
-     return REG_ESPACE;
- 
--  /* Double the lengths of the buffers.  */
--  ret = re_string_realloc_buffers (pstr, MIN (pstr->len, pstr->bufs_len * 2));
-+  /* Double the lengths of the buffers, but allocate at least MIN_LEN.  */
-+  ret = re_string_realloc_buffers (pstr,
-+				   MAX (min_len,
-+					MIN (pstr->len, pstr->bufs_len * 2)));
-   if (BE (ret != REG_NOERROR, 0))
-     return ret;
- 
---- origsrc/sed-4.2.2/sed/sed.c	2012-03-16 10:13:31.000000000 +0100
-+++ src/sed-4.2.2/sed/sed.c	2013-06-27 18:06:25.592195456 +0200
-@@ -57,7 +57,11 @@ bool follow_symlinks = false;
- char *in_place_extension = NULL;
- 
- /* The mode to use to read/write files, either "r"/"w" or "rb"/"wb".  */
-+#ifdef HAVE_FOPEN_RT
-+char *read_mode = "rt";
-+#else
- char *read_mode = "r";
-+#endif
- char *write_mode = "w";
- 
- /* Do we need to be pedantically POSIX compliant? */
diff --git a/dev/build/windows/patches_coq/sed-4.2.2.patch b/dev/build/windows/patches_coq/sed-4.2.2.patch
deleted file mode 100644
index c7ccd53c7f..0000000000
--- a/dev/build/windows/patches_coq/sed-4.2.2.patch
+++ /dev/null
@@ -1,1301 +0,0 @@
---- origsrc/doc/sed.1	2012-12-22 15:27:13.000000000 +0100
-+++ src/doc/sed.1	2013-06-27 18:10:47.974060492 +0200
-@@ -1,5 +1,5 @@
- .\" DO NOT MODIFY THIS FILE!  It was generated by help2man 1.28.
--.TH SED "1" "December 2012" "sed 4.2.2" "User Commands"
-+.TH SED "1" "June 2013" "sed 4.2.2" "User Commands"
- .SH NAME
- sed \- stream editor for filtering and transforming text
- .SH SYNOPSIS
-@@ -40,6 +40,10 @@ follow symlinks when processing in place
- .IP
- edit files in place (makes backup if SUFFIX supplied)
- .HP
-+\fB\-b\fR, \fB\-\-binary\fR
-+.IP
-+open files in binary mode (CR+LFs are not processed specially)
-+.HP
- \fB\-l\fR N, \fB\-\-line\-length\fR=\fIN\fR
- .IP
- specify the desired line-wrap length for the `l' command
---- origsrc/lib/regcomp.c	2012-12-22 14:21:52.000000000 +0100
-+++ src/lib/regcomp.c	2013-06-27 18:05:27.044448044 +0200
-@@ -1,22 +1,21 @@
--/* -*- buffer-read-only: t -*- vi: set ro: */
--/* DO NOT EDIT! GENERATED AUTOMATICALLY! */
- /* Extended regular expression matching and search library.
--   Copyright (C) 2002-2012 Free Software Foundation, Inc.
-+   Copyright (C) 2002-2013 Free Software Foundation, Inc.
-    This file is part of the GNU C Library.
-    Contributed by Isamu Hasegawa <isamu@yamato.ibm.com>.
- 
--   This program is free software; you can redistribute it and/or modify
--   it under the terms of the GNU General Public License as published by
--   the Free Software Foundation; either version 3, or (at your option)
--   any later version.
-+   The GNU C Library is free software; you can redistribute it and/or
-+   modify it under the terms of the GNU Lesser General Public
-+   License as published by the Free Software Foundation; either
-+   version 2.1 of the License, or (at your option) any later version.
- 
--   This program is distributed in the hope that it will be useful,
-+   The GNU C Library is distributed in the hope that it will be useful,
-    but WITHOUT ANY WARRANTY; without even the implied warranty of
--   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
--   GNU General Public License for more details.
-+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
-+   Lesser General Public License for more details.
- 
--   You should have received a copy of the GNU General Public License along
--   with this program; if not, see <http://www.gnu.org/licenses/>.  */
-+   You should have received a copy of the GNU Lesser General Public
-+   License along with the GNU C Library; if not, see
-+   <http://www.gnu.org/licenses/>.  */
- 
- static reg_errcode_t re_compile_internal (regex_t *preg, const char * pattern,
- 					  size_t length, reg_syntax_t syntax);
-@@ -95,20 +94,20 @@ static reg_errcode_t build_charclass (RE
- 				      bitset_t sbcset,
- 				      re_charset_t *mbcset,
- 				      Idx *char_class_alloc,
--				      const unsigned char *class_name,
-+				      const char *class_name,
- 				      reg_syntax_t syntax);
- #else  /* not RE_ENABLE_I18N */
- static reg_errcode_t build_equiv_class (bitset_t sbcset,
- 					const unsigned char *name);
- static reg_errcode_t build_charclass (RE_TRANSLATE_TYPE trans,
- 				      bitset_t sbcset,
--				      const unsigned char *class_name,
-+				      const char *class_name,
- 				      reg_syntax_t syntax);
- #endif /* not RE_ENABLE_I18N */
- static bin_tree_t *build_charclass_op (re_dfa_t *dfa,
- 				       RE_TRANSLATE_TYPE trans,
--				       const unsigned char *class_name,
--				       const unsigned char *extra,
-+				       const char *class_name,
-+				       const char *extra,
- 				       bool non_match, reg_errcode_t *err);
- static bin_tree_t *create_tree (re_dfa_t *dfa,
- 				bin_tree_t *left, bin_tree_t *right,
-@@ -293,7 +292,7 @@ weak_alias (__re_compile_fastmap, re_com
- #endif
- 
- static inline void
--__attribute ((always_inline))
-+__attribute__ ((always_inline))
- re_set_fastmap (char *fastmap, bool icase, int ch)
- {
-   fastmap[ch] = 1;
-@@ -587,7 +586,7 @@ weak_alias (__regerror, regerror)
- static const bitset_t utf8_sb_map =
- {
-   /* Set the first 128 bits.  */
--# ifdef __GNUC__
-+# if defined __GNUC__ && !defined __STRICT_ANSI__
-   [0 ... 0x80 / BITSET_WORD_BITS - 1] = BITSET_WORD_MAX
- # else
- #  if 4 * BITSET_WORD_BITS < ASCII_CHARS
-@@ -664,7 +663,10 @@ regfree (preg)
- {
-   re_dfa_t *dfa = preg->buffer;
-   if (BE (dfa != NULL, 1))
--    free_dfa_content (dfa);
-+    {
-+      lock_fini (dfa->lock);
-+      free_dfa_content (dfa);
-+    }
-   preg->buffer = NULL;
-   preg->allocated = 0;
- 
-@@ -785,6 +787,8 @@ re_compile_internal (regex_t *preg, cons
-   preg->used = sizeof (re_dfa_t);
- 
-   err = init_dfa (dfa, length);
-+  if (BE (err == REG_NOERROR && lock_init (dfa->lock) != 0, 0))
-+    err = REG_ESPACE;
-   if (BE (err != REG_NOERROR, 0))
-     {
-       free_dfa_content (dfa);
-@@ -798,8 +802,6 @@ re_compile_internal (regex_t *preg, cons
-   strncpy (dfa->re_str, pattern, length + 1);
- #endif
- 
--  __libc_lock_init (dfa->lock);
--
-   err = re_string_construct (&regexp, pattern, length, preg->translate,
- 			     (syntax & RE_ICASE) != 0, dfa);
-   if (BE (err != REG_NOERROR, 0))
-@@ -807,6 +809,7 @@ re_compile_internal (regex_t *preg, cons
-     re_compile_internal_free_return:
-       free_workarea_compile (preg);
-       re_string_destruct (&regexp);
-+      lock_fini (dfa->lock);
-       free_dfa_content (dfa);
-       preg->buffer = NULL;
-       preg->allocated = 0;
-@@ -839,6 +842,7 @@ re_compile_internal (regex_t *preg, cons
- 
-   if (BE (err != REG_NOERROR, 0))
-     {
-+      lock_fini (dfa->lock);
-       free_dfa_content (dfa);
-       preg->buffer = NULL;
-       preg->allocated = 0;
-@@ -954,10 +958,10 @@ static void
- internal_function
- init_word_char (re_dfa_t *dfa)
- {
--  dfa->word_ops_used = 1;
-   int i = 0;
-   int j;
-   int ch = 0;
-+  dfa->word_ops_used = 1;
-   if (BE (dfa->map_notascii == 0, 1))
-     {
-       bitset_word_t bits0 = 0x00000000;
-@@ -2423,8 +2427,8 @@ parse_expression (re_string_t *regexp, r
-     case OP_WORD:
-     case OP_NOTWORD:
-       tree = build_charclass_op (dfa, regexp->trans,
--				 (const unsigned char *) "alnum",
--				 (const unsigned char *) "_",
-+				 "alnum",
-+				 "_",
- 				 token->type == OP_NOTWORD, err);
-       if (BE (*err != REG_NOERROR && tree == NULL, 0))
- 	return NULL;
-@@ -2432,8 +2436,8 @@ parse_expression (re_string_t *regexp, r
-     case OP_SPACE:
-     case OP_NOTSPACE:
-       tree = build_charclass_op (dfa, regexp->trans,
--				 (const unsigned char *) "space",
--				 (const unsigned char *) "",
-+				 "space",
-+				 "",
- 				 token->type == OP_NOTSPACE, err);
-       if (BE (*err != REG_NOERROR && tree == NULL, 0))
- 	return NULL;
-@@ -2713,7 +2717,6 @@ build_range_exp (const reg_syntax_t synt
-     wchar_t wc;
-     wint_t start_wc;
-     wint_t end_wc;
--    wchar_t cmp_buf[6] = {L'\0', L'\0', L'\0', L'\0', L'\0', L'\0'};
- 
-     start_ch = ((start_elem->type == SB_CHAR) ? start_elem->opr.ch
- 		: ((start_elem->type == COLL_SYM) ? start_elem->opr.name[0]
-@@ -2727,11 +2730,7 @@ build_range_exp (const reg_syntax_t synt
- 	      ? __btowc (end_ch) : end_elem->opr.wch);
-     if (start_wc == WEOF || end_wc == WEOF)
-       return REG_ECOLLATE;
--    cmp_buf[0] = start_wc;
--    cmp_buf[4] = end_wc;
--
--    if (BE ((syntax & RE_NO_EMPTY_RANGES)
--            && wcscoll (cmp_buf, cmp_buf + 4) > 0, 0))
-+    else if (BE ((syntax & RE_NO_EMPTY_RANGES) && start_wc > end_wc, 0))
-       return REG_ERANGE;
- 
-     /* Got valid collation sequence values, add them as a new entry.
-@@ -2772,9 +2771,7 @@ build_range_exp (const reg_syntax_t synt
-     /* Build the table for single byte characters.  */
-     for (wc = 0; wc < SBC_MAX; ++wc)
-       {
--	cmp_buf[2] = wc;
--	if (wcscoll (cmp_buf, cmp_buf + 2) <= 0
--	    && wcscoll (cmp_buf + 2, cmp_buf + 4) <= 0)
-+	if (start_wc <= wc && wc <= end_wc)
- 	  bitset_set (sbcset, wc);
-       }
-   }
-@@ -2843,40 +2840,29 @@ parse_bracket_exp (re_string_t *regexp,
- 
-   /* Local function for parse_bracket_exp used in _LIBC environment.
-      Seek the collating symbol entry corresponding to NAME.
--     Return the index of the symbol in the SYMB_TABLE.  */
-+     Return the index of the symbol in the SYMB_TABLE,
-+     or -1 if not found.  */
- 
-   auto inline int32_t
--  __attribute ((always_inline))
--  seek_collating_symbol_entry (name, name_len)
--	 const unsigned char *name;
--	 size_t name_len;
--    {
--      int32_t hash = elem_hash ((const char *) name, name_len);
--      int32_t elem = hash % table_size;
--      if (symb_table[2 * elem] != 0)
--	{
--	  int32_t second = hash % (table_size - 2) + 1;
--
--	  do
--	    {
--	      /* First compare the hashing value.  */
--	      if (symb_table[2 * elem] == hash
--		  /* Compare the length of the name.  */
--		  && name_len == extra[symb_table[2 * elem + 1]]
--		  /* Compare the name.  */
--		  && memcmp (name, &extra[symb_table[2 * elem + 1] + 1],
--			     name_len) == 0)
--		{
--		  /* Yep, this is the entry.  */
--		  break;
--		}
-+  __attribute__ ((always_inline))
-+  seek_collating_symbol_entry (const unsigned char *name, size_t name_len)
-+    {
-+      int32_t elem;
- 
--	      /* Next entry.  */
--	      elem += second;
--	    }
--	  while (symb_table[2 * elem] != 0);
--	}
--      return elem;
-+      for (elem = 0; elem < table_size; elem++)
-+	if (symb_table[2 * elem] != 0)
-+	  {
-+	    int32_t idx = symb_table[2 * elem + 1];
-+	    /* Skip the name of collating element name.  */
-+	    idx += 1 + extra[idx];
-+	    if (/* Compare the length of the name.  */
-+		name_len == extra[idx]
-+		/* Compare the name.  */
-+		&& memcmp (name, &extra[idx + 1], name_len) == 0)
-+	      /* Yep, this is the entry.  */
-+	      return elem;
-+	  }
-+      return -1;
-     }
- 
-   /* Local function for parse_bracket_exp used in _LIBC environment.
-@@ -2884,9 +2870,8 @@ parse_bracket_exp (re_string_t *regexp,
-      Return the value if succeeded, UINT_MAX otherwise.  */
- 
-   auto inline unsigned int
--  __attribute ((always_inline))
--  lookup_collation_sequence_value (br_elem)
--	 bracket_elem_t *br_elem;
-+  __attribute__ ((always_inline))
-+  lookup_collation_sequence_value (bracket_elem_t *br_elem)
-     {
-       if (br_elem->type == SB_CHAR)
- 	{
-@@ -2914,7 +2899,7 @@ parse_bracket_exp (re_string_t *regexp,
- 	      int32_t elem, idx;
- 	      elem = seek_collating_symbol_entry (br_elem->opr.name,
- 						  sym_name_len);
--	      if (symb_table[2 * elem] != 0)
-+	      if (elem != -1)
- 		{
- 		  /* We found the entry.  */
- 		  idx = symb_table[2 * elem + 1];
-@@ -2932,7 +2917,7 @@ parse_bracket_exp (re_string_t *regexp,
- 		  /* Return the collation sequence value.  */
- 		  return *(unsigned int *) (extra + idx);
- 		}
--	      else if (symb_table[2 * elem] == 0 && sym_name_len == 1)
-+	      else if (sym_name_len == 1)
- 		{
- 		  /* No valid character.  Match it as a single byte
- 		     character.  */
-@@ -2953,12 +2938,9 @@ parse_bracket_exp (re_string_t *regexp,
-      update it.  */
- 
-   auto inline reg_errcode_t
--  __attribute ((always_inline))
--  build_range_exp (sbcset, mbcset, range_alloc, start_elem, end_elem)
--	 re_charset_t *mbcset;
--	 Idx *range_alloc;
--	 bitset_t sbcset;
--	 bracket_elem_t *start_elem, *end_elem;
-+  __attribute__ ((always_inline))
-+  build_range_exp (bitset_t sbcset, re_charset_t *mbcset, int *range_alloc,
-+		   bracket_elem_t *start_elem, bracket_elem_t *end_elem)
-     {
-       unsigned int ch;
-       uint32_t start_collseq;
-@@ -2971,6 +2953,7 @@ parse_bracket_exp (re_string_t *regexp,
- 	      0))
- 	return REG_ERANGE;
- 
-+      /* FIXME: Implement rational ranges here, too.  */
-       start_collseq = lookup_collation_sequence_value (start_elem);
-       end_collseq = lookup_collation_sequence_value (end_elem);
-       /* Check start/end collation sequence values.  */
-@@ -3036,26 +3019,23 @@ parse_bracket_exp (re_string_t *regexp,
-      pointer argument since we may update it.  */
- 
-   auto inline reg_errcode_t
--  __attribute ((always_inline))
--  build_collating_symbol (sbcset, mbcset, coll_sym_alloc, name)
--	 re_charset_t *mbcset;
--	 Idx *coll_sym_alloc;
--	 bitset_t sbcset;
--	 const unsigned char *name;
-+  __attribute__ ((always_inline))
-+  build_collating_symbol (bitset_t sbcset, re_charset_t *mbcset,
-+			  Idx *coll_sym_alloc, const unsigned char *name)
-     {
-       int32_t elem, idx;
-       size_t name_len = strlen ((const char *) name);
-       if (nrules != 0)
- 	{
- 	  elem = seek_collating_symbol_entry (name, name_len);
--	  if (symb_table[2 * elem] != 0)
-+	  if (elem != -1)
- 	    {
- 	      /* We found the entry.  */
- 	      idx = symb_table[2 * elem + 1];
- 	      /* Skip the name of collating element name.  */
- 	      idx += 1 + extra[idx];
- 	    }
--	  else if (symb_table[2 * elem] == 0 && name_len == 1)
-+	  else if (name_len == 1)
- 	    {
- 	      /* No valid character, treat it as a normal
- 		 character.  */
-@@ -3298,7 +3278,8 @@ parse_bracket_exp (re_string_t *regexp,
- #ifdef RE_ENABLE_I18N
- 				      mbcset, &char_class_alloc,
- #endif /* RE_ENABLE_I18N */
--				      start_elem.opr.name, syntax);
-+				      (const char *) start_elem.opr.name,
-+				      syntax);
- 	      if (BE (*err != REG_NOERROR, 0))
- 	       goto parse_bracket_exp_free_return;
- 	      break;
-@@ -3578,14 +3559,14 @@ static reg_errcode_t
- #ifdef RE_ENABLE_I18N
- build_charclass (RE_TRANSLATE_TYPE trans, bitset_t sbcset,
- 		 re_charset_t *mbcset, Idx *char_class_alloc,
--		 const unsigned char *class_name, reg_syntax_t syntax)
-+		 const char *class_name, reg_syntax_t syntax)
- #else /* not RE_ENABLE_I18N */
- build_charclass (RE_TRANSLATE_TYPE trans, bitset_t sbcset,
--		 const unsigned char *class_name, reg_syntax_t syntax)
-+		 const char *class_name, reg_syntax_t syntax)
- #endif /* not RE_ENABLE_I18N */
- {
-   int i;
--  const char *name = (const char *) class_name;
-+  const char *name = class_name;
- 
-   /* In case of REG_ICASE "upper" and "lower" match the both of
-      upper and lower cases.  */
-@@ -3659,8 +3640,8 @@ build_charclass (RE_TRANSLATE_TYPE trans
- 
- static bin_tree_t *
- build_charclass_op (re_dfa_t *dfa, RE_TRANSLATE_TYPE trans,
--		    const unsigned char *class_name,
--		    const unsigned char *extra, bool non_match,
-+		    const char *class_name,
-+		    const char *extra, bool non_match,
- 		    reg_errcode_t *err)
- {
-   re_bitset_ptr_t sbcset;
---- origsrc/lib/regex-quote.c	1970-01-01 01:00:00.000000000 +0100
-+++ src/lib/regex-quote.c	2013-06-27 18:05:27.081447884 +0200
-@@ -0,0 +1,216 @@
-+/* Construct a regular expression from a literal string.
-+   Copyright (C) 1995, 2010-2013 Free Software Foundation, Inc.
-+   Written by Bruno Haible <haible@clisp.cons.org>, 2010.
-+
-+   This program is free software: you can redistribute it and/or modify
-+   it under the terms of the GNU General Public License as published by
-+   the Free Software Foundation; either version 3 of the License, or
-+   (at your option) any later version.
-+
-+   This program is distributed in the hope that it will be useful,
-+   but WITHOUT ANY WARRANTY; without even the implied warranty of
-+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-+   GNU General Public License for more details.
-+
-+   You should have received a copy of the GNU General Public License
-+   along with this program.  If not, see <http://www.gnu.org/licenses/>.  */
-+
-+#include <config.h>
-+
-+/* Specification.  */
-+#include "regex-quote.h"
-+
-+#include <string.h>
-+
-+#include "mbuiter.h"
-+#include "xalloc.h"
-+
-+/* Characters that are special in a BRE.  */
-+static const char bre_special[] = "$^.*[]\\";
-+
-+/* Characters that are special in an ERE.  */
-+static const char ere_special[] = "$^.*[]\\+?{}()|";
-+
-+struct regex_quote_spec
-+regex_quote_spec_posix (int cflags, bool anchored)
-+{
-+  struct regex_quote_spec result;
-+
-+  strcpy (result.special, cflags != 0 ? ere_special : bre_special);
-+  result.multibyte = true;
-+  result.anchored = anchored;
-+
-+  return result;
-+}
-+
-+/* Syntax bit values, defined in GNU <regex.h>.  We don't include it here,
-+   otherwise this module would need to depend on gnulib module 'regex'.  */
-+#define RE_BK_PLUS_QM    0x00000002
-+#define RE_INTERVALS     0x00000200
-+#define RE_LIMITED_OPS   0x00000400
-+#define RE_NEWLINE_ALT   0x00000800
-+#define RE_NO_BK_BRACES  0x00001000
-+#define RE_NO_BK_PARENS  0x00002000
-+#define RE_NO_BK_VBAR    0x00008000
-+
-+struct regex_quote_spec
-+regex_quote_spec_gnu (unsigned long /*reg_syntax_t*/ syntax, bool anchored)
-+{
-+  struct regex_quote_spec result;
-+  char *p;
-+
-+  p = result.special;
-+  memcpy (p, bre_special, sizeof (bre_special) - 1);
-+  p += sizeof (bre_special) - 1;
-+  if ((syntax & RE_LIMITED_OPS) == 0 && (syntax & RE_BK_PLUS_QM) == 0)
-+    {
-+      *p++ = '+';
-+      *p++ = '?';
-+    }
-+  if ((syntax & RE_INTERVALS) != 0 && (syntax & RE_NO_BK_BRACES) != 0)
-+    {
-+      *p++ = '{';
-+      *p++ = '}';
-+    }
-+  if ((syntax & RE_NO_BK_PARENS) != 0)
-+    {
-+      *p++ = '(';
-+      *p++ = ')';
-+    }
-+  if ((syntax & RE_LIMITED_OPS) == 0 && (syntax & RE_NO_BK_VBAR) != 0)
-+    *p++ = '|';
-+  if ((syntax & RE_NEWLINE_ALT) != 0)
-+    *p++ = '\n';
-+  *p = '\0';
-+
-+  result.multibyte = true;
-+  result.anchored = anchored;
-+
-+  return result;
-+}
-+
-+/* Characters that are special in a PCRE.  */
-+static const char pcre_special[] = "$^.*[]\\+?{}()|";
-+
-+/* Options bit values, defined in <pcre.h>.  We don't include it here, because
-+   it is not a standard header.  */
-+#define PCRE_ANCHORED 0x00000010
-+#define PCRE_EXTENDED 0x00000008
-+
-+struct regex_quote_spec
-+regex_quote_spec_pcre (int options, bool anchored)
-+{
-+  struct regex_quote_spec result;
-+  char *p;
-+
-+  p = result.special;
-+  memcpy (p, bre_special, sizeof (pcre_special) - 1);
-+  p += sizeof (pcre_special) - 1;
-+  if (options & PCRE_EXTENDED)
-+    {
-+      *p++ = ' ';
-+      *p++ = '\t';
-+      *p++ = '\n';
-+      *p++ = '\v';
-+      *p++ = '\f';
-+      *p++ = '\r';
-+      *p++ = '#';
-+    }
-+  *p = '\0';
-+
-+  /* PCRE regular expressions consist of UTF-8 characters of options contains
-+     PCRE_UTF8 and of single bytes otherwise.  */
-+  result.multibyte = false;
-+  /* If options contains PCRE_ANCHORED, the anchoring is implicit.  */
-+  result.anchored = (options & PCRE_ANCHORED ? 0 : anchored);
-+
-+  return result;
-+}
-+
-+size_t
-+regex_quote_length (const char *string, const struct regex_quote_spec *spec)
-+{
-+  const char *special = spec->special;
-+  size_t length;
-+
-+  length = 0;
-+  if (spec->anchored)
-+    length += 2; /* for '^' at the beginning and '$' at the end */
-+  if (spec->multibyte)
-+    {
-+      mbui_iterator_t iter;
-+
-+      for (mbui_init (iter, string); mbui_avail (iter); mbui_advance (iter))
-+        {
-+          /* We know that special contains only ASCII characters.  */
-+          if (mb_len (mbui_cur (iter)) == 1
-+              && strchr (special, * mbui_cur_ptr (iter)))
-+            length += 1;
-+          length += mb_len (mbui_cur (iter));
-+        }
-+    }
-+  else
-+    {
-+      const char *iter;
-+
-+      for (iter = string; *iter != '\0'; iter++)
-+        {
-+          if (strchr (special, *iter))
-+            length += 1;
-+          length += 1;
-+        }
-+    }
-+
-+  return length;
-+}
-+
-+char *
-+regex_quote_copy (char *p, const char *string, const struct regex_quote_spec *spec)
-+{
-+  const char *special = spec->special;
-+
-+  if (spec->anchored)
-+    *p++ = '^';
-+  if (spec->multibyte)
-+    {
-+      mbui_iterator_t iter;
-+
-+      for (mbui_init (iter, string); mbui_avail (iter); mbui_advance (iter))
-+        {
-+          /* We know that special contains only ASCII characters.  */
-+          if (mb_len (mbui_cur (iter)) == 1
-+              && strchr (special, * mbui_cur_ptr (iter)))
-+            *p++ = '\\';
-+          memcpy (p, mbui_cur_ptr (iter), mb_len (mbui_cur (iter)));
-+          p += mb_len (mbui_cur (iter));
-+        }
-+    }
-+  else
-+    {
-+      const char *iter;
-+
-+      for (iter = string; *iter != '\0'; iter++)
-+        {
-+          if (strchr (special, *iter))
-+            *p++ = '\\';
-+          *p++ = *iter++;
-+        }
-+    }
-+  if (spec->anchored)
-+    *p++ = '$';
-+
-+  return p;
-+}
-+
-+char *
-+regex_quote (const char *string, const struct regex_quote_spec *spec)
-+{
-+  size_t length = regex_quote_length (string, spec);
-+  char *result = XNMALLOC (length + 1, char);
-+  char *p;
-+
-+  p = result;
-+  p = regex_quote_copy (p, string, spec);
-+  *p = '\0';
-+  return result;
-+}
---- origsrc/lib/regex-quote.h	1970-01-01 01:00:00.000000000 +0100
-+++ src/lib/regex-quote.h	2013-06-27 18:05:27.112447751 +0200
-@@ -0,0 +1,88 @@
-+/* Construct a regular expression from a literal string.
-+   Copyright (C) 1995, 2010-2013 Free Software Foundation, Inc.
-+   Written by Bruno Haible <haible@clisp.cons.org>, 2010.
-+
-+   This program is free software: you can redistribute it and/or modify
-+   it under the terms of the GNU General Public License as published by
-+   the Free Software Foundation; either version 3 of the License, or
-+   (at your option) any later version.
-+
-+   This program is distributed in the hope that it will be useful,
-+   but WITHOUT ANY WARRANTY; without even the implied warranty of
-+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-+   GNU General Public License for more details.
-+
-+   You should have received a copy of the GNU General Public License
-+   along with this program.  If not, see <http://www.gnu.org/licenses/>.  */
-+
-+#ifndef _REGEX_QUOTE_H
-+#define _REGEX_QUOTE_H
-+
-+#include <stddef.h>
-+#include <stdbool.h>
-+
-+
-+/* Specifies a quotation task for converting a fixed string to a regular
-+   expression pattern.  */
-+struct regex_quote_spec
-+{
-+  /* True if the regular expression pattern consists of multibyte characters
-+     (in the encoding given by the LC_CTYPE category of the locale),
-+     false if it consists of single bytes or UTF-8 characters.  */
-+  unsigned int /*bool*/ multibyte : 1;
-+  /* True if the regular expression pattern shall match only entire lines.  */
-+  unsigned int /*bool*/ anchored : 1;
-+  /* Set of characters that need to be escaped (all ASCII), as a
-+     NUL-terminated string.  */
-+  char special[30 + 1];
-+};
-+
-+
-+/* Creates a quotation task that produces a POSIX regular expression, that is,
-+   a pattern that can be compiled with regcomp().
-+   CFLAGS can be 0 or REG_EXTENDED.
-+   If it is 0, the result is a Basic Regular Expression (BRE)
-+   <http://www.opengroup.org/onlinepubs/9699919799/basedefs/V1_chap09.html#tag_09_03>.
-+   If it is REG_EXTENDED, the result is an Extended Regular Expression (ERE)
-+   <http://www.opengroup.org/onlinepubs/9699919799/basedefs/V1_chap09.html#tag_09_04>.
-+   If ANCHORED is false, the regular expression will match substrings of lines.
-+   If ANCHORED is true, it will match only complete lines,  */
-+extern struct regex_quote_spec
-+       regex_quote_spec_posix (int cflags, bool anchored);
-+
-+/* Creates a quotation task that produces a regular expression that can be
-+   compiled with the GNU API function re_compile_pattern().
-+   SYNTAX describes the syntax of the regular expression (such as
-+   RE_SYNTAX_POSIX_BASIC, RE_SYNTAX_POSIX_EXTENDED, RE_SYNTAX_EMACS, all
-+   defined in <regex.h>).  It must be the same value as 're_syntax_options'
-+   at the moment of the re_compile_pattern() call.
-+   If ANCHORED is false, the regular expression will match substrings of lines.
-+   If ANCHORED is true, it will match only complete lines,  */
-+extern struct regex_quote_spec
-+       regex_quote_spec_gnu (unsigned long /*reg_syntax_t*/ syntax, bool anchored);
-+
-+/* Creates a quotation task that produces a PCRE regular expression, that is,
-+   a pattern that can be compiled with pcre_compile().
-+   OPTIONS is the same value as the second argument passed to pcre_compile().
-+   If ANCHORED is false, the regular expression will match substrings of lines.
-+   If ANCHORED is true, it will match only complete lines,  */
-+extern struct regex_quote_spec
-+       regex_quote_spec_pcre (int options, bool anchored);
-+
-+
-+/* Returns the number of bytes needed for the quoted string.  */
-+extern size_t
-+       regex_quote_length (const char *string, const struct regex_quote_spec *spec);
-+
-+/* Copies the quoted string to p and returns the incremented p.
-+   There must be room for regex_quote_length (string, spec) + 1 bytes at p.  */
-+extern char *
-+       regex_quote_copy (char *p,
-+                         const char *string, const struct regex_quote_spec *spec);
-+
-+/* Returns the freshly allocated quoted string.  */
-+extern char *
-+       regex_quote (const char *string, const struct regex_quote_spec *spec);
-+
-+
-+#endif /* _REGEX_QUOTE_H */
---- origsrc/lib/regex.c	2012-12-22 14:21:52.000000000 +0100
-+++ src/lib/regex.c	2013-06-27 18:05:27.138447639 +0200
-@@ -1,22 +1,21 @@
--/* -*- buffer-read-only: t -*- vi: set ro: */
--/* DO NOT EDIT! GENERATED AUTOMATICALLY! */
- /* Extended regular expression matching and search library.
--   Copyright (C) 2002-2003, 2005-2006, 2009-2012 Free Software Foundation, Inc.
-+   Copyright (C) 2002-2013 Free Software Foundation, Inc.
-    This file is part of the GNU C Library.
-    Contributed by Isamu Hasegawa <isamu@yamato.ibm.com>.
- 
--   This program is free software; you can redistribute it and/or modify
--   it under the terms of the GNU General Public License as published by
--   the Free Software Foundation; either version 3, or (at your option)
--   any later version.
-+   The GNU C Library is free software; you can redistribute it and/or
-+   modify it under the terms of the GNU Lesser General Public
-+   License as published by the Free Software Foundation; either
-+   version 2.1 of the License, or (at your option) any later version.
- 
--   This program is distributed in the hope that it will be useful,
-+   The GNU C Library is distributed in the hope that it will be useful,
-    but WITHOUT ANY WARRANTY; without even the implied warranty of
--   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
--   GNU General Public License for more details.
-+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
-+   Lesser General Public License for more details.
- 
--   You should have received a copy of the GNU General Public License along
--   with this program; if not, see <http://www.gnu.org/licenses/>.  */
-+   You should have received a copy of the GNU Lesser General Public
-+   License along with the GNU C Library; if not, see
-+   <http://www.gnu.org/licenses/>.  */
- 
- #ifndef _LIBC
- # include <config.h>
-@@ -25,6 +24,7 @@
- #  pragma GCC diagnostic ignored "-Wsuggest-attribute=pure"
- # endif
- # if (__GNUC__ == 4 && 3 <= __GNUC_MINOR__) || 4 < __GNUC__
-+#  pragma GCC diagnostic ignored "-Wold-style-definition"
- #  pragma GCC diagnostic ignored "-Wtype-limits"
- # endif
- #endif
---- origsrc/lib/regex.h	2012-12-22 14:21:52.000000000 +0100
-+++ src/lib/regex.h	2013-06-27 18:05:27.168447509 +0200
-@@ -1,23 +1,22 @@
--/* -*- buffer-read-only: t -*- vi: set ro: */
--/* DO NOT EDIT! GENERATED AUTOMATICALLY! */
- /* Definitions for data structures and routines for the regular
-    expression library.
--   Copyright (C) 1985, 1989-1993, 1995-1998, 2000-2003, 2005-2012
--   Free Software Foundation, Inc.
-+   Copyright (C) 1985, 1989-1993, 1995-1998, 2000-2003, 2005-2013 Free Software
-+   Foundation, Inc.
-    This file is part of the GNU C Library.
- 
--   This program is free software; you can redistribute it and/or modify
--   it under the terms of the GNU General Public License as published by
--   the Free Software Foundation; either version 3, or (at your option)
--   any later version.
-+   The GNU C Library is free software; you can redistribute it and/or
-+   modify it under the terms of the GNU Lesser General Public
-+   License as published by the Free Software Foundation; either
-+   version 2.1 of the License, or (at your option) any later version.
- 
--   This program is distributed in the hope that it will be useful,
-+   The GNU C Library is distributed in the hope that it will be useful,
-    but WITHOUT ANY WARRANTY; without even the implied warranty of
--   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
--   GNU General Public License for more details.
-+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
-+   Lesser General Public License for more details.
- 
--   You should have received a copy of the GNU General Public License along
--   with this program; if not, see <http://www.gnu.org/licenses/>.  */
-+   You should have received a copy of the GNU Lesser General Public
-+   License along with the GNU C Library; if not, see
-+   <http://www.gnu.org/licenses/>.  */
- 
- #ifndef _REGEX_H
- #define _REGEX_H 1
---- origsrc/lib/regex_internal.c	2012-12-22 14:21:52.000000000 +0100
-+++ src/lib/regex_internal.c	2013-06-27 18:05:27.199447375 +0200
-@@ -1,22 +1,21 @@
--/* -*- buffer-read-only: t -*- vi: set ro: */
--/* DO NOT EDIT! GENERATED AUTOMATICALLY! */
- /* Extended regular expression matching and search library.
--   Copyright (C) 2002-2012 Free Software Foundation, Inc.
-+   Copyright (C) 2002-2013 Free Software Foundation, Inc.
-    This file is part of the GNU C Library.
-    Contributed by Isamu Hasegawa <isamu@yamato.ibm.com>.
- 
--   This program is free software; you can redistribute it and/or modify
--   it under the terms of the GNU General Public License as published by
--   the Free Software Foundation; either version 3, or (at your option)
--   any later version.
-+   The GNU C Library is free software; you can redistribute it and/or
-+   modify it under the terms of the GNU Lesser General Public
-+   License as published by the Free Software Foundation; either
-+   version 2.1 of the License, or (at your option) any later version.
- 
--   This program is distributed in the hope that it will be useful,
-+   The GNU C Library is distributed in the hope that it will be useful,
-    but WITHOUT ANY WARRANTY; without even the implied warranty of
--   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
--   GNU General Public License for more details.
-+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
-+   Lesser General Public License for more details.
- 
--   You should have received a copy of the GNU General Public License along
--   with this program; if not, see <http://www.gnu.org/licenses/>.  */
-+   You should have received a copy of the GNU Lesser General Public
-+   License along with the GNU C Library; if not, see
-+   <http://www.gnu.org/licenses/>.  */
- 
- static void re_string_construct_common (const char *str, Idx len,
- 					re_string_t *pstr,
-@@ -835,7 +834,7 @@ re_string_reconstruct (re_string_t *pstr
- }
- 
- static unsigned char
--internal_function __attribute ((pure))
-+internal_function __attribute__ ((pure))
- re_string_peek_byte_case (const re_string_t *pstr, Idx idx)
- {
-   int ch;
-@@ -975,7 +974,7 @@ re_node_set_alloc (re_node_set *set, Idx
-   set->alloc = size;
-   set->nelem = 0;
-   set->elems = re_malloc (Idx, size);
--  if (BE (set->elems == NULL, 0))
-+  if (BE (set->elems == NULL, 0) && (MALLOC_0_IS_NONNULL || size != 0))
-     return REG_ESPACE;
-   return REG_NOERROR;
- }
-@@ -1355,7 +1354,7 @@ re_node_set_insert_last (re_node_set *se
-    Return true if SET1 and SET2 are equivalent.  */
- 
- static bool
--internal_function __attribute ((pure))
-+internal_function __attribute__ ((pure))
- re_node_set_compare (const re_node_set *set1, const re_node_set *set2)
- {
-   Idx i;
-@@ -1370,7 +1369,7 @@ re_node_set_compare (const re_node_set *
- /* Return (idx + 1) if SET contains the element ELEM, return 0 otherwise.  */
- 
- static Idx
--internal_function __attribute ((pure))
-+internal_function __attribute__ ((pure))
- re_node_set_contains (const re_node_set *set, Idx elem)
- {
-   __re_size_t idx, right, mid;
-@@ -1444,11 +1443,9 @@ re_dfa_add_node (re_dfa_t *dfa, re_token
-   dfa->nodes[dfa->nodes_len] = token;
-   dfa->nodes[dfa->nodes_len].constraint = 0;
- #ifdef RE_ENABLE_I18N
--  {
--  int type = token.type;
-   dfa->nodes[dfa->nodes_len].accept_mb =
--    (type == OP_PERIOD && dfa->mb_cur_max > 1) || type == COMPLEX_BRACKET;
--  }
-+    ((token.type == OP_PERIOD && dfa->mb_cur_max > 1)
-+     || token.type == COMPLEX_BRACKET);
- #endif
-   dfa->nexts[dfa->nodes_len] = REG_MISSING;
-   re_node_set_init_empty (dfa->edests + dfa->nodes_len);
---- origsrc/lib/regex_internal.h	2012-12-22 14:21:52.000000000 +0100
-+++ src/lib/regex_internal.h	2013-06-27 18:05:27.230447242 +0200
-@@ -1,22 +1,21 @@
--/* -*- buffer-read-only: t -*- vi: set ro: */
--/* DO NOT EDIT! GENERATED AUTOMATICALLY! */
- /* Extended regular expression matching and search library.
--   Copyright (C) 2002-2012 Free Software Foundation, Inc.
-+   Copyright (C) 2002-2013 Free Software Foundation, Inc.
-    This file is part of the GNU C Library.
-    Contributed by Isamu Hasegawa <isamu@yamato.ibm.com>.
- 
--   This program is free software; you can redistribute it and/or modify
--   it under the terms of the GNU General Public License as published by
--   the Free Software Foundation; either version 3, or (at your option)
--   any later version.
-+   The GNU C Library is free software; you can redistribute it and/or
-+   modify it under the terms of the GNU Lesser General Public
-+   License as published by the Free Software Foundation; either
-+   version 2.1 of the License, or (at your option) any later version.
- 
--   This program is distributed in the hope that it will be useful,
-+   The GNU C Library is distributed in the hope that it will be useful,
-    but WITHOUT ANY WARRANTY; without even the implied warranty of
--   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
--   GNU General Public License for more details.
-+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
-+   Lesser General Public License for more details.
- 
--   You should have received a copy of the GNU General Public License along
--   with this program; if not, see <http://www.gnu.org/licenses/>.  */
-+   You should have received a copy of the GNU Lesser General Public
-+   License along with the GNU C Library; if not, see
-+   <http://www.gnu.org/licenses/>.  */
- 
- #ifndef _REGEX_INTERNAL_H
- #define _REGEX_INTERNAL_H 1
-@@ -28,21 +27,54 @@
- #include <string.h>
- 
- #include <langinfo.h>
--#ifndef _LIBC
--# include "localcharset.h"
--#endif
- #include <locale.h>
- #include <wchar.h>
- #include <wctype.h>
- #include <stdbool.h>
- #include <stdint.h>
--#if defined _LIBC
-+
-+#ifdef _LIBC
- # include <bits/libc-lock.h>
-+# define lock_define(name) __libc_lock_define (, name)
-+# define lock_init(lock) (__libc_lock_init (lock), 0)
-+# define lock_fini(lock) 0
-+# define lock_lock(lock) __libc_lock_lock (lock)
-+# define lock_unlock(lock) __libc_lock_unlock (lock)
-+#elif defined GNULIB_LOCK
-+# include "glthread/lock.h"
-+  /* Use gl_lock_define if empty macro arguments are known to work.
-+     Otherwise, fall back on less-portable substitutes.  */
-+# if ((defined __GNUC__ && !defined __STRICT_ANSI__) \
-+      || (defined __STDC_VERSION__ && 199901L <= __STDC_VERSION__))
-+#  define lock_define(name) gl_lock_define (, name)
-+# elif USE_POSIX_THREADS
-+#  define lock_define(name) pthread_mutex_t name;
-+# elif USE_PTH_THREADS
-+#  define lock_define(name) pth_mutex_t name;
-+# elif USE_SOLARIS_THREADS
-+#  define lock_define(name) mutex_t name;
-+# elif USE_WINDOWS_THREADS
-+#  define lock_define(name) gl_lock_t name;
-+# else
-+#  define lock_define(name)
-+# endif
-+# define lock_init(lock) glthread_lock_init (&(lock))
-+# define lock_fini(lock) glthread_lock_destroy (&(lock))
-+# define lock_lock(lock) glthread_lock_lock (&(lock))
-+# define lock_unlock(lock) glthread_lock_unlock (&(lock))
-+#elif defined GNULIB_PTHREAD
-+# include <pthread.h>
-+# define lock_define(name) pthread_mutex_t name;
-+# define lock_init(lock) pthread_mutex_init (&(lock), 0)
-+# define lock_fini(lock) pthread_mutex_destroy (&(lock))
-+# define lock_lock(lock) pthread_mutex_lock (&(lock))
-+# define lock_unlock(lock) pthread_mutex_unlock (&(lock))
- #else
--# define __libc_lock_define(CLASS,NAME)
--# define __libc_lock_init(NAME) do { } while (0)
--# define __libc_lock_lock(NAME) do { } while (0)
--# define __libc_lock_unlock(NAME) do { } while (0)
-+# define lock_define(name)
-+# define lock_init(lock) 0
-+# define lock_fini(lock) 0
-+# define lock_lock(lock) ((void) 0)
-+# define lock_unlock(lock) ((void) 0)
- #endif
- 
- /* In case that the system doesn't have isblank().  */
-@@ -65,7 +97,7 @@
- # ifdef _LIBC
- #  undef gettext
- #  define gettext(msgid) \
--  INTUSE(__dcgettext) (_libc_intl_domainname, msgid, LC_MESSAGES)
-+  __dcgettext (_libc_intl_domainname, msgid, LC_MESSAGES)
- # endif
- #else
- # define gettext(msgid) (msgid)
-@@ -101,6 +133,8 @@
- 
- /* Rename to standard API for using out of glibc.  */
- #ifndef _LIBC
-+# undef __wctype
-+# undef __iswctype
- # define __wctype wctype
- # define __iswctype iswctype
- # define __btowc btowc
-@@ -110,10 +144,8 @@
- # define attribute_hidden
- #endif /* not _LIBC */
- 
--#if __GNUC__ >= 4 || (__GNUC__ == 3 && __GNUC_MINOR__ >= 1)
--# define __attribute(arg) __attribute__ (arg)
--#else
--# define __attribute(arg)
-+#if __GNUC__ < 3 + (__GNUC_MINOR__ < 1)
-+# define __attribute__(arg)
- #endif
- 
- typedef __re_idx_t Idx;
-@@ -429,7 +461,7 @@ static void build_upper_buffer (re_strin
- static void re_string_translate_buffer (re_string_t *pstr) internal_function;
- static unsigned int re_string_context_at (const re_string_t *input, Idx idx,
- 					  int eflags)
--     internal_function __attribute ((pure));
-+     internal_function __attribute__ ((pure));
- #endif
- #define re_string_peek_byte(pstr, offset) \
-   ((pstr)->mbs[(pstr)->cur_idx + offset])
-@@ -448,7 +480,9 @@ static unsigned int re_string_context_at
- #define re_string_skip_bytes(pstr,idx) ((pstr)->cur_idx += (idx))
- #define re_string_set_index(pstr,idx) ((pstr)->cur_idx = (idx))
- 
--#include <alloca.h>
-+#if defined _LIBC || HAVE_ALLOCA
-+# include <alloca.h>
-+#endif
- 
- #ifndef _LIBC
- # if HAVE_ALLOCA
-@@ -465,6 +499,12 @@ static unsigned int re_string_context_at
- # endif
- #endif
- 
-+#ifdef _LIBC
-+# define MALLOC_0_IS_NONNULL 1
-+#elif !defined MALLOC_0_IS_NONNULL
-+# define MALLOC_0_IS_NONNULL 0
-+#endif
-+
- #ifndef MAX
- # define MAX(a,b) ((a) < (b) ? (b) : (a))
- #endif
-@@ -695,7 +735,7 @@ struct re_dfa_t
- #ifdef DEBUG
-   char* re_str;
- #endif
--  __libc_lock_define (, lock)
-+  lock_define (lock)
- };
- 
- #define re_node_set_init_empty(set) memset (set, '\0', sizeof (re_node_set))
-@@ -767,7 +807,7 @@ bitset_copy (bitset_t dest, const bitset
-   memcpy (dest, src, sizeof (bitset_t));
- }
- 
--static void
-+static void __attribute__ ((unused))
- bitset_not (bitset_t set)
- {
-   int bitset_i;
-@@ -779,7 +819,7 @@ bitset_not (bitset_t set)
-        & ~set[BITSET_WORDS - 1]);
- }
- 
--static void
-+static void __attribute__ ((unused))
- bitset_merge (bitset_t dest, const bitset_t src)
- {
-   int bitset_i;
-@@ -787,7 +827,7 @@ bitset_merge (bitset_t dest, const bitse
-     dest[bitset_i] |= src[bitset_i];
- }
- 
--static void
-+static void __attribute__ ((unused))
- bitset_mask (bitset_t dest, const bitset_t src)
- {
-   int bitset_i;
-@@ -798,7 +838,7 @@ bitset_mask (bitset_t dest, const bitset
- #ifdef RE_ENABLE_I18N
- /* Functions for re_string.  */
- static int
--internal_function __attribute ((pure))
-+internal_function __attribute__ ((pure, unused))
- re_string_char_size_at (const re_string_t *pstr, Idx idx)
- {
-   int byte_idx;
-@@ -811,7 +851,7 @@ re_string_char_size_at (const re_string_
- }
- 
- static wint_t
--internal_function __attribute ((pure))
-+internal_function __attribute__ ((pure, unused))
- re_string_wchar_at (const re_string_t *pstr, Idx idx)
- {
-   if (pstr->mb_cur_max == 1)
-@@ -821,7 +861,7 @@ re_string_wchar_at (const re_string_t *p
- 
- # ifndef NOT_IN_libc
- static int
--internal_function __attribute ((pure))
-+internal_function __attribute__ ((pure, unused))
- re_string_elem_size_at (const re_string_t *pstr, Idx idx)
- {
- #  ifdef _LIBC
---- origsrc/lib/regexec.c	2012-12-22 14:21:52.000000000 +0100
-+++ src/lib/regexec.c	2013-06-27 18:05:27.268447078 +0200
-@@ -1,22 +1,21 @@
--/* -*- buffer-read-only: t -*- vi: set ro: */
--/* DO NOT EDIT! GENERATED AUTOMATICALLY! */
- /* Extended regular expression matching and search library.
--   Copyright (C) 2002-2012 Free Software Foundation, Inc.
-+   Copyright (C) 2002-2013 Free Software Foundation, Inc.
-    This file is part of the GNU C Library.
-    Contributed by Isamu Hasegawa <isamu@yamato.ibm.com>.
- 
--   This program is free software; you can redistribute it and/or modify
--   it under the terms of the GNU General Public License as published by
--   the Free Software Foundation; either version 3, or (at your option)
--   any later version.
-+   The GNU C Library is free software; you can redistribute it and/or
-+   modify it under the terms of the GNU Lesser General Public
-+   License as published by the Free Software Foundation; either
-+   version 2.1 of the License, or (at your option) any later version.
- 
--   This program is distributed in the hope that it will be useful,
-+   The GNU C Library is distributed in the hope that it will be useful,
-    but WITHOUT ANY WARRANTY; without even the implied warranty of
--   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
--   GNU General Public License for more details.
-+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
-+   Lesser General Public License for more details.
- 
--   You should have received a copy of the GNU General Public License along
--   with this program; if not, see <http://www.gnu.org/licenses/>.  */
-+   You should have received a copy of the GNU Lesser General Public
-+   License along with the GNU C Library; if not, see
-+   <http://www.gnu.org/licenses/>.  */
- 
- static reg_errcode_t match_ctx_init (re_match_context_t *cache, int eflags,
- 				     Idx n) internal_function;
-@@ -200,7 +199,7 @@ static Idx group_nodes_into_DFAstates (c
- static bool check_node_accept (const re_match_context_t *mctx,
- 			       const re_token_t *node, Idx idx)
-      internal_function;
--static reg_errcode_t extend_buffers (re_match_context_t *mctx)
-+static reg_errcode_t extend_buffers (re_match_context_t *mctx, int min_len)
-      internal_function;
- 
- /* Entry point for POSIX code.  */
-@@ -229,9 +228,7 @@ regexec (preg, string, nmatch, pmatch, e
- {
-   reg_errcode_t err;
-   Idx start, length;
--#ifdef _LIBC
-   re_dfa_t *dfa = preg->buffer;
--#endif
- 
-   if (eflags & ~(REG_NOTBOL | REG_NOTEOL | REG_STARTEND))
-     return REG_BADPAT;
-@@ -247,14 +244,14 @@ regexec (preg, string, nmatch, pmatch, e
-       length = strlen (string);
-     }
- 
--  __libc_lock_lock (dfa->lock);
-+  lock_lock (dfa->lock);
-   if (preg->no_sub)
-     err = re_search_internal (preg, string, length, start, length,
- 			      length, 0, NULL, eflags);
-   else
-     err = re_search_internal (preg, string, length, start, length,
- 			      length, nmatch, pmatch, eflags);
--  __libc_lock_unlock (dfa->lock);
-+  lock_unlock (dfa->lock);
-   return err != REG_NOERROR;
- }
- 
-@@ -422,9 +419,7 @@ re_search_stub (struct re_pattern_buffer
-   Idx nregs;
-   regoff_t rval;
-   int eflags = 0;
--#ifdef _LIBC
-   re_dfa_t *dfa = bufp->buffer;
--#endif
-   Idx last_start = start + range;
- 
-   /* Check for out-of-range.  */
-@@ -435,7 +430,7 @@ re_search_stub (struct re_pattern_buffer
-   else if (BE (last_start < 0 || (range < 0 && start <= last_start), 0))
-     last_start = 0;
- 
--  __libc_lock_lock (dfa->lock);
-+  lock_lock (dfa->lock);
- 
-   eflags |= (bufp->not_bol) ? REG_NOTBOL : 0;
-   eflags |= (bufp->not_eol) ? REG_NOTEOL : 0;
-@@ -499,7 +494,7 @@ re_search_stub (struct re_pattern_buffer
-     }
-   re_free (pmatch);
-  out:
--  __libc_lock_unlock (dfa->lock);
-+  lock_unlock (dfa->lock);
-   return rval;
- }
- 
-@@ -1065,7 +1060,7 @@ prune_impossible_nodes (re_match_context
-    since initial states may have constraints like "\<", "^", etc..  */
- 
- static inline re_dfastate_t *
--__attribute ((always_inline)) internal_function
-+__attribute__ ((always_inline)) internal_function
- acquire_init_state_context (reg_errcode_t *err, const re_match_context_t *mctx,
- 			    Idx idx)
- {
-@@ -1177,7 +1172,7 @@ check_matching (re_match_context_t *mctx
- 	  || (BE (next_char_idx >= mctx->input.valid_len, 0)
- 	      && mctx->input.valid_len < mctx->input.len))
- 	{
--	  err = extend_buffers (mctx);
-+	  err = extend_buffers (mctx, next_char_idx + 1);
- 	  if (BE (err != REG_NOERROR, 0))
- 	    {
- 	      assert (err == REG_ESPACE);
-@@ -1757,7 +1752,7 @@ clean_state_log_if_needed (re_match_cont
- 	  && mctx->input.valid_len < mctx->input.len))
-     {
-       reg_errcode_t err;
--      err = extend_buffers (mctx);
-+      err = extend_buffers (mctx, next_state_log_idx + 1);
-       if (BE (err != REG_NOERROR, 0))
- 	return err;
-     }
-@@ -2814,7 +2809,7 @@ get_subexp (re_match_context_t *mctx, Id
- 		  if (bkref_str_off >= mctx->input.len)
- 		    break;
- 
--		  err = extend_buffers (mctx);
-+		  err = extend_buffers (mctx, bkref_str_off + 1);
- 		  if (BE (err != REG_NOERROR, 0))
- 		    return err;
- 
-@@ -3937,6 +3932,7 @@ check_node_accept_bytes (const re_dfa_t
- 		in_collseq = find_collation_sequence_value (pin, elem_len);
- 	    }
- 	  /* match with range expression?  */
-+	  /* FIXME: Implement rational ranges here, too.  */
- 	  for (i = 0; i < cset->nranges; ++i)
- 	    if (cset->range_starts[i] <= in_collseq
- 		&& in_collseq <= cset->range_ends[i])
-@@ -3988,18 +3984,9 @@ check_node_accept_bytes (const re_dfa_t
- # endif /* _LIBC */
- 	{
- 	  /* match with range expression?  */
--#if __GNUC__ >= 2 && ! (__STDC_VERSION__ < 199901L && defined __STRICT_ANSI__)
--	  wchar_t cmp_buf[] = {L'\0', L'\0', wc, L'\0', L'\0', L'\0'};
--#else
--	  wchar_t cmp_buf[] = {L'\0', L'\0', L'\0', L'\0', L'\0', L'\0'};
--	  cmp_buf[2] = wc;
--#endif
- 	  for (i = 0; i < cset->nranges; ++i)
- 	    {
--	      cmp_buf[0] = cset->range_starts[i];
--	      cmp_buf[4] = cset->range_ends[i];
--	      if (wcscoll (cmp_buf, cmp_buf + 2) <= 0
--		  && wcscoll (cmp_buf + 2, cmp_buf + 4) <= 0)
-+	      if (cset->range_starts[i] <= wc && wc <= cset->range_ends[i])
- 		{
- 		  match_len = char_len;
- 		  goto check_node_accept_bytes_match;
-@@ -4137,7 +4124,7 @@ check_node_accept (const re_match_contex
- 
- static reg_errcode_t
- internal_function __attribute_warn_unused_result__
--extend_buffers (re_match_context_t *mctx)
-+extend_buffers (re_match_context_t *mctx, int min_len)
- {
-   reg_errcode_t ret;
-   re_string_t *pstr = &mctx->input;
-@@ -4147,8 +4134,10 @@ extend_buffers (re_match_context_t *mctx
-           <= pstr->bufs_len, 0))
-     return REG_ESPACE;
- 
--  /* Double the lengths of the buffers.  */
--  ret = re_string_realloc_buffers (pstr, MIN (pstr->len, pstr->bufs_len * 2));
-+  /* Double the lengths of the buffers, but allocate at least MIN_LEN.  */
-+  ret = re_string_realloc_buffers (pstr,
-+				   MAX (min_len,
-+					MIN (pstr->len, pstr->bufs_len * 2)));
-   if (BE (ret != REG_NOERROR, 0))
-     return ret;
- 
---- origsrc/sed/sed.c	2012-03-16 10:13:31.000000000 +0100
-+++ src/sed/sed.c	2013-06-27 18:06:25.592195456 +0200
-@@ -57,7 +57,11 @@ bool follow_symlinks = false;
- char *in_place_extension = NULL;
- 
- /* The mode to use to read/write files, either "r"/"w" or "rb"/"wb".  */
-+#ifdef HAVE_FOPEN_RT
-+char *read_mode = "rt";
-+#else
- char *read_mode = "r";
-+#endif
- char *write_mode = "w";
- 
- /* Do we need to be pedantically POSIX compliant? */