diff options
73 files changed, 3606 insertions, 486 deletions
diff --git a/Makefile.ci b/Makefile.ci index 3be90c0a3..c8bc09fdc 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -24,4 +24,4 @@ CI_TARGETS=ci-all \ # Generic rule, we use make to easy travis integraton with mixed rules $(CI_TARGETS): ci-%: - ./dev/ci/ci-$*.sh + +./dev/ci/ci-$*.sh @@ -3,7 +3,7 @@ ## This micro-configure shell script is here only to ## launch the real configuration via ocaml -cmd=ocaml +ocaml=ocaml script=./configure.ml if [ ! -f $script ]; then @@ -16,17 +16,18 @@ fi ## Parse the args, only looking for -camldir ## We avoid using shift to keep "$@" intact +cmd=$ocaml last= for i; do case $last in - -camldir|--camldir) cmd="$i/ocaml"; break;; + -camldir) cmd="$i/$ocaml"; break;; esac last=$i done ## We check that $cmd is ok before the real exec $cmd -`$cmd -version > /dev/null 2>&1` && exec $cmd $script "$@" +`$cmd -version > /dev/null 2>&1` && exec $cmd -w "-3" $script "$@" ## If we're still here, something is wrong with $cmd diff --git a/configure.ml b/configure.ml index 549b32772..c75c3d7e1 100644 --- a/configure.ml +++ b/configure.ml @@ -364,6 +364,8 @@ let args_options = Arg.align [ " Force OCaml version"; "-warn-error", Arg.Set Prefs.warn_error, " Make OCaml warnings into errors"; + "-camldir", Arg.String (fun _ -> ()), + "<dir> Specifies path to 'ocaml' for running configure script"; ] let parse_args () = diff --git a/dev/build/windows/MakeCoq_84pl6_abs_ocaml.bat b/dev/build/windows/MakeCoq_84pl6_abs_ocaml.bat index bdcb01db9..9dbce1920 100644 --- a/dev/build/windows/MakeCoq_84pl6_abs_ocaml.bat +++ b/dev/build/windows/MakeCoq_84pl6_abs_ocaml.bat @@ -1,3 +1,16 @@ +@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 ^
@@ -6,5 +19,10 @@ call MakeCoq_MinGW.bat ^ -ocaml=Y ^
-make=Y ^
-coqver=8.4pl6 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_84pl6_abs ^
- -destcoq=%ROOTPATH%\coq64_84pl6_abs
+ -destcyg="%ROOTPATH%\cygwin_coq64_84pl6_abs" ^
+ -destcoq="%ROOTPATH%\coq64_84pl6_abs"
+
+IF %ERRORLEVEL% NEQ 0 (
+ ECHO MakeCoq_84pl6_abs_ocaml.bat failed with error code %ERRORLEVEL%
+ EXIT /b %ERRORLEVEL%
+)
diff --git a/dev/build/windows/MakeCoq_85pl2_abs_ocaml.bat b/dev/build/windows/MakeCoq_85pl2_abs_ocaml.bat index 2e4a692e9..7faf3e9ce 100644 --- a/dev/build/windows/MakeCoq_85pl2_abs_ocaml.bat +++ b/dev/build/windows/MakeCoq_85pl2_abs_ocaml.bat @@ -1,3 +1,16 @@ +@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 ^
@@ -6,5 +19,10 @@ call MakeCoq_MinGW.bat ^ -ocaml=Y ^
-make=Y ^
-coqver=8.5pl2 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_85pl2_abs ^
- -destcoq=%ROOTPATH%\coq64_85pl2_abs
+ -destcyg="%ROOTPATH%\cygwin_coq64_85pl2_abs" ^
+ -destcoq="%ROOTPATH%\coq64_85pl2_abs"
+
+IF %ERRORLEVEL% NEQ 0 (
+ ECHO MakeCoq_85pl2_abs_ocaml.bat failed with error code %ERRORLEVEL%
+ EXIT /b %ERRORLEVEL%
+)
diff --git a/dev/build/windows/MakeCoq_85pl3_abs_ocaml.bat b/dev/build/windows/MakeCoq_85pl3_abs_ocaml.bat index 6e4e440a2..b719b14c5 100644 --- a/dev/build/windows/MakeCoq_85pl3_abs_ocaml.bat +++ b/dev/build/windows/MakeCoq_85pl3_abs_ocaml.bat @@ -1,3 +1,16 @@ +@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 ^
@@ -6,5 +19,10 @@ call MakeCoq_MinGW.bat ^ -ocaml=Y ^
-make=Y ^
-coqver=8.5pl3 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_85pl3_abs ^
- -destcoq=%ROOTPATH%\coq64_85pl3_abs
+ -destcyg="%ROOTPATH%\cygwin_coq64_85pl3_abs" ^
+ -destcoq="%ROOTPATH%\coq64_85pl3_abs"
+
+IF %ERRORLEVEL% NEQ 0 (
+ ECHO MakeCoq_85pl3_abs_ocaml.bat failed with error code %ERRORLEVEL%
+ EXIT /b %ERRORLEVEL%
+)
diff --git a/dev/build/windows/MakeCoq_85pl3_installer.bat b/dev/build/windows/MakeCoq_85pl3_installer.bat index c305e2f52..a9f4e2da2 100644 --- a/dev/build/windows/MakeCoq_85pl3_installer.bat +++ b/dev/build/windows/MakeCoq_85pl3_installer.bat @@ -1,8 +1,26 @@ +@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=8.5pl3 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_85pl3_inst ^
- -destcoq=%ROOTPATH%\coq64_85pl3_inst
+ -destcyg="%ROOTPATH%\cygwin_coq64_85pl3_inst" ^
+ -destcoq="%ROOTPATH%\coq64_85pl3_inst"
+
+IF %ERRORLEVEL% NEQ 0 (
+ ECHO MakeCoq_85pl3_installer.bat failed with error code %ERRORLEVEL%
+ EXIT /b %ERRORLEVEL%
+)
diff --git a/dev/build/windows/MakeCoq_85pl3_installer_32.bat b/dev/build/windows/MakeCoq_85pl3_installer_32.bat index d87ff5919..ef593cc63 100644 --- a/dev/build/windows/MakeCoq_85pl3_installer_32.bat +++ b/dev/build/windows/MakeCoq_85pl3_installer_32.bat @@ -1,8 +1,26 @@ +@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=32 ^
-installer=Y ^
-coqver=8.5pl3 ^
- -destcyg=%ROOTPATH%\cygwin_coq32_85pl3_inst ^
- -destcoq=%ROOTPATH%\coq32_85pl3_inst
+ -destcyg="%ROOTPATH%\cygwin_coq32_85pl3_inst" ^
+ -destcoq="%ROOTPATH%\coq32_85pl3_inst"
+
+IF %ERRORLEVEL% NEQ 0 (
+ ECHO MakeCoq_85pl3_installer_32.bat failed with error code %ERRORLEVEL%
+ EXIT /b %ERRORLEVEL%
+)
diff --git a/dev/build/windows/MakeCoq_86git_abs_ocaml.bat b/dev/build/windows/MakeCoq_86git_abs_ocaml.bat index f1d855a02..99a1f156b 100644 --- a/dev/build/windows/MakeCoq_86git_abs_ocaml.bat +++ b/dev/build/windows/MakeCoq_86git_abs_ocaml.bat @@ -1,3 +1,16 @@ +@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 ^
@@ -6,5 +19,10 @@ call MakeCoq_MinGW.bat ^ -ocaml=Y ^
-make=Y ^
-coqver=git-v8.6 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_86git_abs ^
- -destcoq=%ROOTPATH%\coq64_86git_abs
+ -destcyg="%ROOTPATH%\cygwin_coq64_86git_abs" ^
+ -destcoq="%ROOTPATH%\coq64_86git_abs"
+
+IF %ERRORLEVEL% NEQ 0 (
+ ECHO MakeCoq_86git_abs_ocaml.bat failed with error code %ERRORLEVEL%
+ EXIT /b %ERRORLEVEL%
+)
diff --git a/dev/build/windows/MakeCoq_86git_abs_ocaml_gtksrc.bat b/dev/build/windows/MakeCoq_86git_abs_ocaml_gtksrc.bat index 70ab42bc3..896d1cd63 100644 --- a/dev/build/windows/MakeCoq_86git_abs_ocaml_gtksrc.bat +++ b/dev/build/windows/MakeCoq_86git_abs_ocaml_gtksrc.bat @@ -1,3 +1,16 @@ +@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 ^
@@ -7,5 +20,10 @@ call MakeCoq_MinGW.bat ^ -make=Y ^
-gtksrc=Y ^
-coqver=git-v8.6 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_86git_abs_gtksrc ^
- -destcoq=%ROOTPATH%\coq64_86git_abs_gtksrc
+ -destcyg="%ROOTPATH%\cygwin_coq64_86git_abs_gtksrc" ^
+ -destcoq="%ROOTPATH%\coq64_86git_abs_gtksrc"
+
+IF %ERRORLEVEL% NEQ 0 (
+ ECHO MakeCoq_86git_abs_ocaml_gtksrc.bat failed with error code %ERRORLEVEL%
+ EXIT /b %ERRORLEVEL%
+)
diff --git a/dev/build/windows/MakeCoq_86git_installer.bat b/dev/build/windows/MakeCoq_86git_installer.bat index 40506318e..c4823103f 100644 --- a/dev/build/windows/MakeCoq_86git_installer.bat +++ b/dev/build/windows/MakeCoq_86git_installer.bat @@ -1,8 +1,26 @@ +@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_86git_inst ^
- -destcoq=%ROOTPATH%\coq64_86git_inst
+ -destcyg="%ROOTPATH%\cygwin_coq64_86git_inst" ^
+ -destcoq="%ROOTPATH%\coq64_86git_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_86git_installer_32.bat b/dev/build/windows/MakeCoq_86git_installer_32.bat index b9127c945..19146c96c 100644 --- a/dev/build/windows/MakeCoq_86git_installer_32.bat +++ b/dev/build/windows/MakeCoq_86git_installer_32.bat @@ -1,8 +1,26 @@ +@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=32 ^
-installer=Y ^
-coqver=git-v8.6 ^
- -destcyg=%ROOTPATH%\cygwin_coq32_86git_inst ^
- -destcoq=%ROOTPATH%\coq32_86git_inst
+ -destcyg="%ROOTPATH%\cygwin_coq32_86git_inst" ^
+ -destcoq="%ROOTPATH%\coq32_86git_inst"
+
+IF %ERRORLEVEL% NEQ 0 (
+ ECHO MakeCoq_86git_installer_32.bat failed with error code %ERRORLEVEL%
+ EXIT /b %ERRORLEVEL%
+)
diff --git a/dev/build/windows/MakeCoq_86git_installer_cyglocal.bat b/dev/build/windows/MakeCoq_86git_installer_cyglocal.bat new file mode 100755 index 000000000..cf6cafaa0 --- /dev/null +++ b/dev/build/windows/MakeCoq_86git_installer_cyglocal.bat @@ -0,0 +1,27 @@ +@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 ^
+ -cyglocal=Y ^
+ -destcyg="%ROOTPATH%\cygwin_coq64_86git_inst_cyglocal" ^
+ -destcoq="%ROOTPATH%\coq64_86git_inst_cyglocal"
+
+IF %ERRORLEVEL% NEQ 0 (
+ ECHO MakeCoq_86git_installer_cyglocal.bat failed with error code %ERRORLEVEL%
+ EXIT /b %ERRORLEVEL%
+)
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index 1e08cc5a3..b2efe2ddd 100644 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -18,7 +18,7 @@ REM ========== DEFAULT VALUES FOR PARAMETERS ========== REM For a description of all parameters, see ReadMe.txt -SET BATCHFILE=%0 +SET BATCHFILE=%~0 SET BATCHDIR=%~dp0 REM see -arch in ReadMe.txt, but values are x86_64 or i686 (not 64 or 32) @@ -47,9 +47,11 @@ SET SETUP=setup-x86_64.exe REM see -proxy in ReadMe.txt IF DEFINED HTTP_PROXY ( - SET PROXY="%HTTP_PROXY:http://=%" + SET PROXY=%HTTP_PROXY:http://=% ) else ( - SET PROXY="" + 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 @@ -82,12 +84,12 @@ SHIFT :Parse -IF "%0" == "-arch" ( - IF "%1" == "32" ( +IF "%~0" == "-arch" ( + IF "%~1" == "32" ( SET ARCH=i686 SET SETUP=setup-x86.exe ) ELSE ( - IF "%1" == "64" ( + IF "%~1" == "64" ( SET ARCH=x86_64 SET SETUP=setup-x86_64.exe ) ELSE ( @@ -100,15 +102,15 @@ IF "%0" == "-arch" ( GOTO Parse ) -IF "%0" == "-mode" ( - IF "%1" == "mingwincygwin" ( - SET INSTALLMODE=%1 +IF "%~0" == "-mode" ( + IF "%~1" == "mingwincygwin" ( + SET INSTALLMODE=%~1 ) ELSE ( - IF "%1" == "absolute" ( - SET INSTALLMODE=%1 + IF "%~1" == "absolute" ( + SET INSTALLMODE=%~1 ) ELSE ( - IF "%1" == "relocatable" ( - SET INSTALLMODE=%1 + IF "%~1" == "relocatable" ( + SET INSTALLMODE=%~1 ) ELSE ( ECHO "Invalid -mode, valid are mingwincygwin, absolute and relocatable" GOTO :EOF @@ -120,118 +122,124 @@ IF "%0" == "-mode" ( GOTO Parse ) -IF "%0" == "-installer" ( - SET MAKEINSTALLER=%1 +IF "%~0" == "-installer" ( + SET MAKEINSTALLER=%~1 + CALL :CheckYN -installer %~1 || GOTO ErrorExit SHIFT SHIFT GOTO Parse ) -IF "%0" == "-ocaml" ( - SET INSTALLOCAML=%1 +IF "%~0" == "-ocaml" ( + SET INSTALLOCAML=%~1 + CALL :CheckYN -installer %~1 || GOTO ErrorExit SHIFT SHIFT GOTO Parse ) -IF "%0" == "-make" ( - SET INSTALLMAKE=%1 +IF "%~0" == "-make" ( + SET INSTALLMAKE=%~1 + CALL :CheckYN -installer %~1 || GOTO ErrorExit SHIFT SHIFT GOTO Parse ) -IF "%0" == "-destcyg" ( - SET DESTCYG=%1 +IF "%~0" == "-destcyg" ( + SET DESTCYG=%~1 SHIFT SHIFT GOTO Parse ) -IF "%0" == "-destcoq" ( - SET DESTCOQ=%1 +IF "%~0" == "-destcoq" ( + SET DESTCOQ=%~1 SHIFT SHIFT GOTO Parse ) -IF "%0" == "-setup" ( - SET SETUP=%1 +IF "%~0" == "-setup" ( + SET SETUP=%~1 SHIFT SHIFT GOTO Parse ) -IF "%0" == "-proxy" ( - SET PROXY="%1" +IF "%~0" == "-proxy" ( + SET PROXY=%~1 SHIFT SHIFT GOTO Parse ) -IF "%0" == "-cygrepo" ( - SET CYGWIN_REPOSITORY="%1" +IF "%~0" == "-cygrepo" ( + SET CYGWIN_REPOSITORY=%~1 SHIFT SHIFT GOTO Parse ) -IF "%0" == "-cygcache" ( - SET CYGWIN_LOCAL_CACHE_WFMT="%1" +IF "%~0" == "-cygcache" ( + SET CYGWIN_LOCAL_CACHE_WFMT=%~1 SHIFT SHIFT GOTO Parse ) -IF "%0" == "-cyglocal" ( - SET CYGWIN_FROM_CACHE=%1 +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 +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" +IF "%~0" == "-srccache" ( + SET SOURCE_LOCAL_CACHE_WFMT=%~1 SHIFT SHIFT GOTO Parse ) -IF "%0" == "-coqver" ( - SET COQ_VERSION=%1 +IF "%~0" == "-coqver" ( + SET COQ_VERSION=%~1 SHIFT SHIFT GOTO Parse ) -IF "%0" == "-gtksrc" ( - SET GTK_FROM_SOURCES=%1 +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 +IF "%~0" == "-threads" ( + SET MAKE_THREADS=%~1 SHIFT SHIFT GOTO Parse ) -IF NOT "%0" == "" ( +IF NOT "%~0" == "" ( ECHO Install cygwin and download, compile and install OCaml and Coq for MinGW - ECHO !!! Illegal parameter %0 + ECHO !!! Illegal parameter %~0 ECHO Usage: ECHO MakeCoq_MinGW CALL :PrintPars - goto :EOF + GOTO :EOF ) IF NOT EXIST %SETUP% ( @@ -255,7 +263,7 @@ 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) +IF "%COQREGTESTING%"=="Y" (GOTO DontAsk) SET /p ANSWER=Is this correct? y/n IF NOT "%ANSWER%"=="y" (GOTO :EOF) :DontAsk @@ -325,7 +333,7 @@ REM => Create the setup log in a temporary location and move it later. REM Get Unique temporary file name :logfileloop SET LOGFILE=%TEMP%\CygwinSetUp%RANDOM%-%RANDOM%-%RANDOM%-%RANDOM%.log -if exist "%LOGFILE%" goto :logfileloop +if exist "%LOGFILE%" GOTO logfileloop REM Run Cygwin Setup @@ -339,10 +347,10 @@ IF NOT "%CYGWIN_QUIET%" == "Y" ( IF "%RUNSETUP%"=="Y" ( %SETUP% ^ - --proxy %PROXY% ^ - --site %CYGWIN_REPOSITORY% ^ - --root %CYGWIN_INSTALLDIR_WFMT% ^ - --local-package-dir %CYGWIN_LOCAL_CACHE_WFMT% ^ + --proxy "%PROXY%" ^ + --site "%CYGWIN_REPOSITORY%" ^ + --root "%CYGWIN_INSTALLDIR_WFMT%" ^ + --local-package-dir "%CYGWIN_LOCAL_CACHE_WFMT%" ^ --no-shortcuts ^ %CYGWIN_OPT% ^ -P wget,curl,git,make,unzip ^ @@ -359,11 +367,11 @@ IF "%RUNSETUP%"=="Y" ( -P libtool,automake ^ -P intltool ^ > "%LOGFILE%" ^ - || GOTO :Error + || GOTO ErrorExit - MKDIR %CYGWIN_INSTALLDIR_WFMT%\build - MKDIR %CYGWIN_INSTALLDIR_WFMT%\build\buildlogs - MOVE "%LOGFILE%" %CYGWIN_INSTALLDIR_WFMT%\build\buildlogs\cygwinsetup.log || GOTO :Error + MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build" + MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\buildlogs" + MOVE "%LOGFILE%" "%CYGWIN_INSTALLDIR_WFMT%\build\buildlogs\cygwinsetup.log" || GOTO ErrorExit ) @@ -377,18 +385,18 @@ IF NOT "%CYGWIN_QUIET%" == "Y" ( ECHO ========== CONFIGURE CYGWIN USER ACCOUNT ========== -copy %BATCHDIR%\configure_profile.sh %CYGWIN_INSTALLDIR_WFMT%\var\tmp || GOTO :Error -%BASH% --login %CYGWIN_INSTALLDIR_CFMT%\var\tmp\configure_profile.sh %PROXY% || GOTO :Error +copy "%BATCHDIR%\configure_profile.sh" "%CYGWIN_INSTALLDIR_WFMT%\var\tmp" || GOTO ErrorExit +%BASH% --login "%CYGWIN_INSTALLDIR_CFMT%\var\tmp\configure_profile.sh" "%PROXY%" || GOTO ErrorExit ECHO ========== BUILD COQ ========== -MKDIR %CYGWIN_INSTALLDIR_WFMT%\build -MKDIR %CYGWIN_INSTALLDIR_WFMT%\build\patches +MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build" +MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\patches" -COPY %BATCHDIR%\makecoq_mingw.sh %CYGWIN_INSTALLDIR_WFMT%\build || GOTO :Error -COPY %BATCHDIR%\patches_coq\*.* %CYGWIN_INSTALLDIR_WFMT%\build\patches || GOTO :Error +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 :Error +%BASH% --login "%CYGWIN_INSTALLDIR_CFMT%\build\makecoq_mingw.sh" || GOTO ErrorExit ECHO ========== FINISHED ========== @@ -440,6 +448,19 @@ ECHO ========== BATCH FUNCTIONS ========== ECHO -threads = %MAKE_THREADS% GOTO :EOF -:Error -ECHO Building Coq failed with error code %errorlevel% -EXIT /b %errorlevel% +: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 index 3a3711724..bcb104772 100644 --- a/dev/build/windows/MakeCoq_SetRootPath.bat +++ b/dev/build/windows/MakeCoq_SetRootPath.bat @@ -1,3 +1,14 @@ +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 diff --git a/dev/build/windows/MakeCoq_explicitcachefolders_installer.bat b/dev/build/windows/MakeCoq_explicitcachefolders_installer.bat new file mode 100755 index 000000000..d7d3c5b9d --- /dev/null +++ b/dev/build/windows/MakeCoq_explicitcachefolders_installer.bat @@ -0,0 +1,28 @@ +@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 new file mode 100755 index 000000000..752b73c10 --- /dev/null +++ b/dev/build/windows/MakeCoq_local_installer.bat @@ -0,0 +1,26 @@ +@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_regtest_noproxy.bat b/dev/build/windows/MakeCoq_regtest_noproxy.bat index 2b0b83fed..7b17e721b 100644 --- a/dev/build/windows/MakeCoq_regtest_noproxy.bat +++ b/dev/build/windows/MakeCoq_regtest_noproxy.bat @@ -1,7 +1,18 @@ +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=
-EXPORT HTTP_PROXY=
+SET HTTPS_PROXY=
MKDIR C:\Temp\srccache
call MakeCoq_MinGW.bat ^
diff --git a/dev/build/windows/MakeCoq_regtests.bat b/dev/build/windows/MakeCoq_regtests.bat index 6e36d0140..74c26456b 100644 --- a/dev/build/windows/MakeCoq_regtests.bat +++ b/dev/build/windows/MakeCoq_regtests.bat @@ -1,16 +1,36 @@ -SET COQREGTESTING=Y +REM ========== COPYRIGHT/COPYLEFT ========== -REM Bleeding edge -call MakeCoq_86git_abs_ocaml.bat -call MakeCoq_86git_installer.bat -call MakeCoq_86git_installer_32.bat -call MakeCoq_86git_abs_ocaml_gtksrc.bat +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_85pl3_abs_ocaml.bat -call MakeCoq_85pl3_installer.bat -call MakeCoq_85pl3_installer_32.bat +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_85pl2_abs_ocaml.bat -call MakeCoq_84pl6_abs_ocaml.bat +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/MakeCoq_trunk_installer.bat b/dev/build/windows/MakeCoq_trunk_installer.bat new file mode 100755 index 000000000..f4f582732 --- /dev/null +++ b/dev/build/windows/MakeCoq_trunk_installer.bat @@ -0,0 +1,26 @@ +@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-trunk ^
+ -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/ReadMe.txt b/dev/build/windows/ReadMe.txt index 0faf5bc53..a6d8e4462 100644 --- a/dev/build/windows/ReadMe.txt +++ b/dev/build/windows/ReadMe.txt @@ -1,3 +1,12 @@ +(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 @@ -286,9 +295,16 @@ Default value: <folder of MakeCoq_MinGW.bat>\source_cache The version of Coq to download and compile. -Possible values: 8.4pl6, 8.5pl2, 8.5pl3, git-v8.6 - Others might work, but are untested. +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=absoloute + + 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 @@ -322,6 +338,8 @@ Possible values: 1..N. ==================== TODO ==================== +- Check for spaces in destination paths +- Check for = signs in all paths (DOS commands don't work with pathes 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) diff --git a/dev/build/windows/configure_profile.sh b/dev/build/windows/configure_profile.sh index 09a9cf35a..0b61a31e7 100644 --- a/dev/build/windows/configure_profile.sh +++ b/dev/build/windows/configure_profile.sh @@ -1,5 +1,16 @@ #!/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 @@ -7,7 +18,7 @@ if [ ! -f $donefile ] ; then echo >> $rcfile - if [ -n "$1" ]; then + if [ "$1" != "" -a "$1" != " " ]; then echo export http_proxy="http://$1" >> $rcfile echo export https_proxy="http://$1" >> $rcfile echo export ftp_proxy="http://$1" >> $rcfile diff --git a/dev/build/windows/difftar-folder.sh b/dev/build/windows/difftar-folder.sh index 65278d5c9..cbcf14ec2 100644 --- a/dev/build/windows/difftar-folder.sh +++ b/dev/build/windows/difftar-folder.sh @@ -8,35 +8,28 @@ # 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 ###################### +###################### DIFF A TAR FILE AND A FOLDER ###################### set -o nounset # Print usage -if [ "$#" -lt 1 ] ; then +if [ "$#" -lt 2 ] ; then echo 'Diff a tar (or compressed tar) file with a folder' - echo 'difftar-folder.sh <tarfile> [<folder>] [strip]' - echo default for folder is . - echo default for strip is 0. - echo 'strip must be 0 or 1.' + 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 - -if [ "$#" -ge 2 ] ; then - folder=$2 -else - folder=. -fi +folder=$2 if [ "$#" -ge 3 ] ; then strip=$3 @@ -47,27 +40,33 @@ fi # Get path prefix if --strip is used if [ "$strip" -gt 0 ] ; then - prefix=`tar -t -f $tarfile | head -1` + # Get the path/name of the first file from teh 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 -if [ "$strip" -gt 0 ] ; then - orig=${prefix%/}.orig -elif [ "$folder" = "." ] ; then - orig=${tarfile##*/} - orig=./${orig%%.tar*}.orig -elif [ "$folder" = "" ] ; then - orig=${tarfile##*/} - orig=${orig%%.tar*}.orig -else - orig=$folder.orig -fi -echo $orig +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 @@ -83,4 +82,8 @@ tar --diff -a -f "$tarfile" --strip $strip --directory "$folder" | grep "Mod tim # Compute diff diff -u "$orig/$file" "$folder/$file" fi -done
\ No newline at end of file +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 index 98e80c765..e17923951 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -98,6 +98,8 @@ 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 PREFIX=$CYGWIN_INSTALLDIR_MFMT/usr/$TARGET_ARCH/sys-root/mingw @@ -112,9 +114,9 @@ else PREFIXOCAML=$PREFIX fi -mkdir -p $PREFIX/bin -mkdir -p $PREFIXCOQ/bin -mkdir -p $PREFIXOCAML/bin +mkdir -p "$PREFIX/bin" +mkdir -p "$PREFIXCOQ/bin" +mkdir -p "$PREFIXOCAML/bin" ###################### Copy Cygwin Setup Info ##################### @@ -128,7 +130,7 @@ 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 "$CYGWIN_LOCAL_CACHE_WFMT/$CYGWIN_REPO_FOLDER/$CYGWINARCH/setup.ini" $TARBALLS cp /etc/setup/installed.db $TARBALLS ###################### LOGGING ##################### @@ -158,6 +160,21 @@ logn() { "$@" > $LOGS/$LOGTARGET-$LOGTARGETEX.log 2> $LOGS/$LOGTARGET-$LOGTARGETEX.err } +###################### '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 ##################### # ------------------------------------------------------------------------------ @@ -202,8 +219,8 @@ function get_expand_source_tar { # 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 + if [ -f "$SOURCE_LOCAL_CACHE_CFMT/$name.$3" ] ; then + cp "$SOURCE_LOCAL_CACHE_CFMT/$name.$3" $TARBALLS else wget $1/$2.$3 if [ ! "$2.$3" == "$name.$3" ] ; then @@ -211,8 +228,8 @@ function get_expand_source_tar { 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 + if [ -d "$SOURCE_LOCAL_CACHE_CFMT" ] ; then + cp $TARBALLS/$name.$3 "$SOURCE_LOCAL_CACHE_CFMT" fi fi fi @@ -341,7 +358,7 @@ function build_post { function build_conf_make_inst { if build_prep $1 $2 $3 ; then $4 - logn configure ./configure --build=$BUILD --host=$HOST --target=$TARGET --prefix=$PREFIX "${@:5}" + logn configure ./configure --build=$BUILD --host=$HOST --target=$TARGET --prefix="$PREFIX" "${@:5}" log1 make $MAKE_OPT log2 make install log2 make clean @@ -388,7 +405,7 @@ function install_rec { function list_files { if [ ! -e "/build/filelists/$1" ] ; then - ( cd $PREFIXCOQ && find -type f | sort > /build/filelists/$1 ) + ( cd "$PREFIXCOQ" && find -type f | sort > /build/filelists/$1 ) fi } @@ -436,6 +453,18 @@ function files_to_nsis { ###################### 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 + log2 make install + log2 make clean + build_post + fi +} + ##### LIBPNG ##### function make_libpng { @@ -639,9 +668,9 @@ function make_libxml2 { # 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=$PREFIX --disable-shared --without-python + # ./autogen.sh --build=$BUILD --host=$HOST --target=$TARGET --prefix="$PREFIX" --disable-shared --without-python # shared library required by gtksourceview - ./autogen.sh --build=$BUILD --host=$HOST --target=$TARGET --prefix=$PREFIX --without-python + ./autogen.sh --build=$BUILD --host=$HOST --target=$TARGET --prefix="$PREFIX" --without-python log1 make $MAKE_OPT all log2 make install log2 make clean @@ -676,10 +705,10 @@ function install_flexdll { cp flexdll.h /usr/$TARGET_ARCH/sys-root/mingw/include if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then cp flexdll*_mingw.o /usr/$TARGET_ARCH/bin - cp flexdll*_mingw.o $PREFIXOCAML/bin + cp flexdll*_mingw.o "$PREFIXOCAML/bin" elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then cp flexdll*_mingw64.o /usr/$TARGET_ARCH/bin - cp flexdll*_mingw64.o $PREFIXOCAML/bin + cp flexdll*_mingw64.o "$PREFIXOCAML/bin" else echo "Unknown target architecture" return 1 @@ -691,7 +720,7 @@ function install_flexdll { function install_flexlink { cp flexlink.exe /usr/$TARGET_ARCH/bin - cp flexlink.exe $PREFIXOCAML/bin + cp flexlink.exe "$PREFIXOCAML/bin" } # Get binary flexdll flexlink for building OCaml @@ -737,7 +766,7 @@ function make_ln { 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 + install -D ln.exe "$PREFIXCOQ/bin/ln.exe" cd .. touch flagfiles/myln.finished fi @@ -762,6 +791,7 @@ function make_ocaml { fi # Prefix is fixed in make file - replace it with the real one + # TODO: this might not work if PREFIX contains spaces sed -i "s|^PREFIX=.*|PREFIX=$PREFIXOCAML|" config/Makefile # We don't want to mess up Coq's dirctory structure so put the OCaml library in a separate folder @@ -782,15 +812,15 @@ function make_ocaml { # Move license files and other into into special folder if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then - mkdir -p $PREFIXOCAML/license_readme/ocaml + 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 $PREFIXOCAML/license_readme/ocaml/Install.txt - cp README $PREFIXOCAML/license_readme/ocaml/ReadMe.txt - cp README.win32 $PREFIXOCAML/license_readme/ocaml/ReadMeWin32.txt - cp VERSION $PREFIXOCAML/license_readme/ocaml/Version.txt - cp Changes $PREFIXOCAML/license_readme/ocaml/Changes.txt + cp LICENSE "$PREFIXOCAML/license_readme/ocaml/License.txt" + cp INSTALL "$PREFIXOCAML/license_readme/ocaml/Install.txt" + cp README "$PREFIXOCAML/license_readme/ocaml/ReadMe.txt" + cp README.win32 "$PREFIXOCAML/license_readme/ocaml/ReadMeWin32.txt" + cp VERSION "$PREFIXOCAML/license_readme/ocaml/Version.txt" + cp Changes "$PREFIXOCAML/license_readme/ocaml/Changes.txt" fi build_post @@ -798,12 +828,28 @@ function make_ocaml { make_flex_dll_link } +##### OCAML EXTRA TOOLS ##### + +function make_ocaml_tools { + make_findlib + make_menhir + make_camlp5 +} + +##### OCAML EXTRA LIBRARIES ##### + +function make_ocaml_libs { + make_findlib + make_lablgtk + make_stdint +} + ##### FINDLIB Ocaml library manager ##### function make_findlib { make_ocaml if build_prep http://download.camlcity.org/download findlib-1.5.6 tar.gz 1 ; then - ./configure -bindir $PREFIXOCAML\\bin -sitelib $PREFIXOCAML\\libocaml\\site-lib -config $PREFIXOCAML\\etc\\findlib.conf + 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 @@ -824,9 +870,9 @@ function make_menhir { # For Ocaml 4.01 if build_prep http://gallium.inria.fr/~fpottier/menhir menhir-20140422 tar.gz 1 ; then # Note: menhir doesn't support -j 8, so don't pass MAKE_OPT - log2 make all PREFIX=$PREFIXOCAML - log2 make install PREFIX=$PREFIXOCAML - mv $PREFIXOCAML/bin/menhir $PREFIXOCAML/bin/menhir.exe + log2 make all PREFIX="$PREFIXOCAML" + log2 make install PREFIX="$PREFIXOCAML" + mv "$PREFIXOCAML/bin/menhir" "$PREFIXOCAML/bin/menhir.exe" build_post fi } @@ -863,7 +909,7 @@ function make_camlp5 { log1 make world.opt $MAKE_OPT log2 make install # For some reason gramlib.a is not copied, but it is required by Coq - cp lib/gramlib.a $PREFIXOCAML/libocaml/camlp5/ + cp lib/gramlib.a "$PREFIXOCAML/libocaml/camlp5/" log2 make clean build_post fi @@ -878,11 +924,13 @@ function make_camlp5 { function make_lablgtk { make_ocaml make_findlib - make_camlp4 + make_camlp4 # required by lablgtk-2.18.3 and lablgtk-2.18.5 + make_gtk2 + make_gtk_sourceview2 if build_prep https://forge.ocamlcore.org/frs/download.php/1479 lablgtk-2.18.3 tar.gz 1 ; then # configure should be fixed to search for $TARGET_ARCH-pkg-config.exe cp /bin/$TARGET_ARCH-pkg-config.exe bin_special/pkg-config.exe - logn configure ./configure --build=$BUILD --host=$HOST --target=$TARGET --prefix=$PREFIXOCAML + logn configure ./configure --build=$BUILD --host=$HOST --target=$TARGET --prefix="$PREFIXOCAML" # lablgtk shows occasional errors with -j, so don't pass $MAKE_OPT @@ -920,7 +968,7 @@ function make_stdint { function copy_coq_dll { if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then - cp /usr/${ARCH}-w64-mingw32/sys-root/mingw/bin/$1 $PREFIXCOQ/bin/$1 + cp /usr/${ARCH}-w64-mingw32/sys-root/mingw/bin/$1 "$PREFIXCOQ/bin/$1" fi } @@ -954,6 +1002,7 @@ function copy_coq_dlls { copy_coq_dll LIBPANGO-1.0-0.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 @@ -962,7 +1011,6 @@ function copy_coq_dlls { # Depends on if GTK is built from sources if [ "$GTK_FROM_SOURCES" == "Y" ]; then copy_coq_dll libiconv-2.dll - copy_coq_dll libpcre-1.dll else copy_coq_dll ICONV.DLL copy_coq_dll LIBBZ2-1.DLL @@ -986,13 +1034,13 @@ function copy_coq_dlls { function copy_coq_objects { # copy objects only from folders which exist in the target lib directory find . -type d | while read FOLDER ; do - if [ -e $PREFIXCOQ/lib/$FOLDER ] ; then - install_glob $FOLDER/'*.cmxa' $PREFIXCOQ/lib/$FOLDER - install_glob $FOLDER/'*.cmi' $PREFIXCOQ/lib/$FOLDER - install_glob $FOLDER/'*.cma' $PREFIXCOQ/lib/$FOLDER - install_glob $FOLDER/'*.cmo' $PREFIXCOQ/lib/$FOLDER - install_glob $FOLDER/'*.a' $PREFIXCOQ/lib/$FOLDER - install_glob $FOLDER/'*.o' $PREFIXCOQ/lib/$FOLDER + if [ -e "$PREFIXCOQ/lib/$FOLDER" ] ; then + install_glob $FOLDER/'*.cmxa' "$PREFIXCOQ/lib/$FOLDER" + install_glob $FOLDER/'*.cmi' "$PREFIXCOQ/lib/$FOLDER" + install_glob $FOLDER/'*.cma' "$PREFIXCOQ/lib/$FOLDER" + install_glob $FOLDER/'*.cmo' "$PREFIXCOQ/lib/$FOLDER" + install_glob $FOLDER/'*.a' "$PREFIXCOQ/lib/$FOLDER" + install_glob $FOLDER/'*.o' "$PREFIXCOQ/lib/$FOLDER" fi done } @@ -1000,23 +1048,23 @@ function copy_coq_objects { # Copy required GTK config and suport files function copq_coq_gtk { - echo 'gtk-theme-name = "MS-Windows"' > $PREFIX/etc/gtk-2.0/gtkrc - echo 'gtk-fallback-icon-theme = "Tango"' >> $PREFIX/etc/gtk-2.0/gtkrc + echo 'gtk-theme-name = "MS-Windows"' > "$PREFIX/etc/gtk-2.0/gtkrc" + echo 'gtk-fallback-icon-theme = "Tango"' >> "$PREFIX/etc/gtk-2.0/gtkrc" if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then - install_glob $PREFIX/etc/gtk-2.0/'*' $PREFIXCOQ/gtk-2.0 - install_glob $PREFIX/share/gtksourceview-2.0/language-specs/'*' $PREFIXCOQ/share/gtksourceview-2.0/language-specs - install_glob $PREFIX/share/gtksourceview-2.0/styles/'*' $PREFIXCOQ/share/gtksourceview-2.0/styles - install_rec $PREFIX/share/themes/ '*' $PREFIXCOQ/share/themes + install_glob "$PREFIX/etc/gtk-2.0/"'*' "$PREFIXCOQ/gtk-2.0" + install_glob "$PREFIX/share/gtksourceview-2.0/language-specs/"'*' "$PREFIXCOQ/share/gtksourceview-2.0/language-specs" + install_glob "$PREFIX/share/gtksourceview-2.0/styles/"'*' "$PREFIXCOQ/share/gtksourceview-2.0/styles" + install_rec "$PREFIX/share/themes/" '*' "$PREFIXCOQ/share/themes" # This below item look like a bug in make install if [[ ! $COQ_VERSION == 8.4* ]] ; then - mv $PREFIXCOQ/share/coq/*.lang $PREFIXCOQ/share/gtksourceview-2.0/language-specs - mv $PREFIXCOQ/share/coq/*.xml $PREFIXCOQ/share/gtksourceview-2.0/styles + mv "$PREFIXCOQ/share/coq/"*.lang "$PREFIXCOQ/share/gtksourceview-2.0/language-specs" + mv "$PREFIXCOQ/share/coq/"*.xml "$PREFIXCOQ/share/gtksourceview-2.0/styles" fi - mkdir -p $PREFIXCOQ/ide - mv $PREFIXCOQ/share/coq/*.png $PREFIXCOQ/ide - rmdir $PREFIXCOQ/share/coq + mkdir -p "$PREFIXCOQ/ide" + mv "$PREFIXCOQ/share/coq/"*.png "$PREFIXCOQ/ide" + rmdir "$PREFIXCOQ/share/coq" fi } @@ -1024,16 +1072,17 @@ function copq_coq_gtk { 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 - install -D README $PREFIXCOQ/license_readme/coq/ReadMe.txt || true - install -D README.md $PREFIXCOQ/license_readme/coq/ReadMe.md || true - install -D README.doc $PREFIXCOQ/license_readme/coq/ReadMeDoc.txt - install -D CHANGES $PREFIXCOQ/license_readme/coq/Changes.txt - install -D INSTALL $PREFIXCOQ/license_readme/coq/Install.txt - install -D INSTALL.doc $PREFIXCOQ/license_readme/coq/InstallDoc.txt - install -D INSTALL.ide $PREFIXCOQ/license_readme/coq/InstallIde.txt + 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" + install -D README "$PREFIXCOQ/license_readme/coq/ReadMe.txt" || true + install -D README.md "$PREFIXCOQ/license_readme/coq/ReadMe.md" || true + install -D README.win "$PREFIXCOQ/license_readme/coq/ReadMeWindows.txt" || true + install -D README.doc "$PREFIXCOQ/license_readme/coq/ReadMeDoc.txt" + install -D CHANGES "$PREFIXCOQ/license_readme/coq/Changes.txt" + install -D INSTALL "$PREFIXCOQ/license_readme/coq/Install.txt" + install -D INSTALL.doc "$PREFIXCOQ/license_readme/coq/InstallDoc.txt" + install -D INSTALL.ide "$PREFIXCOQ/license_readme/coq/InstallIde.txt" fi } @@ -1043,19 +1092,38 @@ function make_coq { make_ocaml make_lablgtk make_camlp5 - if + if case $COQ_VERSION in - git-*) build_prep https://github.com/coq/coq/archive ${COQ_VERSION##git-} zip 1 coq-${COQ_VERSION} ;; - *) build_prep https://coq.inria.fr/distrib/V$COQ_VERSION/files coq-$COQ_VERSION tar.gz ;; + # 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 -debug -with-doc no -prefix ./ -libdir ./lib -mandir ./man elif [ "$INSTALLMODE" == "absolute" ]; then - logn configure ./configure -debug -with-doc no -prefix $PREFIXCOQ -libdir $PREFIXCOQ/lib -mandir $PREFIXCOQ/man + logn configure ./configure -debug -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man" else - logn configure ./configure -debug -with-doc no -prefix $PREFIXCOQ + logn configure ./configure -debug -with-doc no -prefix "$PREFIXCOQ" fi # The windows resource compiler binary name is hard coded @@ -1070,7 +1138,7 @@ function make_coq { fi if [ "$INSTALLMODE" == "relocatable" ]; then - ./configure -debug -with-doc no -prefix $PREFIXCOQ -libdir $PREFIXCOQ/lib -mandir $PREFIXCOQ/man + logn reconfigure ./configure -debug -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man" fi log2 make install @@ -1101,7 +1169,7 @@ function make_mingw_make { # 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 + cp GccRel/gnumake.exe "$PREFIXCOQ/bin/make.exe" build_post fi } @@ -1110,7 +1178,7 @@ function make_mingw_make { 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- + logn configure ./configure --build=$BUILD --host=$HOST --target=$TARGET --prefix="$PREFIXCOQ" --program-prefix=$TARGET- log1 make $MAKE_OPT log2 make install # log2 make clean @@ -1133,15 +1201,15 @@ function make_gcc { # 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 + 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 \ + --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=$PREFIX results in configure error that this is not an absolute path + # --with-sysroot="$PREFIX" results in configure error that this is not an absolute path log1 make $MAKE_OPT log2 make install # log2 make clean @@ -1176,14 +1244,14 @@ function get_cygwin_mingw_sources { # 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 + if [ -f "$SOURCE_LOCAL_CACHE_CFMT/$SOURCEFILE" ] ; then + cp "$SOURCE_LOCAL_CACHE_CFMT/$SOURCEFILE" $TARBALLS else wget "$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 + if [ -d "$SOURCE_LOCAL_CACHE_CFMT" ] ; then + cp $TARBALLS/$SOURCEFILE "$SOURCE_LOCAL_CACHE_CFMT" fi fi fi @@ -1199,7 +1267,7 @@ function get_cygwin_mingw_sources { function make_coq_installer { make_coq make_mingw_make - get_cygwin_mingw_sources + # get_cygwin_mingw_sources # Prepare the file lists for the installer. We created to file list dumps of the target folder during the build: # ocaml: ocaml + menhir + camlp5 + findlib @@ -1230,14 +1298,14 @@ function make_coq_installer { NSIS=`pwd`/makensis.exe chmod u+x "$NSIS" # Change to Coq folder - cd ../coq-${COQ_VERSION} + 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` + 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\\coq.ico coq_new.nsi + logn nsis-installer "$NSIS" -DVERSION=$VERSION -DARCH=$ARCH -DCOQ_SRC_PATH="$PREFIXCOQ" -DCOQ_ICON=..\\..\\ide\\coq.ico coq_new.nsi build_post fi @@ -1245,17 +1313,13 @@ function make_coq_installer { ###################### TOP LEVEL BUILD ##################### -make_gtk2 -make_gtk_sourceview2 - +make_sed make_ocaml -make_findlib -make_lablgtk -make_camlp4 -make_camlp5 -make_menhir -make_stdint +make_ocaml_tools +make_ocaml_libs + list_files ocaml + make_coq if [ "$INSTALLMAKE" == "Y" ] ; then 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 new file mode 100755 index 000000000..d210a0415 --- /dev/null +++ b/dev/build/windows/patches_coq/sed-4.2.2-3.src.patch @@ -0,0 +1,1301 @@ +--- 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 new file mode 100755 index 000000000..c7ccd53c7 --- /dev/null +++ b/dev/build/windows/patches_coq/sed-4.2.2.patch @@ -0,0 +1,1301 @@ +--- 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? */ diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index a0a4e0749..309050057 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -32,4 +32,4 @@ sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/List/ListUt sed -i -e "17i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Multiset/MultisetOrder.v sed -i -e "13i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Set/SetUtil.v -( cd ${Color_CI_DIR} && make -j ${NJOBS} ) +( cd ${Color_CI_DIR} && make ) diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 5435e9588..238960948 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -68,7 +68,7 @@ install_ssreflect() sed -i.bak '/field/d' Make && \ sed -i.bak '/fingroup/d' Make && \ sed -i.bak '/algebra/d' Make && \ - make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all && make install ) + make Makefile.coq && make -f Makefile.coq all && make install ) echo -en 'travis_fold:end:ssr.install\\r' diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index c78ffdc2c..0dd904648 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -9,4 +9,4 @@ opam install -j ${NJOBS} -y menhir git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR} # Patch to avoid the upper version limit -( cd ${CompCert_CI_DIR} && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make -j ${NJOBS} ) +( cd ${CompCert_CI_DIR} && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make ) diff --git a/dev/ci/ci-cpdt.sh b/dev/ci/ci-cpdt.sh index 0e791ebbf..8b725f6fe 100755 --- a/dev/ci/ci-cpdt.sh +++ b/dev/ci/ci-cpdt.sh @@ -6,5 +6,5 @@ source ${ci_dir}/ci-common.sh wget http://adam.chlipala.net/cpdt/cpdt.tgz tar xvfz cpdt.tgz -( cd cpdt && make clean && make -j ${NJOBS} ) +( cd cpdt && make clean && make ) diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index c6df45a1d..5ca3ac47f 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -6,5 +6,6 @@ source ${ci_dir}/ci-common.sh fiat_crypto_CI_DIR=${CI_BUILD_DIR}/fiat-crypto git_checkout ${fiat_crypto_CI_BRANCH} ${fiat_crypto_CI_GITURL} ${fiat_crypto_CI_DIR} +( cd ${fiat_crypto_CI_DIR} && git submodule update --init --recursive ) -( cd ${fiat_crypto_CI_DIR} && make -j ${NJOBS} lite ) +( cd ${fiat_crypto_CI_DIR} && make lite ) diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh index 2095245eb..292331b81 100755 --- a/dev/ci/ci-fiat-parsers.sh +++ b/dev/ci/ci-fiat-parsers.sh @@ -7,4 +7,4 @@ fiat_parsers_CI_DIR=${CI_BUILD_DIR}/fiat git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} ${fiat_parsers_CI_DIR} -( cd ${fiat_parsers_CI_DIR} && make -j ${NJOBS} parsers parsers-examples && make -j ${NJOBS} fiat-core ) +( cd ${fiat_parsers_CI_DIR} && make parsers parsers-examples && make fiat-core ) diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh index 64b78c039..2556f84a5 100755 --- a/dev/ci/ci-formal-topology.sh +++ b/dev/ci/ci-formal-topology.sh @@ -17,16 +17,16 @@ source ${ci_dir}/ci-bignums.sh git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR} -( cd ${math_classes_CI_DIR} && make -j ${NJOBS} && make install ) +( cd ${math_classes_CI_DIR} && make && make install ) # Setup Corn git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR} -( cd ${Corn_CI_DIR} && make -j ${NJOBS} && make install ) +( cd ${Corn_CI_DIR} && make && make install ) # Setup formal-topology git_checkout ${formal_topology_CI_BRANCH} ${formal_topology_CI_GITURL} ${formal_topology_CI_DIR} -( cd ${formal_topology_CI_DIR} && make -j ${NJOBS} ) +( cd ${formal_topology_CI_DIR} && make ) diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index 4e5aa2687..eadeb7c38 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -13,4 +13,4 @@ git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} ${GeoCoq_CI_DIR} sed -i.bak '/Elements\/Book_1\.v/d' Make && \ sed -i.bak '/Elements\/Book_3\.v/d' Make && \ coq_makefile -f Make -o Makefile && \ - make -j ${NJOBS} ) + make ) diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 1bf6e9a87..693135a4c 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -7,4 +7,4 @@ HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT git_checkout ${HoTT_CI_BRANCH} ${HoTT_CI_GITURL} ${HoTT_CI_DIR} -( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make -j ${NJOBS} ) +( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make ) diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh index 262dd6fa0..2d127ddc1 100755 --- a/dev/ci/ci-iris-coq.sh +++ b/dev/ci/ci-iris-coq.sh @@ -20,7 +20,7 @@ stdpp_CI_COMMIT=${IRIS_DEP[2]} git_checkout ${stdpp_CI_BRANCH} ${stdpp_CI_GITURL} ${stdpp_CI_DIR} ${stdpp_CI_COMMIT} -( cd ${stdpp_CI_DIR} && make -j ${NJOBS} && make install ) +( cd ${stdpp_CI_DIR} && make && make install ) # Build iris now -( cd ${Iris_CI_DIR} && make -j ${NJOBS} ) +( cd ${Iris_CI_DIR} && make ) diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh index 46581c638..2837dee96 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math-classes.sh @@ -15,10 +15,10 @@ source ${ci_dir}/ci-bignums.sh git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR} -( cd ${math_classes_CI_DIR} && make -j ${NJOBS} && make install ) +( cd ${math_classes_CI_DIR} && make && make install ) # Setup Corn git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR} -( cd ${Corn_CI_DIR} && make -j ${NJOBS} ) +( cd ${Corn_CI_DIR} && make ) diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh index bb8188da4..701403f2c 100755 --- a/dev/ci/ci-math-comp.sh +++ b/dev/ci/ci-math-comp.sh @@ -12,4 +12,4 @@ checkout_mathcomp ${mathcomp_CI_DIR} ( cd ${mathcomp_CI_DIR}/mathcomp && \ sed -i.bak '/PFsection/d' Make && \ sed -i.bak '/stripped_odd_order_theorem/d' Make && \ - make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all ) + make Makefile.coq && make -f Makefile.coq all ) diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh index e31691179..c813b1fe9 100755 --- a/dev/ci/ci-metacoq.sh +++ b/dev/ci/ci-metacoq.sh @@ -10,10 +10,10 @@ metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq git_checkout ${unicoq_CI_BRANCH} ${unicoq_CI_GITURL} ${unicoq_CI_DIR} -( cd ${unicoq_CI_DIR} && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install ) +( cd ${unicoq_CI_DIR} && coq_makefile -f Make -o Makefile && make && make install ) # Setup MetaCoq git_checkout ${metacoq_CI_BRANCH} ${metacoq_CI_GITURL} ${metacoq_CI_DIR} -( cd ${metacoq_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} ) +( cd ${metacoq_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make ) diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index 23ef41d2d..6e6c7012b 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -9,6 +9,6 @@ tar xvfz sf.tgz sed -i.bak '15i From Coq Require Extraction.' sf/Extraction.v -( cd sf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make -j ${NJOBS} ) +( cd sf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make ) diff --git a/dev/ci/ci-template.sh b/dev/ci/ci-template.sh index 700105aed..25da01a82 100755 --- a/dev/ci/ci-template.sh +++ b/dev/ci/ci-template.sh @@ -9,4 +9,4 @@ Template_CI_DIR=${CI_BUILD_DIR}/Template git_checkout ${Template_CI_BRANCH} ${Template_CI_GITURL} ${Template_CI_DIR} -( cd ${Template_CI_DIR} && make -j ${NJOBS} ) +( cd ${Template_CI_DIR} && make ) diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh index ce2639937..8ecd8c441 100755 --- a/dev/ci/ci-tlc.sh +++ b/dev/ci/ci-tlc.sh @@ -7,4 +7,4 @@ tlc_CI_DIR=${CI_BUILD_DIR}/tlc git_checkout ${tlc_CI_BRANCH} ${tlc_CI_GITURL} ${tlc_CI_DIR} -( cd ${tlc_CI_DIR} && make -j ${NJOBS} ) +( cd ${tlc_CI_DIR} && make ) diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh index 175b82b5f..66b56add7 100755 --- a/dev/ci/ci-unimath.sh +++ b/dev/ci/ci-unimath.sh @@ -10,5 +10,5 @@ git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} ${UniMath_CI_DIR} ( cd ${UniMath_CI_DIR} && \ sed -i.bak '/Folds/d' Makefile && \ sed -i.bak '/HomologicalAlgebra/d' Makefile && \ - make -j ${NJOBS} BUILD_COQ=no ) + make BUILD_COQ=no ) diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh index c11195185..27a336d80 100755 --- a/dev/ci/ci-vst.sh +++ b/dev/ci/ci-vst.sh @@ -10,4 +10,4 @@ git_checkout ${VST_CI_BRANCH} ${VST_CI_GITURL} ${VST_CI_DIR} # Targets are: msl veric floyd # Patch to avoid the upper version limit -( cd ${VST_CI_DIR} && sed -i.bak 's/8.6$/8.6 or-else trunk/' Makefile && make -j ${NJOBS} ) +( cd ${VST_CI_DIR} && sed -i.bak 's/8.6$/8.6 or-else trunk/' Makefile && make ) diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index acfc4bea9..5966ac468 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -554,7 +554,7 @@ more efficient resolution behavior (the option is off by default). When a solution to the typeclass goal of this class is found, we never backtrack on it, assuming that it is canonical. -\subsection{\tt Typeclasses eauto := [debug] [dfs | bfs] [\emph{depth}]} +\subsection{\tt Typeclasses eauto := [debug] [(dfs) | (bfs)] [\emph{depth}]} \comindex{Typeclasses eauto} \label{TypeclassesEauto} diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 939fc87a6..f338c3055 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -38,21 +38,19 @@ construction allows defining ``signatures''. \end{figure} \noindent In the expression - -\smallskip -{\tt Record} {\ident} {\params} \texttt{:} - {\sort} := {\ident$_0$} \verb+{+ - {\ident$_1$} \binders$_1$ \texttt{:} {\term$_1$}; - \dots - {\ident$_n$} \binders$_n$ \texttt{:} {\term$_n$} \verb+}+. -\smallskip - +\begin{quote} +{\tt Record {\ident} {\params} : {\sort} := {\ident$_0$} \{ \\ + {\ident$_1$} \binders$_1$ : {\term$_1$} ; ... ; \\ + {\ident$_n$} \binders$_n$ : {\term$_n$} \}.} +\end{quote} \noindent the identifier {\ident} is the name of the defined record and {\sort} is its type. The identifier {\ident$_0$} is the name of its constructor. If {\ident$_0$} is omitted, the default name {\tt -Build\_{\ident}} is used. If {\sort} is omitted, the default sort is ``{\Type}''. -The identifiers {\ident$_1$}, .., -{\ident$_n$} are the names of fields and {\tt forall} \binders$_1${\tt ,} {\term$_1$}, ..., {\tt forall} \binders$_n${\tt ,} {\term$_n$} +Build\_{\ident}} is used. +If {\sort} is omitted, the default sort is {\Type}. +The identifiers {\ident$_1$}, \dots, {\ident$_n$} are the names of +fields and {\tt forall {\binders$_1$}, {\term$_1$}}, \dots, +{\tt forall {\binders$_n$}, {\term$_n$}} their respective types. Remark that the type of {\ident$_i$} may depend on the previous {\ident$_j$} (for $j<i$). Thus the order of the fields is important. Finally, {\params} are the parameters of the @@ -82,26 +80,15 @@ Record Rat : Set := mkRat forall x y z:nat, (x * y) = top /\ (x * z) = bottom -> x = 1}. \end{coq_example} -Remark here that the field -\verb+Rat_cond+ depends on the field \verb+bottom+. - -%Let us now see the work done by the {\tt Record} macro. -%First the macro generates an inductive definition -%with just one constructor: -% -%\medskip -%\noindent -%{\tt Inductive {\ident} \zeroone{\binders} : {\sort} := \\ -%\mbox{}\hspace{0.4cm} {\ident$_0$} : forall ({\ident$_1$}:{\term$_1$}) .. -%({\ident$_n$}:{\term$_n$}), {\ident} {\rm\sl params}.} -%\medskip +Remark here that the field \verb+Rat_bottom_cond+ depends +on the field \verb+bottom+ and \verb+Rat_irred_cond+ depends +on both \verb+top+ and \verb+bottom+. Let us now see the work done by the {\tt Record} macro. First the macro generates a variant type definition with just one constructor: \begin{quote} -{\tt Variant {\ident} {\params} :{\sort} :=} \\ -\qquad {\tt - {\ident$_0$} ({\ident$_1$}:{\term$_1$}) .. ({\ident$_n$}:{\term$_n$}).} +{\tt Variant {\ident} {\params} : {\sort} := \\ + {\ident$_0$} ({\ident$_1$} : {\term$_1$}) ... ({\ident$_n$} : {\term$_n$}).} \end{quote} To build an object of type {\ident}, one should provide the constructor {\ident$_0$} with $n$ terms filling the fields of @@ -109,28 +96,9 @@ the record. As an example, let us define the rational $1/2$: \begin{coq_example*} -Require Import Arith. Theorem one_two_irred : forall x y z:nat, x * y = 1 /\ x * z = 2 -> x = 1. -\end{coq_example*} -\begin{coq_eval} -Lemma mult_m_n_eq_m_1 : forall m n:nat, m * n = 1 -> m = 1. -destruct m; trivial. -intros; apply f_equal with (f := S). -destruct m; trivial. -destruct n; simpl in H. - rewrite <- mult_n_O in H. - discriminate. - rewrite <- plus_n_Sm in H. - discriminate. -Qed. - -intros x y z [H1 H2]. - apply mult_m_n_eq_m_1 with (n := y); trivial. -\end{coq_eval} -\ldots -\begin{coq_example*} -Qed. +Admitted. \end{coq_example*} \begin{coq_example} Definition half := mkRat true 1 2 (O_S 1) one_two_irred. @@ -139,80 +107,6 @@ Definition half := mkRat true 1 2 (O_S 1) one_two_irred. Check half. \end{coq_example} -The macro generates also, when it is possible, the projection -functions for destructuring an object of type {\ident}. These -projection functions have the same name that the corresponding -fields. If a field is named ``\verb=_='' then no projection is built -for it. In our example: - -\begin{coq_example} -Eval compute in half.(top). -Eval compute in half.(bottom). -Eval compute in half.(Rat_bottom_cond). -\end{coq_example} -\begin{coq_eval} -Reset Initial. -\end{coq_eval} - -Records defined with the {\tt Record} keyword are not allowed to be -recursive (references to the record's name in the type of its field -raises an error). To define recursive records, one can use the {\tt - Inductive} and {\tt CoInductive} keywords, resulting in an inductive -or co-inductive record. A \emph{caveat}, however, is that records -cannot appear in mutually inductive (or co-inductive) definitions. -Induction schemes are automatically generated for inductive records. -Automatic generation of induction schemes for non-recursive records -defined with the {\tt Record} keyword can be activated with the -{\tt Nonrecursive Elimination Schemes} option -(see~\ref{set-nonrecursive-elimination-schemes}). - -\begin{Warnings} -\item {\tt {\ident$_i$} cannot be defined.} - - It can happen that the definition of a projection is impossible. - This message is followed by an explanation of this impossibility. - There may be three reasons: - \begin{enumerate} - \item The name {\ident$_i$} already exists in the environment (see - Section~\ref{Axiom}). - \item The body of {\ident$_i$} uses an incorrect elimination for - {\ident} (see Sections~\ref{Fixpoint} and~\ref{Caseexpr}). - \item The type of the projections {\ident$_i$} depends on previous - projections which themselves could not be defined. - \end{enumerate} -\end{Warnings} - -\begin{ErrMsgs} - -\item \errindex{Records declared with the keyword Record or Structure cannot be recursive.} - - The record name {\ident} appears in the type of its fields, but uses - the keyword {\tt Record}. Use the keyword {\tt Inductive} or {\tt - CoInductive} instead. -\item \errindex{Cannot handle mutually (co)inductive records.} - - Records cannot be defined as part of mutually inductive (or - co-inductive) definitions, whether with records only or mixed with - standard definitions. -\item During the definition of the one-constructor inductive - definition, all the errors of inductive definitions, as described in - Section~\ref{gal-Inductive-Definitions}, may also occur. - -\end{ErrMsgs} - -\SeeAlso Coercions and records in Section~\ref{Coercions-and-records} -of the chapter devoted to coercions. - -\Rem {\tt Structure} is a synonym of the keyword {\tt Record}. - -\Rem Creation of an object of record type can be done by calling {\ident$_0$} -and passing arguments in the correct order. - -\begin{coq_example} -Record point := { x : nat; y : nat }. -Definition a := Build_point 5 3. -\end{coq_example} - \begin{figure}[t] \begin{centerframe} \begin{tabular}{lcl} @@ -226,15 +120,17 @@ Definition a := Build_point 5 3. \label{fig:fieldsyntax} \end{figure} -A syntax is available for creating objects by using named fields, as +Alternatively, the following syntax allows creating objects by using named fields, as shown on Figure~\ref{fig:fieldsyntax}. The fields do not have to be in any particular order, nor do they have to be all present if the missing ones can be inferred or prompted for (see Section~\ref{Program}). \begin{coq_example} -Definition b := {| x := 5; y := 3 |}. -Definition c := {| y := 3; x := 5 |}. +Definition half' := + {| sign := true; + Rat_bottom_cond := O_S 1; + Rat_irred_cond := one_two_irred |}. \end{coq_example} This syntax can be disabled globally for printing by @@ -256,23 +152,52 @@ This syntax can also be used for pattern matching. \begin{coq_example} Eval compute in ( - match b with - | {| y := S n |} => n + match half with + | {| sign := true; top := n |} => n | _ => 0 end). \end{coq_example} -\begin{coq_eval} -Reset Initial. -\end{coq_eval} +The macro generates also, when it is possible, the projection +functions for destructuring an object of type {\ident}. These +projection functions are given the names of the corresponding +fields. If a field is named ``\verb=_='' then no projection is built +for it. In our example: + +\begin{coq_example} +Eval compute in top half. +Eval compute in bottom half. +Eval compute in Rat_bottom_cond half. +\end{coq_example} + +An alternative syntax for projections based on a dot notation is +available: + +\begin{coq_example} +Eval compute in half.(top). +\end{coq_example} -\Rem A syntax for projections based on a dot notation is -available. The command to activate it is +It can be activated for printing with the command \optindex{Printing Projections} \begin{quote} {\tt Set Printing Projections.} \end{quote} +\begin{coq_example} +Set Printing Projections. +Check top half. +\end{coq_example} + +The corresponding grammar rules are given in Figure~\ref{fig:projsyntax}. +When {\qualid} denotes a projection, the syntax {\tt + {\term}.({\qualid})} is equivalent to {\qualid~\term}, the syntax +{\term}{\tt .(}{\qualid}~{\termarg}$_1$ {\ldots} {\termarg}$_n${\tt )} to +{\qualid~{\termarg}$_1$ {\ldots} {\termarg}$_n$~\term}, and the syntax +{\term}{\tt .(@}{\qualid}~{\term}$_1$~\ldots~{\term}$_n${\tt )} to +{@\qualid~{\term}$_1$ {\ldots} {\term}$_n$~\term}. In each case, {\term} +is the object projected and the other arguments are the parameters of +the inductive type. + \begin{figure}[t] \begin{centerframe} \begin{tabular}{lcl} @@ -285,18 +210,66 @@ available. The command to activate it is \label{fig:projsyntax} \end{figure} -The corresponding grammar rules are given Figure~\ref{fig:projsyntax}. -When {\qualid} denotes a projection, the syntax {\tt - {\term}.({\qualid})} is equivalent to {\qualid~\term}, the syntax -{\term}{\tt .(}{\qualid}~{\termarg}$_1$ {\ldots} {\termarg}$_n${\tt )} to -{\qualid~{\termarg}$_1$ {\ldots} {\termarg}$_n$~\term}, and the syntax -{\term}{\tt .(@}{\qualid}~{\term}$_1$~\ldots~{\term}$_n${\tt )} to -{@\qualid~{\term}$_1$ {\ldots} {\term}$_n$~\term}. In each case, {\term} -is the object projected and the other arguments are the parameters of -the inductive type. +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + +\begin{Remarks} + +\item Records defined with the {\tt Record} keyword are not allowed to be +recursive (references to the record's name in the type of its field +raises an error). To define recursive records, one can use the {\tt +Inductive} and {\tt CoInductive} keywords, resulting in an inductive +or co-inductive record. +A \emph{caveat}, however, is that records +cannot appear in mutually inductive (or co-inductive) definitions. + +\item Induction schemes are automatically generated for inductive records. +Automatic generation of induction schemes for non-recursive records +defined with the {\tt Record} keyword can be activated with the +{\tt Nonrecursive Elimination Schemes} option +(see~\ref{set-nonrecursive-elimination-schemes}). + +\item {\tt Structure} is a synonym of the keyword {\tt Record}. -To deactivate the printing of projections, use -{\tt Unset Printing Projections}. +\end{Remarks} + +\begin{Warnings} +\item {\tt {\ident$_i$} cannot be defined.} + + It can happen that the definition of a projection is impossible. + This message is followed by an explanation of this impossibility. + There may be three reasons: + \begin{enumerate} + \item The name {\ident$_i$} already exists in the environment (see + Section~\ref{Axiom}). + \item The body of {\ident$_i$} uses an incorrect elimination for + {\ident} (see Sections~\ref{Fixpoint} and~\ref{Caseexpr}). + \item The type of the projections {\ident$_i$} depends on previous + projections which themselves could not be defined. + \end{enumerate} +\end{Warnings} + +\begin{ErrMsgs} + +\item \errindex{Records declared with the keyword Record or Structure cannot be recursive.} + + The record name {\ident} appears in the type of its fields, but uses + the keyword {\tt Record}. Use the keyword {\tt Inductive} or {\tt + CoInductive} instead. +\item \errindex{Cannot handle mutually (co)inductive records.} + + Records cannot be defined as part of mutually inductive (or + co-inductive) definitions, whether with records only or mixed with + standard definitions. +\item During the definition of the one-constructor inductive + definition, all the errors of inductive definitions, as described in + Section~\ref{gal-Inductive-Definitions}, may also occur. + +\end{ErrMsgs} + +\SeeAlso Coercions and records in Section~\ref{Coercions-and-records} +of the chapter devoted to coercions. \subsection{Primitive Projections} \optindex{Primitive Projections} @@ -2011,6 +1984,11 @@ Check (fun x y => _) 0 1. Unset Printing Existential Instances. \end{coq_eval} +Existential variables can be named by the user upon creation using +the syntax {\tt ?[\ident]}. This is useful when the existential +variable needs to be explicitly handled later in the script (e.g. +with a named-goal selector, see~\ref{ltac:selector}). + \subsection{Explicit displaying of existential instances for pretty-printing \label{SetPrintingExistentialInstances} \optindex{Printing Existential Instances}} diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index bb679ecba..f3bc2dd05 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -392,7 +392,7 @@ all selected goals. \item{} [{\ident}] {\tt :} {\tacexpr} In this variant, {\tacexpr} is applied locally to a goal - previously named by the user. + previously named by the user (see~\ref{ExistentialVariables}). \item {\num} {\tt :} {\tacexpr} @@ -891,7 +891,7 @@ behavior can be retrieved with the {\tt Tactic Compat Context} flag. \end{Variants} -\subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal@\texttt{match goal}} +\subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal@\texttt{match goal}}\label{ltac-match-goal} \index{Ltac!match reverse goal@\texttt{match reverse goal}} \index{match goal@\texttt{match goal}!in Ltac} \index{match reverse goal@\texttt{match reverse goal}!in Ltac}} diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index b66659dc8..95fee3241 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -421,6 +421,24 @@ This command displays the current goals. \item \errindex{No focused proof} \end{ErrMsgs} +\item {\tt Show {\ident}.}\\ + Displays the named goal {\ident}. + This is useful in particular to display a shelved goal but only works + if the corresponding existential variable has been named by the user + (see~\ref{ExistentialVariables}) as in the following example. + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + +\begin{coq_example*} +Goal exists n, n = 0. + eexists ?[n]. +\end{coq_example*} +\begin{coq_example} + Show n. +\end{coq_example} + \item {\tt Show Script.}\comindex{Show Script}\\ Displays the whole list of tactics applied from the beginning of the current proof. diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index ecaf82806..d02b06df1 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -889,7 +889,8 @@ statically. For instance, if {\tt f} is a polymorphic function of type recognized as an argument to be interpreted in scope {\scope}. \comindex{Bind Scope} -More generally, any {\class} (see Chapter~\ref{Coercions-full}) can be +\label{bindscope} +More generally, any coercion {\class} (see Chapter~\ref{Coercions-full}) can be bound to an interpretation scope. The command to do it is \begin{quote} {\tt Bind Scope} {\scope} \texttt{with} {\class} @@ -908,7 +909,7 @@ Open Scope nat_scope. (* Define + on the nat as the default for + *) Check (fun x y1 y2 z t => P _ (x + t) ((f _ (y1 + y2) + z))). \end{coq_example} -\Rem The scope {\tt type\_scope} has also a local effect on +\Rem The scopes {\tt type\_scope} and {\tt function\_scope} also have a local effect on interpretation. See the next section. \SeeAlso The command to show the scopes bound to the arguments of a @@ -940,10 +941,21 @@ Check # @@%mybool #. The scope {\tt type\_scope} has a special status. It is a primitive interpretation scope which is temporarily activated each time a -subterm of an expression is expected to be a type. This includes goals -and statements, types of binders, domain and codomain of implication, -codomain of products, and more generally any type argument of a -declared or defined constant. +subterm of an expression is expected to be a type. It is delimited by +the key {\tt type}, and bound to the coercion class {\tt Sortclass}. It is also +used in certain situations where an expression is statically known to +be a type, including the conclusion and the type of hypotheses within +an {\tt Ltac} goal match (see Section~\ref{ltac-match-goal}) +the statement of a theorem, the type of +a definition, the type of a binder, the domain and codomain of +implication, the codomain of products, and more generally any type +argument of a declared or defined constant. + +\subsection[The {\tt function\_scope} interpretation scope]{The {\tt function\_scope} interpretation scope\index{function\_scope@\texttt{function\_scope}}} + +The scope {\tt function\_scope} also has a special status. +It is temporarily activated each time the argument of a global reference is +recognized to be a {\tt Funclass instance}, i.e., of type {\tt forall x:A, B} or {\tt A -> B}. \subsection{Interpretation scopes used in the standard library of {\Coq}} @@ -953,38 +965,39 @@ commands {\tt Print Scopes} or {\tt Print Scope {\scope}}. \subsubsection{\tt type\_scope} -This includes infix {\tt *} for product types and infix {\tt +} for -sum types. It is delimited by key {\tt type}. +This scope includes infix {\tt *} for product types and infix {\tt +} for +sum types. It is delimited by key {\tt type}, and bound to the coercion class +{\tt Sortclass}, as described at \ref{bindscope}. \subsubsection{\tt nat\_scope} -This includes the standard arithmetical operators and relations on +This scope includes the standard arithmetical operators and relations on type {\tt nat}. Positive numerals in this scope are mapped to their canonical representent built from {\tt O} and {\tt S}. The scope is -delimited by key {\tt nat}. +delimited by key {\tt nat}, and bound to the type {\tt nat} (see \ref{bindscope}). \subsubsection{\tt N\_scope} -This includes the standard arithmetical operators and relations on +This scope includes the standard arithmetical operators and relations on type {\tt N} (binary natural numbers). It is delimited by key {\tt N} and comes with an interpretation for numerals as closed term of type {\tt Z}. \subsubsection{\tt Z\_scope} -This includes the standard arithmetical operators and relations on +This scope includes the standard arithmetical operators and relations on type {\tt Z} (binary integer numbers). It is delimited by key {\tt Z} and comes with an interpretation for numerals as closed term of type {\tt Z}. \subsubsection{\tt positive\_scope} -This includes the standard arithmetical operators and relations on +This scope includes the standard arithmetical operators and relations on type {\tt positive} (binary strictly positive numbers). It is delimited by key {\tt positive} and comes with an interpretation for numerals as closed term of type {\tt positive}. \subsubsection{\tt Q\_scope} -This includes the standard arithmetical operators and relations on +This scope includes the standard arithmetical operators and relations on type {\tt Q} (rational numbers defined as fractions of an integer and a strictly positive integer modulo the equality of the numerator-denominator cross-product). As for numerals, only $0$ and @@ -993,13 +1006,13 @@ interpretations are $\frac{0}{1}$ and $\frac{1}{1}$ respectively). \subsubsection{\tt Qc\_scope} -This includes the standard arithmetical operators and relations on the +This scope includes the standard arithmetical operators and relations on the type {\tt Qc} of rational numbers defined as the type of irreducible fractions of an integer and a strictly positive integer. \subsubsection{\tt real\_scope} -This includes the standard arithmetical operators and relations on +This scope includes the standard arithmetical operators and relations on type {\tt R} (axiomatic real numbers). It is delimited by key {\tt R} and comes with an interpretation for numerals as term of type {\tt R}. The interpretation is based on the binary decomposition. The @@ -1014,35 +1027,40 @@ those of {\tt R}. \subsubsection{\tt bool\_scope} -This includes notations for the boolean operators. It is -delimited by key {\tt bool}. +This scope includes notations for the boolean operators. It is +delimited by key {\tt bool}, and bound to the type {\tt bool} (see \ref{bindscope}). \subsubsection{\tt list\_scope} -This includes notations for the list operators. It is -delimited by key {\tt list}. +This scope includes notations for the list operators. It is +delimited by key {\tt list}, and bound to the type {\tt list} (see \ref{bindscope}). + +\subsubsection{\tt function\_scope} + +This scope is delimited by the key {\tt function}, and bound to the coercion class {\tt Funclass}, +as described at \ref{bindscope}. \subsubsection{\tt core\_scope} -This includes the notation for pairs. It is delimited by key {\tt core}. +This scope includes the notation for pairs. It is delimited by key {\tt core}. \subsubsection{\tt string\_scope} -This includes notation for strings as elements of the type {\tt +This scope includes notation for strings as elements of the type {\tt string}. Special characters and escaping follow {\Coq} conventions on strings (see Section~\ref{strings}). Especially, there is no convention to visualize non printable characters of a string. The file {\tt String.v} shows an example that contains quotes, a newline -and a beep (i.e. the ascii character of code 7). +and a beep (i.e. the ASCII character of code 7). \subsubsection{\tt char\_scope} -This includes interpretation for all strings of the form -\verb!"!$c$\verb!"! where $c$ is an ascii character, or of the form +This scope includes interpretation for all strings of the form +\verb!"!$c$\verb!"! where $c$ is an ASCII character, or of the form \verb!"!$nnn$\verb!"! where $nnn$ is a three-digits number (possibly with leading 0's), or of the form \verb!""""!. Their respective -denotations are the ascii code of $c$, the decimal ascii code $nnn$, -or the ascii code of the character \verb!"! (i.e. the ascii code +denotations are the ASCII code of $c$, the decimal ASCII code $nnn$, +or the ASCII code of the character \verb!"! (i.e. the ASCII code 34), all of them being represented in the type {\tt ascii}. \subsection{Displaying informations about scopes} diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index be75dc9d5..4931ca3b6 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1515,23 +1515,33 @@ The {\tt evar} tactic creates a new local definition named \ident\ with type \term\ in the context. The body of this binding is a fresh existential variable. -\subsection{\tt instantiate ( {\num} := {\term} )} +\subsection{\tt instantiate ( {\ident} := {\term} )} \tacindex{instantiate} \label{instantiate} The {\tt instantiate} tactic refines (see Section~\ref{refine}) -an existential variable -with the term \term. The \num\ argument is the position of the -existential variable from right to left in the conclusion. This cannot be -the number of the existential variable since this number is different -in every session. +an existential variable {\ident} with the term {\term}. +It is equivalent to {\tt only [\ident]: refine \term} (preferred alternative). -When you are referring to hypotheses which you did not name +\begin{Remarks} +\item To be able to refer to an existential variable by name, the +user must have given the name explicitly (see~\ref{ExistentialVariables}). + +\item When you are referring to hypotheses which you did not name explicitly, be aware that Coq may make a different decision on how to name the variable in the current goal and in the context of the existential variable. This can lead to surprising behaviors. +\end{Remarks} \begin{Variants} + + \item {\tt instantiate ( {\num} := {\term} )} + This variant allows to refer to an existential variable which was not + named by the user. The {\num} argument is the position of the + existential variable from right to left in the goal. + Because this variant is not robust to slight changes in the goal, + its use is strongly discouraged. + \item {\tt instantiate ( {\num} := {\term} ) in \ident} \item {\tt instantiate ( {\num} := {\term} ) in ( Value of {\ident} )} diff --git a/engine/evd.ml b/engine/evd.ml index ccce584bb..cfc9aa635 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -780,8 +780,9 @@ let new_sort_variable ?loc ?name rigid d = let add_global_univ d u = { d with universes = UState.add_global_univ d.universes u } -let make_flexible_variable evd b u = - { evd with universes = UState.make_flexible_variable evd.universes b u } +let make_flexible_variable evd ~algebraic u = + { evd with universes = + UState.make_flexible_variable evd.universes ~algebraic u } let make_evar_universe_context e l = let uctx = UState.make (Environ.universes e) in diff --git a/engine/evd.mli b/engine/evd.mli index 52327843c..3f00a3b0b 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -522,7 +522,9 @@ val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_ val add_global_univ : evar_map -> Univ.Level.t -> evar_map val universe_rigidity : evar_map -> Univ.Level.t -> rigid -val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map +val make_flexible_variable : evar_map -> algebraic:bool -> Univ.universe_level -> evar_map +(** See [UState.make_flexible_variable] *) + val is_sort_variable : evar_map -> sorts -> Univ.universe_level option (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is not a local sort variable declared in [evm] *) diff --git a/engine/uState.ml b/engine/uState.ml index 0973ca457..63bd247d5 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -384,16 +384,21 @@ let add_global_univ uctx u = uctx_initial_universes = initial; uctx_universes = univs } -let make_flexible_variable ctx b u = - let {uctx_univ_variables = uvars; uctx_univ_algebraic = avars} = ctx in +let make_flexible_variable ctx ~algebraic u = + let {uctx_local = cstrs; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} = ctx in let uvars' = Univ.LMap.add u None uvars in let avars' = - if b then + if algebraic then let uu = Univ.Universe.make u in let substu_not_alg u' v = Option.cata (fun vu -> Univ.Universe.equal uu vu && not (Univ.LSet.mem u' avars)) false v in - if not (Univ.LMap.exists substu_not_alg uvars) + let has_upper_constraint () = + Univ.Constraint.exists + (fun (l,d,r) -> d == Univ.Lt && Univ.Level.equal l u) + (Univ.ContextSet.constraints cstrs) + in + if not (Univ.LMap.exists substu_not_alg uvars || has_upper_constraint ()) then Univ.LSet.add u avars else avars else avars in diff --git a/engine/uState.mli b/engine/uState.mli index 0cdc6277a..3776e4c9f 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -92,7 +92,14 @@ val emit_side_effects : Safe_typing.private_constants -> t -> t val new_univ_variable : ?loc:Loc.t -> rigid -> string option -> t -> t * Univ.Level.t val add_global_univ : t -> Univ.Level.t -> t -val make_flexible_variable : t -> bool -> Univ.Level.t -> t + +(** [make_flexible_variable g algebraic l] + + Turn the variable [l] flexible, and algebraic if [algebraic] is true + and [l] can be. That is if there are no strict upper constraints on + [l] and and it does not appear in the instance of any non-algebraic + universe. Otherwise the variable is just made flexible. *) +val make_flexible_variable : t -> algebraic:bool -> Univ.Level.t -> t val is_sort_variable : t -> Sorts.t -> Univ.Level.t option diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index d42364001..cb2b365a4 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -20,9 +20,8 @@ module CompactedDecl = Context.Compacted.Declaration (** Ide_slave : an implementation of [Interface], i.e. mainly an interp function and a rewind function. This specialized loop is triggered - when the -ideslave option is passed to Coqtop. Currently CoqIDE is - the only one using this mode, but we try here to be as generic as - possible, so this may change in the future... *) + when the -ideslave option is passed to Coqtop. *) + (** Signal handling: we postpone ^C during input and output phases, but make it directly raise a Sys.Break during evaluation of the request. *) @@ -65,7 +64,7 @@ let is_known_option cmd = match cmd with (** Check whether a command is forbidden in the IDE *) let ide_cmd_checks ~id (loc,ast) = - let user_error s = CErrors.user_err ?loc ~hdr:"CoqIde" (str s) in + let user_error s = CErrors.user_err ?loc ~hdr:"IDE" (str s) in let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in if is_debug ast then user_error "Debug mode not available in the IDE"; @@ -509,4 +508,4 @@ let () = Coqtop.toploop_run := loop let () = Usage.add_to_usage "coqidetop" " --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format\ -\n --help-XML-protocol print the documentation of the XML protocol used by CoqIDE\n" +\n --help-XML-protocol print documentation of the Coq XML protocol\n" diff --git a/ide/preferences.ml b/ide/preferences.ml index 95c03b9fc..7c251f79c 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -407,11 +407,15 @@ let opposite_tabs = let background_color = new preference ~name:["background_color"] ~init:"cornsilk" ~repr:Repr.(string) +let attach_tag (pref : string preference) (tag : GText.tag) f = + tag#set_property (f pref#get); + pref#connect#changed ~callback:(fun c -> tag#set_property (f c)) + let attach_bg (pref : string preference) (tag : GText.tag) = - pref#connect#changed ~callback:(fun c -> tag#set_property (`BACKGROUND c)) + attach_tag pref tag (fun c -> `BACKGROUND c) let attach_fg (pref : string preference) (tag : GText.tag) = - pref#connect#changed ~callback:(fun c -> tag#set_property (`FOREGROUND c)) + attach_tag pref tag (fun c -> `FOREGROUND c) let processing_color = new preference ~name:["processing_color"] ~init:"light blue" ~repr:Repr.(string) diff --git a/interp/notation.ml b/interp/notation.ml index f2b99513a..4067a6b94 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -582,11 +582,12 @@ let interpretation_eq (vars1, t1) (vars2, t2) = List.equal var_attributes_eq vars1 vars2 && Notation_ops.eq_notation_constr (List.map fst vars1, List.map fst vars2) t1 t2 -let exists_notation_in_scope scopt ntn r = +let exists_notation_in_scope scopt ntn onlyprint r = let scope = match scopt with Some s -> s | None -> default_scope in try let sc = String.Map.find scope !scope_map in let n = String.Map.find ntn sc.notations in + onlyprint = n.not_onlyprinting && interpretation_eq n.not_interp r with Not_found -> false diff --git a/interp/notation.mli b/interp/notation.mli index a1dcb2034..dd0144e8d 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -148,7 +148,7 @@ val interp_notation_as_global_reference : ?loc:Loc.t -> (global_reference -> boo (** Checks for already existing notations *) val exists_notation_in_scope : scope_name option -> notation -> - interpretation -> bool + bool -> interpretation -> bool (** Declares and looks for scopes associated to arguments of a global ref *) val declare_arguments_scope : diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 1931e8167..5d703011d 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -22,9 +22,16 @@ open Notation_term (**********************************************************************) (* Utilities *) +(* helper for NVar, NVar case in eq_notation_constr *) +let get_var_ndx id vs = try Some (List.index Id.equal id vs) with Not_found -> None + let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with | NRef gr1, NRef gr2 -> eq_gr gr1 gr2 -| NVar id1, NVar id2 -> Int.equal (List.index Id.equal id1 vars1) (List.index Id.equal id2 vars2) +| NVar id1, NVar id2 -> ( + match (get_var_ndx id1 vars1,get_var_ndx id2 vars2) with + | Some n,Some m -> Int.equal n m + | None ,None -> Id.equal id1 id2 + | _ -> false) | NApp (t1, a1), NApp (t2, a2) -> (eq_notation_constr vars) t1 t2 && List.equal (eq_notation_constr vars) a1 a2 | NHole (_, _, _), NHole (_, _, _) -> true (** FIXME? *) diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml index a9849819b..ff7145267 100644 --- a/lib/cWarnings.ml +++ b/lib/cWarnings.ml @@ -35,28 +35,6 @@ let add_warning_in_category ~name ~category = in Hashtbl.replace categories category (name::ws) -let create ~name ~category ?(default=Enabled) pp = - Hashtbl.add warnings name { default; category; status = default }; - add_warning_in_category ~name ~category; - if default <> Disabled then - add_warning_in_category ~name ~category:"default"; - fun ?loc x -> - let w = Hashtbl.find warnings name in - let loc = Option.append loc !current_loc in - match w.status with - | Disabled -> () - | AsError -> CErrors.user_err ?loc (pp x) - | Enabled -> - let msg = - pp x ++ spc () ++ str "[" ++ str name ++ str "," ++ - str category ++ str "]" - in - Feedback.msg_warning ?loc msg - -let warn_unknown_warning = - create ~name:"unknown-warning" ~category:"toplevel" - (fun name -> strbrk "Unknown warning name: " ++ str name) - let set_warning_status ~name status = try let w = Hashtbl.find warnings name in @@ -111,12 +89,6 @@ let set_status ~name status = let split_flags s = let reg = Str.regexp "[ ,]+" in Str.split reg s -let check_warning ~silent (_status,name) = - is_all_keyword name || - Hashtbl.mem categories name || - Hashtbl.mem warnings name || - (if not silent then warn_unknown_warning name; false) - (** [cut_before_all_rev] removes all flags subsumed by a later occurrence of the "all" flag, and reverses the list. *) let rec cut_before_all_rev acc = function @@ -143,10 +115,9 @@ let uniquize_flags_rev flags = | [] -> acc in aux [] CString.Set.empty flags -(** [normalize_flags] removes unknown or redundant warnings. If [silent] is - true, it emits a warning when an unknown warning is met. *) +(** [normalize_flags] removes redundant warnings. Unknown warnings are kept + because they may be declared in a plugin that will be linked later. *) let normalize_flags ~silent warnings = - let warnings = List.filter (check_warning ~silent) warnings in let warnings = cut_before_all_rev warnings in uniquize_flags_rev warnings @@ -179,3 +150,27 @@ let parse_flags s = let set_flags s = reset_default_warnings (); let s = parse_flags s in flags := s + +(* Adds a warning to the [warnings] and [category] tables. We then reparse the + warning flags string, because the warning being created might have been set + already. *) +let create ~name ~category ?(default=Enabled) pp = + Hashtbl.replace warnings name { default; category; status = default }; + add_warning_in_category ~name ~category; + if default <> Disabled then + add_warning_in_category ~name ~category:"default"; + (* We re-parse and also re-normalize the flags, because the category of the + new warning is now known. *) + set_flags !flags; + fun ?loc x -> + let w = Hashtbl.find warnings name in + let loc = Option.append loc !current_loc in + match w.status with + | Disabled -> () + | AsError -> CErrors.user_err ?loc (pp x) + | Enabled -> + let msg = + pp x ++ spc () ++ str "[" ++ str name ++ str "," ++ + str category ++ str "]" + in + Feedback.msg_warning ?loc msg diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 92d78f6b2..9f4829761 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -70,7 +70,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) else t | UnivFlexible alg -> if onlyalg && alg then - (evdref := Evd.make_flexible_variable !evdref false l; t) + (evdref := Evd.make_flexible_variable !evdref ~algebraic:false l; t) else t)) | Prop Pos when refreshset && not direction -> (* Cannot make a universe "lower" than "Set", diff --git a/test-suite/bugs/closed/5205.v b/test-suite/bugs/closed/5205.v new file mode 100644 index 000000000..406f37a4b --- /dev/null +++ b/test-suite/bugs/closed/5205.v @@ -0,0 +1,6 @@ +Definition foo (n : nat) (m : nat) : nat := m. + +Arguments foo {_} _, _ _. + +Check foo 1 1. +Check foo (n:=1) 1. diff --git a/test-suite/bugs/closed/5365.v b/test-suite/bugs/closed/5365.v new file mode 100644 index 000000000..be360d24d --- /dev/null +++ b/test-suite/bugs/closed/5365.v @@ -0,0 +1,13 @@ + +Inductive TupleT : nat -> Type := +| nilT : TupleT 0 +| consT {n} A : (A -> TupleT n) -> TupleT (S n). + +Inductive Tuple : forall n, TupleT n -> Type := + nil : Tuple _ nilT +| cons {n A} (x : A) (F : A -> TupleT n) : Tuple _ (F x) -> Tuple _ (consT A F). + +Inductive TupleMap : forall n, TupleT n -> TupleT n -> Type := + tmNil : TupleMap _ nilT nilT +| tmCons {n} {A B : Type} (F : A -> TupleT n) (G : B -> TupleT n) + : (forall x, sigT (fun y => TupleMap _ (F x) (G y))) -> TupleMap _ (consT A F) (consT B G). diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index 2ccca829d..b9985a594 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -1,3 +1,14 @@ +(* Bug 5568, don't warn for notations in repeated module import *) + +Module foo. +Notation compose := (fun g f => g f). +Notation "g & f" := (compose g f) (at level 10). +End foo. + +Import foo. +Import foo. +Import foo. + (**********************************************************************) (* Notations for if and let (submitted by Roland Zumkeller) *) diff --git a/test-suite/output/RecognizePluginWarning.out b/test-suite/output/RecognizePluginWarning.out new file mode 100644 index 000000000..e69de29bb --- /dev/null +++ b/test-suite/output/RecognizePluginWarning.out diff --git a/test-suite/output/RecognizePluginWarning.v b/test-suite/output/RecognizePluginWarning.v new file mode 100644 index 000000000..cd667bbd0 --- /dev/null +++ b/test-suite/output/RecognizePluginWarning.v @@ -0,0 +1,5 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "extraction-logical-axiom") -*- *) + +(* Test that mentioning a warning defined in plugins works. The failure +mode here is that these result in a warning about unknown warnings, since the +plugins are not known at command line parsing time. *) diff --git a/test-suite/output/UsePluginWarning.out b/test-suite/output/UsePluginWarning.out new file mode 100644 index 000000000..47409f3ec --- /dev/null +++ b/test-suite/output/UsePluginWarning.out @@ -0,0 +1 @@ +type foo = __ diff --git a/test-suite/output/UsePluginWarning.v b/test-suite/output/UsePluginWarning.v new file mode 100644 index 000000000..c6e005464 --- /dev/null +++ b/test-suite/output/UsePluginWarning.v @@ -0,0 +1,7 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-extraction-logical-axiom") -*- *) + +Require Extraction. +Axiom foo : Prop. + +Extraction foo. + diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index b800953b8..8eeb59898 100644 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -46,10 +46,9 @@ } let space = [' ' '\t' '\n' '\r'] -let lowercase = ['a'-'z' '\223'-'\246' '\248'-'\255'] -let uppercase = ['A'-'Z' '\192'-'\214' '\216'-'\222'] -let identchar = - ['A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9'] +let lowercase = ['a'-'z'] +let uppercase = ['A'-'Z'] +let identchar = ['A'-'Z' 'a'-'z' '_' '\'' '0'-'9'] let caml_up_ident = uppercase identchar* let caml_low_ident = lowercase identchar* diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll index 5d11e3008..308bb582a 100644 --- a/tools/ocamllibdep.mll +++ b/tools/ocamllibdep.mll @@ -20,10 +20,9 @@ } let space = [' ' '\t' '\n' '\r'] -let lowercase = ['a'-'z' '\223'-'\246' '\248'-'\255'] -let uppercase = ['A'-'Z' '\192'-'\214' '\216'-'\222'] -let identchar = - ['A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9'] +let lowercase = ['a'-'z'] +let uppercase = ['A'-'Z'] +let identchar = ['A'-'Z' 'a'-'z' '_' '\'' '0'-'9'] let caml_up_ident = uppercase identchar* let caml_low_ident = lowercase identchar* diff --git a/vernac/command.ml b/vernac/command.ml index 0a82a945a..e04bebe33 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -383,7 +383,7 @@ let make_conclusion_flexible evdref ty poly = | Type u -> (match Univ.universe_level u with | Some u -> - evdref := Evd.make_flexible_variable !evdref true u + evdref := Evd.make_flexible_variable !evdref ~algebraic:true u | None -> ()) | _ -> () else () diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index ae662d74b..567fc57fa 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1164,11 +1164,11 @@ let open_notation i (_, nobj) = let scope = nobj.notobj_scope in let (ntn, df) = nobj.notobj_notation in let pat = nobj.notobj_interp in - let fresh = not (Notation.exists_notation_in_scope scope ntn pat) in + let onlyprint = nobj.notobj_onlyprint in + let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in let active = is_active_compat nobj.notobj_compat in if Int.equal i 1 && fresh && active then begin (* Declare the interpretation *) - let onlyprint = nobj.notobj_onlyprint in let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint in (* Declare the uninterpretation *) if not nobj.notobj_onlyparse then diff --git a/vernac/record.ml b/vernac/record.ml index 218cf7a0a..d61f44cac 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -124,7 +124,7 @@ let typecheck_params_and_fields finite def id pl t ps nots fs = let s' = EConstr.ESorts.kind !evars s' in (if poly then match Evd.is_sort_variable !evars s' with - | Some l -> evars := Evd.make_flexible_variable !evars true l; + | Some l -> evars := Evd.make_flexible_variable !evars ~algebraic:true l; s, s', true | None -> s, s', false else s, s', false) |