diff options
Diffstat (limited to 'dev')
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 (®exp, 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 (®exp); -+ 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 (®exp, 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 (®exp); -+ 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? */ |