diff options
Diffstat (limited to 'dev/build')
38 files changed, 221 insertions, 1046 deletions
diff --git a/dev/build/windows/MakeCoq_84pl6_abs_ocaml.bat b/dev/build/windows/MakeCoq_84pl6_abs_ocaml.bat deleted file mode 100644 index 9dbce1920f..0000000000 --- a/dev/build/windows/MakeCoq_84pl6_abs_ocaml.bat +++ /dev/null @@ -1,28 +0,0 @@ -@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -mode=absolute ^
- -ocaml=Y ^
- -make=Y ^
- -coqver=8.4pl6 ^
- -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 deleted file mode 100644 index 7faf3e9ce1..0000000000 --- a/dev/build/windows/MakeCoq_85pl2_abs_ocaml.bat +++ /dev/null @@ -1,28 +0,0 @@ -@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -mode=absolute ^
- -ocaml=Y ^
- -make=Y ^
- -coqver=8.5pl2 ^
- -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 deleted file mode 100644 index b719b14c53..0000000000 --- a/dev/build/windows/MakeCoq_85pl3_abs_ocaml.bat +++ /dev/null @@ -1,28 +0,0 @@ -@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -mode=absolute ^
- -ocaml=Y ^
- -make=Y ^
- -coqver=8.5pl3 ^
- -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 deleted file mode 100644 index a9f4e2da2e..0000000000 --- a/dev/build/windows/MakeCoq_85pl3_installer.bat +++ /dev/null @@ -1,26 +0,0 @@ -@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -installer=Y ^
- -coqver=8.5pl3 ^
- -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 deleted file mode 100644 index ef593cc63a..0000000000 --- a/dev/build/windows/MakeCoq_85pl3_installer_32.bat +++ /dev/null @@ -1,26 +0,0 @@ -@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=32 ^
- -installer=Y ^
- -coqver=8.5pl3 ^
- -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_86_abs_ocaml.bat b/dev/build/windows/MakeCoq_86_abs_ocaml.bat deleted file mode 100644 index 50483c4d4a..0000000000 --- a/dev/build/windows/MakeCoq_86_abs_ocaml.bat +++ /dev/null @@ -1,10 +0,0 @@ -call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -mode=absolute ^
- -ocaml=Y ^
- -make=Y ^
- -coqver=8.6 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_86_abs ^
- -destcoq=%ROOTPATH%\coq64_86_abs
diff --git a/dev/build/windows/MakeCoq_86_installer.bat b/dev/build/windows/MakeCoq_86_installer.bat deleted file mode 100644 index 263520ff14..0000000000 --- a/dev/build/windows/MakeCoq_86_installer.bat +++ /dev/null @@ -1,8 +0,0 @@ -call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -installer=Y ^
- -coqver=8.6 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_86_inst ^
- -destcoq=%ROOTPATH%\coq64_86_inst
diff --git a/dev/build/windows/MakeCoq_86_installer_32.bat b/dev/build/windows/MakeCoq_86_installer_32.bat deleted file mode 100644 index 14921dd7c3..0000000000 --- a/dev/build/windows/MakeCoq_86_installer_32.bat +++ /dev/null @@ -1,8 +0,0 @@ -call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=32 ^
- -installer=Y ^
- -coqver=8.6 ^
- -destcyg=%ROOTPATH%\cygwin_coq32_86_inst ^
- -destcoq=%ROOTPATH%\coq32_86_inst
diff --git a/dev/build/windows/MakeCoq_86beta1_abs_ocaml.bat b/dev/build/windows/MakeCoq_86beta1_abs_ocaml.bat deleted file mode 100644 index 914c332f46..0000000000 --- a/dev/build/windows/MakeCoq_86beta1_abs_ocaml.bat +++ /dev/null @@ -1,10 +0,0 @@ -call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -mode=absolute ^
- -ocaml=Y ^
- -make=Y ^
- -coqver=8.6beta1 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_86beta1_abs ^
- -destcoq=%ROOTPATH%\coq64_86beta1_abs
diff --git a/dev/build/windows/MakeCoq_86beta1_installer.bat b/dev/build/windows/MakeCoq_86beta1_installer.bat deleted file mode 100644 index 76a5bb35ac..0000000000 --- a/dev/build/windows/MakeCoq_86beta1_installer.bat +++ /dev/null @@ -1,8 +0,0 @@ -call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -installer=Y ^
- -coqver=8.6beta1 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_86beta1_inst ^
- -destcoq=%ROOTPATH%\coq64_86beta1_inst
diff --git a/dev/build/windows/MakeCoq_86beta1_installer_32.bat b/dev/build/windows/MakeCoq_86beta1_installer_32.bat deleted file mode 100644 index f53232b651..0000000000 --- a/dev/build/windows/MakeCoq_86beta1_installer_32.bat +++ /dev/null @@ -1,8 +0,0 @@ -call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=32 ^
- -installer=Y ^
- -coqver=8.6beta1 ^
- -destcyg=%ROOTPATH%\cygwin_coq32_86beta1_inst ^
- -destcoq=%ROOTPATH%\coq32_86beta1_inst
diff --git a/dev/build/windows/MakeCoq_86git_abs_ocaml.bat b/dev/build/windows/MakeCoq_86git_abs_ocaml.bat deleted file mode 100644 index 99a1f156b0..0000000000 --- a/dev/build/windows/MakeCoq_86git_abs_ocaml.bat +++ /dev/null @@ -1,28 +0,0 @@ -@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -mode=absolute ^
- -ocaml=Y ^
- -make=Y ^
- -coqver=git-v8.6 ^
- -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 deleted file mode 100644 index 896d1cd633..0000000000 --- a/dev/build/windows/MakeCoq_86git_abs_ocaml_gtksrc.bat +++ /dev/null @@ -1,29 +0,0 @@ -@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -mode=absolute ^
- -ocaml=Y ^
- -make=Y ^
- -gtksrc=Y ^
- -coqver=git-v8.6 ^
- -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 deleted file mode 100644 index c4823103f1..0000000000 --- a/dev/build/windows/MakeCoq_86git_installer.bat +++ /dev/null @@ -1,26 +0,0 @@ -@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -installer=Y ^
- -coqver=git-v8.6 ^
- -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_installer2.bat b/dev/build/windows/MakeCoq_86git_installer2.bat deleted file mode 100644 index d184f0e30e..0000000000 --- a/dev/build/windows/MakeCoq_86git_installer2.bat +++ /dev/null @@ -1,8 +0,0 @@ -call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -installer=Y ^
- -coqver=git-v8.6 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_86git_inst2 ^
- -destcoq=%ROOTPATH%\coq64_86git_inst2
diff --git a/dev/build/windows/MakeCoq_86git_installer_32.bat b/dev/build/windows/MakeCoq_86git_installer_32.bat deleted file mode 100644 index 19146c96c9..0000000000 --- a/dev/build/windows/MakeCoq_86git_installer_32.bat +++ /dev/null @@ -1,26 +0,0 @@ -@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=32 ^
- -installer=Y ^
- -coqver=git-v8.6 ^
- -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 deleted file mode 100755 index cf6cafaa02..0000000000 --- a/dev/build/windows/MakeCoq_86git_installer_cyglocal.bat +++ /dev/null @@ -1,27 +0,0 @@ -@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -installer=Y ^
- -coqver=git-v8.6 ^
- -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_86rc1_abs_ocaml.bat b/dev/build/windows/MakeCoq_86rc1_abs_ocaml.bat deleted file mode 100644 index c0669f01d2..0000000000 --- a/dev/build/windows/MakeCoq_86rc1_abs_ocaml.bat +++ /dev/null @@ -1,10 +0,0 @@ -call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -mode=absolute ^
- -ocaml=Y ^
- -make=Y ^
- -coqver=8.6rc1 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_86rc1_abs ^
- -destcoq=%ROOTPATH%\coq64_86rc1_abs
diff --git a/dev/build/windows/MakeCoq_86rc1_installer.bat b/dev/build/windows/MakeCoq_86rc1_installer.bat deleted file mode 100644 index 66234ebbde..0000000000 --- a/dev/build/windows/MakeCoq_86rc1_installer.bat +++ /dev/null @@ -1,8 +0,0 @@ -call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -installer=Y ^
- -coqver=8.6rc1 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_86rc1_inst ^
- -destcoq=%ROOTPATH%\coq64_86rc1_inst
diff --git a/dev/build/windows/MakeCoq_86rc1_installer_32.bat b/dev/build/windows/MakeCoq_86rc1_installer_32.bat deleted file mode 100644 index 96f43e16a5..0000000000 --- a/dev/build/windows/MakeCoq_86rc1_installer_32.bat +++ /dev/null @@ -1,8 +0,0 @@ -call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=32 ^
- -installer=Y ^
- -coqver=8.6rc1 ^
- -destcyg=%ROOTPATH%\cygwin_coq32_86rc1_inst ^
- -destcoq=%ROOTPATH%\coq32_86rc1_inst
diff --git a/dev/build/windows/MakeCoq_88git_installer.bat b/dev/build/windows/MakeCoq_88git_installer.bat deleted file mode 100755 index b016fb3891..0000000000 --- a/dev/build/windows/MakeCoq_88git_installer.bat +++ /dev/null @@ -1,27 +0,0 @@ -@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== BUILD COQ ==========
-
-call MakeCoq_SetRootPath
-
-call MakeCoq_MinGW.bat ^
- -arch=64 ^
- -installer=Y ^
- -coqver=git-v8.8 ^
- -destcyg=%ROOTPATH%\cygwin_coq64_88_inst ^
- -destcoq=%ROOTPATH%\coq64_88_inst ^
- -addon=bignums
-
-IF %ERRORLEVEL% NEQ 0 (
- ECHO MakeCoq_88git_installer.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 33feeed45c..c3f3a97ff5 100755 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -55,7 +55,7 @@ IF DEFINED HTTP_PROXY ( )
REM see -cygrepo in ReadMe.txt
-SET CYGWIN_REPOSITORY=http://ftp.inf.tu-dresden.de/software/windows/cygwin32
+SET CYGWIN_REPOSITORY=http://mirror.easyname.at/cygwin
REM see -cygcache in ReadMe.txt
SET CYGWIN_LOCAL_CACHE_WFMT=%BATCHDIR%cygwin_cache
@@ -331,7 +331,7 @@ IF "%CYGWIN_QUIET%" == "Y" ( )
IF "%GTK_FROM_SOURCES%"=="N" (
- SET CYGWIN_OPT= %CYGWIN_OPT% -P mingw64-%ARCH%-gtk2.0,mingw64-%ARCH%-gtksourceview2.0
+ SET CYGWIN_OPT= %CYGWIN_OPT% -P mingw64-%ARCH%-gtk3,mingw64-%ARCH%-gtksourceview3.0
)
REM Cygwin setup sets proper ACLs (permissions) for folders it CREATES.
@@ -373,7 +373,8 @@ IF "%RUNSETUP%"=="Y" ( -P make,unzip ^
-P gdb,liblzma5 ^
-P patch,automake1.14 ^
- -P mingw64-%ARCH%-binutils,mingw64-%ARCH%-gcc-core,mingw64-%ARCH%-gcc-g++,mingw64-%ARCH%-pkg-config,mingw64-%ARCH%-windows_default_manifest ^
+ -P pkg-config ^
+ -P mingw64-%ARCH%-binutils,mingw64-%ARCH%-gcc-core,mingw64-%ARCH%-gcc-g++,mingw64-%ARCH%-windows_default_manifest ^
-P mingw64-%ARCH%-headers,mingw64-%ARCH%-runtime,mingw64-%ARCH%-pthreads,mingw64-%ARCH%-zlib ^
-P libiconv-devel,libunistring-devel,libncurses-devel ^
-P gettext-devel,libgettextpo-devel ^
diff --git a/dev/build/windows/ReadMe.txt b/dev/build/windows/ReadMe.txt index 93851aeb8d..a392115ea4 100644 --- a/dev/build/windows/ReadMe.txt +++ b/dev/build/windows/ReadMe.txt @@ -369,8 +369,6 @@ Text files patched by the installer: Text files containing the install folder path after install: -./bin/mkcamlp5:LIB=D:/bin/coq64_buildtest_reloc_ocaml20/libocaml/camlp5 -./bin/mkcamlp5.opt:LIB=D:/bin/coq64_buildtest_reloc_ocaml20/libocaml/camlp5 ./libocaml/Makefile.config:PREFIX=D:/bin/coq64_buildtest_reloc_ocaml20 ./libocaml/Makefile.config:LIBDIR=D:/bin/coq64_buildtest_reloc_ocaml20/libocaml ./libocaml/site-lib/findlib/Makefile.config:OCAML_CORE_BIN=/cygdrive/d/bin/coq64_buildtest_reloc_ocaml20/bin @@ -382,8 +380,6 @@ Text files containing the install folder path after install: ./libocaml/topfind: Topdirs.dir_load Format.err_formatter "D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib/findlib/findlib_top.cma"; ./libocaml/topfind:(* #load "D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib/findlib/findlib.cma";; *) ./libocaml/topfind:(* #load "D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib/findlib/findlib_top.cma";; *) -./man/man1/camlp5.1:These files are installed in the directory D:/bin/coq64_buildtest_reloc_ocaml20/libocaml/camlp5. -./man/man1/camlp5.1:D:/bin/coq64_buildtest_reloc_ocaml20/libocaml/camlp5 Binary files containing the build folder path after install: @@ -398,26 +394,6 @@ Binary file ./libocaml/ocamldoc/odoc_info.cma matches Binary files containing the install folder path after install: $ find . -type f -exec grep "coq64_buildtest_reloc_ocaml20" {} /dev/null \; -Binary file ./bin/camlp4.exe matches -Binary file ./bin/camlp4boot.exe matches -Binary file ./bin/camlp4o.exe matches -Binary file ./bin/camlp4o.opt.exe matches -Binary file ./bin/camlp4of.exe matches -Binary file ./bin/camlp4of.opt.exe matches -Binary file ./bin/camlp4oof.exe matches -Binary file ./bin/camlp4oof.opt.exe matches -Binary file ./bin/camlp4orf.exe matches -Binary file ./bin/camlp4orf.opt.exe matches -Binary file ./bin/camlp4r.exe matches -Binary file ./bin/camlp4r.opt.exe matches -Binary file ./bin/camlp4rf.exe matches -Binary file ./bin/camlp4rf.opt.exe matches -Binary file ./bin/camlp5.exe matches -Binary file ./bin/camlp5o.exe matches -Binary file ./bin/camlp5o.opt matches -Binary file ./bin/camlp5r.exe matches -Binary file ./bin/camlp5r.opt matches -Binary file ./bin/camlp5sch.exe matches Binary file ./bin/coqc.exe matches Binary file ./bin/coqchk.exe matches Binary file ./bin/coqdep.exe matches @@ -428,11 +404,7 @@ Binary file ./bin/coqtop.exe matches Binary file ./bin/coqworkmgr.exe matches Binary file ./bin/coq_makefile.exe matches Binary file ./bin/menhir matches -Binary file ./bin/mkcamlp4.exe matches Binary file ./bin/ocaml.exe matches -Binary file ./bin/ocamlbuild.byte.exe matches -Binary file ./bin/ocamlbuild.exe matches -Binary file ./bin/ocamlbuild.native.exe matches Binary file ./bin/ocamlc.exe matches Binary file ./bin/ocamlc.opt.exe matches Binary file ./bin/ocamldebug.exe matches @@ -455,17 +427,6 @@ Binary file ./lib/ide/ide_win32_stubs.o matches Binary file ./lib/lib/clib.a matches Binary file ./lib/lib/clib.cma matches Binary file ./lib/libcoqrun.a matches -Binary file ./libocaml/camlp4/camlp4fulllib.a matches -Binary file ./libocaml/camlp4/camlp4fulllib.cma matches -Binary file ./libocaml/camlp4/camlp4lib.a matches -Binary file ./libocaml/camlp4/camlp4lib.cma matches -Binary file ./libocaml/camlp4/camlp4o.cma matches -Binary file ./libocaml/camlp4/camlp4of.cma matches -Binary file ./libocaml/camlp4/camlp4oof.cma matches -Binary file ./libocaml/camlp4/camlp4orf.cma matches -Binary file ./libocaml/camlp4/camlp4r.cma matches -Binary file ./libocaml/camlp4/camlp4rf.cma matches -Binary file ./libocaml/camlp5/odyl.cma matches Binary file ./libocaml/compiler-libs/ocamlcommon.a matches Binary file ./libocaml/compiler-libs/ocamlcommon.cma matches Binary file ./libocaml/dynlink.cma matches diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index c3d895784e..4c5bd29236 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -434,7 +434,7 @@ function build_prep_overlay { # ------------------------------------------------------------------------------ function load_overlay_data { - if [ -n "${GITLAB_CI+}" ]; then + if [ -n "${GITLAB_CI-}" ]; then export CI_BRANCH="$CI_COMMIT_REF_NAME" if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]]; then export CI_PULL_REQUEST="${CI_BRANCH#pr-}" @@ -444,9 +444,6 @@ function load_overlay_data { else export CI_BRANCH="" export CI_PULL_REQUEST="" - # Used when building 8.8.0 with the latest scripts - export TRAVIS_BRANCH="" - export TRAVIS_PULL_REQUEST="" fi for overlay in /build/user-overlays/*.sh; do @@ -691,7 +688,7 @@ function installer_addon_end { # ------------------------------------------------------------------------------ function coq_set_timeouts_1000 { - find . -type f -name '*.v' -print0 | xargs -0 sed -i 's/timeout\s\+[0-9]\+/timeout 1000/' + find . -type f -name '*.v' -print0 | xargs -0 sed -i 's/timeout\s\+[0-9]\+/timeout 1000/g' } ###################### MODULE BUILD FUNCTIONS ##################### @@ -701,7 +698,7 @@ function coq_set_timeouts_1000 { function make_sed { if build_prep https://ftp.gnu.org/gnu/sed/ sed-4.2.2 tar.gz ; then logn configure ./configure - log1 make + log1 make $MAKE_OPT log2 make install log2 make clean build_post @@ -745,7 +742,7 @@ function make_fontconfig { ##### ICONV ##### function make_libiconv { - build_conf_make_inst http://ftp.gnu.org/pub/gnu/libiconv libiconv-1.14 tar.gz true + build_conf_make_inst http://ftp.gnu.org/pub/gnu/libiconv libiconv-1.15 tar.gz true } ##### UNISTRING ##### @@ -819,7 +816,9 @@ function make_glib { make_gettext make_libffi make_libpcre + build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/glib/2.57 glib-2.57.1 tar.xz true + } ##### ATK ##### @@ -827,7 +826,7 @@ function make_glib { function make_atk { make_gettext make_glib - build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/atk/2.29 atk-2.29.1 tar.xz true + build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/atk/2.30 atk-2.30.0 tar.xz true } ##### PIXBUF ##### @@ -840,7 +839,7 @@ function make_gdk-pixbuf { # CONFIGURE PARAMETERS # --with-included-loaders=yes statically links the image file format handlers # This avoids "Cannot open pixbuf loader module file '/usr/x86_64-w64-mingw32/sys-root/mingw/lib/gdk-pixbuf-2.0/2.10.0/loaders.cache': No such file or directory" - build_conf_make_inst http://ftp.gnome.org/pub/GNOME/sources/gdk-pixbuf/2.36 gdk-pixbuf-2.36.12 tar.xz true --with-included-loaders=yes + build_conf_make_inst http://ftp.gnome.org/pub/GNOME/sources/gdk-pixbuf/2.38 gdk-pixbuf-2.38.0 tar.xz true --with-included-loaders=yes } ##### CAIRO ##### @@ -851,7 +850,7 @@ function make_cairo { make_glib make_pixman make_fontconfig - build_conf_make_inst http://cairographics.org/releases rcairo-1.15.13 tar.xz true + build_conf_make_inst http://cairographics.org/releases rcairo-1.16.2 tar.xz true } ##### PANGO ##### @@ -860,37 +859,23 @@ function make_pango { make_cairo make_glib make_fontconfig - build_conf_make_inst http://ftp.gnome.org/pub/GNOME/sources/pango/1.42 pango-1.42.1 tar.xz true + build_conf_make_inst http://ftp.gnome.org/pub/GNOME/sources/pango/1.42 pango-1.42.4 tar.xz true } -##### GTK2 ##### +##### GTK3 ##### -function patch_gtk2 { - rm gtk/gtk.def -} +function make_gtk3 { -function make_gtk2 { - # Cygwin packet dependencies: gtk-update-icon-cache if [ "$GTK_FROM_SOURCES" == "Y" ]; then - make_glib - make_atk - make_pango - make_gdk-pixbuf - make_cairo - build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/gtk+/2.24 gtk+-2.24.32 tar.xz patch_gtk2 - fi -} -##### GTK3 ##### - -function make_gtk3 { - make_glib - make_atk - make_pango - make_gdk-pixbuf - make_cairo - make_libepoxy - build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/gtk+/3.22 gtk+-3.22.30 tar.xz true + make_glib + make_atk + make_pango + make_gdk-pixbuf + make_cairo + make_libepoxy + build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/gtk+/3.24 gtk+-3.24.5 tar.xz true + fi # make all incl. tests and examples runs through fine # make install fails with issue with @@ -921,17 +906,17 @@ function make_libxml2 { fi } -##### GTK-SOURCEVIEW2 ##### +##### GTK-SOURCEVIEW3 ##### -function make_gtk_sourceview2 { +function make_gtk_sourceview3 { # Cygwin packet dependencies: intltool # gtksourceview-2.11.2 requires GTK2 # gtksourceview-2.91.9 requires GTK3 # => We use gtksourceview-2.11.2 which seems to be the newest GTK2 based one if [ "$GTK_FROM_SOURCES" == "Y" ]; then - make_gtk2 + make_gtk3 make_libxml2 - build_conf_make_inst https://download.gnome.org/sources/gtksourceview/2.11 gtksourceview-2.11.2 tar.bz2 true + build_conf_make_inst https://download.gnome.org/sources/gtksourceview/3.24 gtksourceview-3.24.9 tar.bz2 true fi } @@ -980,7 +965,7 @@ function get_flex_dll_link_bin { # Build flexdll and flexlink from sources after building OCaml function make_flex_dll_link { - if build_prep https://github.com/alainfrisch/flexdll/releases/download/0.37/ flexdll-bin-0.37 zip ; then + if build_prep https://github.com/alainfrisch/flexdll/archive 0.37 tar.gz 1 flexdll-0.37 ; then if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then # shellcheck disable=SC2086 log1 make $MAKE_OPT build_mingw flexlink.exe @@ -1017,11 +1002,21 @@ function make_ln { fi } +##### ARCH-pkg-config replacement ##### + +# cygwin replaced ARCH-pkg-config with a shell script, which doesn't work e.g. for dune on Windows. +# This builds a binary replacement for the shell script and puts it into the bin_special folder. +# There is no global installation since it is module specific what pkg-config is needed under what name. + +function make_arch_pkg_config { + gcc -DARCH="$TARGET_ARCH" -o bin_special/pkg-config.exe $PATCHES/pkg-config.c +} + ##### OCAML ##### function make_ocaml { get_flex_dll_link_bin - if build_prep https://github.com/ocaml/ocaml/archive 4.07.0 tar.gz 1 ocaml-4.07.0 ; then + if build_prep https://github.com/ocaml/ocaml/archive 4.07.1 tar.gz 1 ocaml-4.07.1 ; then # See README.win32.adoc cp config/m-nt.h byterun/caml/m.h cp config/s-nt.h byterun/caml/s.h @@ -1076,7 +1071,6 @@ function make_ocaml { function make_ocaml_tools { make_findlib - make_camlp5 } ##### OCAML EXTRA LIBRARIES ##### @@ -1085,7 +1079,6 @@ function make_ocaml_libs { make_num make_findlib make_lablgtk - # make_stdint } ##### Ocaml num library ##### @@ -1107,7 +1100,7 @@ function make_ocamlbuild { make_ocaml if build_prep https://github.com/ocaml/ocamlbuild/archive 0.12.0 tar.gz 1 ocamlbuild-0.12.0; then log2 make configure OCAML_NATIVE=true OCAMLBUILD_PREFIX=$PREFIXOCAML OCAMLBUILD_BINDIR=$PREFIXOCAML/bin OCAMLBUILD_LIBDIR=$PREFIXOCAML/lib - log1 make + log1 make $MAKE_OPT log2 make install build_post fi @@ -1133,6 +1126,20 @@ function make_findlib { fi } +##### Dune build system ##### + +function make_dune { + make_ocaml + + if build_prep https://github.com/ocaml/dune/archive/ 1.6.3 tar.gz 1 dune-1.6.3 ; then + + log2 make release + log2 make install + + build_post + fi +} + ##### MENHIR Ocaml Parser Generator ##### function make_menhir { @@ -1147,108 +1154,44 @@ function make_menhir { fi } -##### CAMLP4 Ocaml Preprocessor ##### - -function make_camlp4 { - # OCaml up to 4.01 includes camlp4, from 4.02 it isn't included - # Check if command camlp4 exists, if not build camlp4 - if ! command camlp4 ; then - make_ocaml - make_findlib - if build_prep https://github.com/ocaml/camlp4/archive 4.06+2 tar.gz 1 camlp4-4.06+2 ; then - # See https://github.com/ocaml/camlp4/issues/41#issuecomment-112018910 - logn configure ./configure - # Note: camlp4 doesn't support -j 8, so don't pass MAKE_OPT - log2 make all - log2 make install - log2 make clean - build_post - fi - fi -} - -##### CAMLP5 Ocaml Preprocessor ##### - -function make_camlp5 { - make_ocaml - make_findlib - - if build_prep https://github.com/camlp5/camlp5/archive rel706 tar.gz 1 camlp5-rel706; then - logn configure ./configure - # Somehow my virus scanner has the boot.new/SAVED directory locked after the move for a second => repeat until success - sed -i 's/mv boot.new boot/until mv boot.new boot; do sleep 1; done/' Makefile - # shellcheck disable=SC2086 - log1 make world.opt $MAKE_OPT - log2 make install - # For some reason gramlib.a is not copied, but it is required by Coq - cp lib/gramlib.a "$PREFIXOCAML/libocaml/camlp5/" - # For some reason META is not copied, but it is required by coq_makefile - log2 make -C etc META - mkdir -p "$PREFIXOCAML/libocaml/site-lib/camlp5/" - cp etc/META "$PREFIXOCAML/libocaml/site-lib/camlp5/" - log2 make clean - build_post - fi -} - ##### LABLGTK Ocaml GTK binding ##### # Note: when rebuilding lablgtk by deleting the .finished file, # also delete <root>\usr\x86_64-w64-mingw32\sys-root\mingw\lib\site-lib # Otherwise make install fails -function make_lablgtk { - make_ocaml - make_findlib - # 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/1726 lablgtk-2.18.6 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" - - # lablgtk shows occasional errors with -j, so don't pass $MAKE_OPT - - # lablgtk binary needs to be stripped - otherwise flexdll goes wild - # Fix version 1: explicit strip after failed build - this randomly fails in CI - # See https://sympa.inria.fr/sympa/arc/caml-list/2015-10/msg00204.html - # logn make-world-pre make world || true - # $TARGET_ARCH-strip.exe --strip-unneeded src/dlllablgtk2.dll - - # Fix version 2: Strip by passing linker argument rather than explicit call to strip - # See https://github.com/alainfrisch/flexdll/issues/6 - # Argument to ocamlmklib: -ldopt "-link -Wl,-s" - # -ldopt is the okamlmklib linker prefix option - # -link is the flexlink linker prefix option - # -Wl, is the gcc (linker driver) linker prefix option - # -s is the gnu linker option for stripping symbols - # These changes are included in dev/build/windows/patches_coq/lablgtk-2.18.3.patch - - log2 make world - - # lablgtk does not escape FINDLIBDIR path, which can contain backslashes - sed -i "s|^FINDLIBDIR=.*|FINDLIBDIR=$PREFIXOCAML/libocaml/site-lib|" config.make +function make_ocaml_cairo2 { + if build_prep https://github.com/Chris00/ocaml-cairo/archive 0.6 tar.gz 1 ocaml_cairo2-0.6; then + make_arch_pkg_config - log2 make install - log2 make clean + log2 dune build cairo2.install + log2 dune install cairo2 + log2 dune clean build_post + fi } -##### Ocaml Stdint ##### - -function make_stdint { +function make_lablgtk { make_ocaml make_findlib - if build_prep https://github.com/andrenth/ocaml-stdint/archive 0.3.0 tar.gz 1 Stdint-0.3.0; then - # Note: the setup gets the proper install path from ocamlfind, but for whatever reason it wants - # to create an empty folder in some folder which defaults to C:\Program Files. - # The --preifx overrides this. Id didn't see any files created in /tmp/extra. - log_1_3 ocaml setup.ml -configure --prefix /tmp/extra - log_1_3 ocaml setup.ml -build - log_1_3 ocaml setup.ml -install - log_1_3 ocaml setup.ml -clean + make_dune + make_gtk3 + make_gtk_sourceview3 + make_ocaml_cairo2 + + if build_prep https://github.com/garrigue/lablgtk/archive 3.0.beta5 tar.gz 1 lablgtk-3.0.beta5 ; then + make_arch_pkg_config + + # lablgtk3 includes more packages that are not relevant for Coq, + # such as gtkspell + log2 dune build -p lablgtk3 + log2 dune install lablgtk3 + + log2 dune build -p lablgtk3-sourceview3 + log2 dune install lablgtk3-sourceview3 + + log2 dune clean build_post fi } @@ -1273,42 +1216,44 @@ function copy_coq_dlls { # Select all missing DLLs from the module list, right click "copy filenames" # Delay loaded DLLs from Windows can be ignored (hour-glass icon at begin of line) # Do this recursively until there are no further missing DLLs (File close + reopen) - # For running this quickly, just do "cd coq-<ver> ; call copy_coq_dlls ; cd .." at the end of this script. + # For running this quickly, just do "cd coq-<ver> ; copy_coq_dlls ; cd .." at the end of this script. # Do the same for coqc and ocamlc (usually doesn't result in additional files) - copy_coq_dll LIBATK-1.0-0.DLL copy_coq_dll LIBCAIRO-2.DLL - copy_coq_dll LIBEXPAT-1.DLL - copy_coq_dll LIBFFI-6.DLL copy_coq_dll LIBFONTCONFIG-1.DLL copy_coq_dll LIBFREETYPE-6.DLL - copy_coq_dll LIBGDK-WIN32-2.0-0.DLL + copy_coq_dll LIBGDK-3-0.DLL copy_coq_dll LIBGDK_PIXBUF-2.0-0.DLL - copy_coq_dll LIBGIO-2.0-0.DLL copy_coq_dll LIBGLIB-2.0-0.DLL - copy_coq_dll LIBGMODULE-2.0-0.DLL copy_coq_dll LIBGOBJECT-2.0-0.DLL - copy_coq_dll LIBGTK-WIN32-2.0-0.DLL - copy_coq_dll LIBINTL-8.DLL + copy_coq_dll LIBGTK-3-0.DLL + copy_coq_dll LIBGTKSOURCEVIEW-3.0-1.DLL copy_coq_dll LIBPANGO-1.0-0.DLL + copy_coq_dll LIBATK-1.0-0.DLL + copy_coq_dll LIBBZ2-1.DLL + copy_coq_dll LIBCAIRO-GOBJECT-2.DLL + copy_coq_dll LIBEPOXY-0.DLL + copy_coq_dll LIBEXPAT-1.DLL + copy_coq_dll LIBFFI-6.DLL + copy_coq_dll LIBGIO-2.0-0.DLL + copy_coq_dll LIBGMODULE-2.0-0.DLL + copy_coq_dll LIBINTL-8.DLL copy_coq_dll LIBPANGOCAIRO-1.0-0.DLL copy_coq_dll LIBPANGOWIN32-1.0-0.DLL - copy_coq_dll libpcre-1.dll + copy_coq_dll LIBPCRE-1.DLL copy_coq_dll LIBPIXMAN-1-0.DLL copy_coq_dll LIBPNG16-16.DLL copy_coq_dll LIBXML2-2.DLL copy_coq_dll ZLIB1.DLL + copy_coq_dll ICONV.DLL + copy_coq_dll LIBLZMA-5.DLL + copy_coq_dll LIBPANGOFT2-1.0-0.DLL + copy_coq_dll LIBHARFBUZZ-0.DLL # Depends on if GTK is built from sources if [ "$GTK_FROM_SOURCES" == "Y" ]; then - copy_coq_dll libiconv-2.dll - else - copy_coq_dll ICONV.DLL - copy_coq_dll LIBBZ2-1.DLL - copy_coq_dll LIBGTKSOURCEVIEW-2.0-0.DLL - copy_coq_dll LIBHARFBUZZ-0.DLL - copy_coq_dll LIBLZMA-5.DLL - copy_coq_dll LIBPANGOFT2-1.0-0.DLL + echo "Building GTK from sources is currently not supported" + exit 1 fi; # Architecture dependent files @@ -1338,14 +1283,14 @@ 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" +function copy_coq_gtk { + echo 'gtk-theme-name = "Default"' > "$PREFIX/etc/gtk-3.0/gtkrc" + echo 'gtk-fallback-icon-theme = "Tango"' >> "$PREFIX/etc/gtk-3.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_glob "$PREFIX/etc/gtk-3.0" '*' "$PREFIXCOQ/gtk-3.0" + install_glob "$PREFIX/share/gtksourceview-3.0/language-specs" '*' "$PREFIXCOQ/share/gtksourceview-3.0/language-specs" + install_glob "$PREFIX/share/gtksourceview-3.0/styles" '*' "$PREFIXCOQ/share/gtksourceview-3.0/styles" install_rec "$PREFIX/share/themes" '*' "$PREFIXCOQ/share/themes" # This below item look like a bug in make install @@ -1354,10 +1299,7 @@ function copq_coq_gtk { else COQSHARE="$PREFIXCOQ/share/" fi - if [[ ! $COQ_VERSION == 8.4* ]] ; then - mv "$COQSHARE"*.lang "$PREFIXCOQ/share/gtksourceview-2.0/language-specs" - mv "$COQSHARE"*.xml "$PREFIXCOQ/share/gtksourceview-2.0/styles" - fi + mkdir -p "$PREFIXCOQ/ide" mv "$COQSHARE"*.png "$PREFIXCOQ/ide" rmdir "$PREFIXCOQ/share/coq" || true @@ -1386,7 +1328,6 @@ function make_coq { make_ocaml make_num make_findlib - make_camlp5 make_lablgtk if case $COQ_VERSION in @@ -1440,11 +1381,12 @@ function make_coq { log2 make install log1 copy_coq_dlls + log1 copy_coq_gtk + if [ "$INSTALLOCAML" == "Y" ]; then copy_coq_objects fi - log1 copq_coq_gtk log1 copy_coq_license # make clean seems to be broken for 8.5pl2 @@ -1634,7 +1576,7 @@ function make_addon_bignums { installer_addon_section bignums "Bignums" "Coq library for fast arbitrary size numbers" "" # To make command lines shorter :-( echo 'COQ_SRC_SUBDIRS:=$(filter-out plugins/%,$(COQ_SRC_SUBDIRS)) plugins/syntax' >> Makefile.coq.local - log1 make all + log1 make $MAKE_OPT all log2 make install build_post fi @@ -1645,12 +1587,12 @@ function make_addon_bignums { function make_addon_equations { installer_addon_dependency equations - if build_prep_overlay Equations; then + if build_prep_overlay equations; then installer_addon_section equations "Equations" "Coq plugin for defining functions by equations" "" # Note: PATH is automatically saved/restored by build_prep / build_post PATH=$COQBIN:$PATH logn coq_makefile ${COQBIN}coq_makefile -f _CoqProject -o Makefile - log1 make + log1 make $MAKE_OPT log2 make install build_post fi @@ -1696,7 +1638,7 @@ function make_addon_ltac2 { installer_addon_dependency ltac2 if build_prep_overlay ltac2; then installer_addon_section ltac2 "Ltac-2" "Coq plugin with the Ltac-2 enhanced tactic language" "" - log1 make all + log1 make $MAKE_OPT all log2 make install build_post fi @@ -1709,7 +1651,7 @@ function make_addon_unicoq { if build_prep_overlay unicoq; then installer_addon_section unicoq "Unicoq" "Coq plugin for an enhanced unification algorithm" "" log1 coq_makefile -f Make -o Makefile - log1 make + log1 make $MAKE_OPT log2 make install build_post fi @@ -1724,7 +1666,7 @@ function make_addon_mtac2 { if build_prep_overlay mtac2; then installer_addon_section mtac2 "Mtac-2" "Coq plugin for a typed tactic language for Coq." "" log1 coq_makefile -f _CoqProject -o Makefile - log1 make + log1 make $MAKE_OPT log2 make install build_post fi @@ -1766,7 +1708,7 @@ function make_addon_menhirlib { echo -R . MenhirLib > _CoqProject ls -1 *.v >> _CoqProject log1 coq_makefile -f _CoqProject -o Makefile.coq - log1 make -f Makefile.coq all + log1 make -f Makefile.coq $MAKE_OPT all logn make-install make -f Makefile.coq install build_post fi @@ -1779,10 +1721,10 @@ function make_addon_compcert { make_menhir make_addon_menhirlib installer_addon_dependency_end - if build_prep_overlay CompCert; then + if build_prep_overlay compcert; then installer_addon_section compcert "CompCert" "ATTENTION: THIS IS NOT OPEN SOURCE! CompCert verified C compiler and Clightgen (required for using VST for your own code)" "off" logn configure ./configure -ignore-coq-version -clightgen -prefix "$PREFIXCOQ" -coqdevdir "$PREFIXCOQ/lib/coq/user-contrib/compcert" x86_32-cygwin - log1 make + log1 make $MAKE_OPT log2 make install logn install-license-1 install -D -T "LICENSE" "$PREFIXCOQ/lib/coq/user-contrib/compcert/LICENSE" logn install-license-2 install -D -T "LICENSE" "$PREFIXCOQ/lib/compcert/LICENSE" @@ -1807,8 +1749,8 @@ function install_addon_vst { install_glob "progs" '*.v' "$VSTDEST/progs/" install_glob "progs" '*.c' "$VSTDEST/progs/" install_glob "progs" '*.h' "$VSTDEST/progs/" - install_glob "veric" '*.v' "$VSTDEST/msl/" - install_glob "veric" '*.vo' "$VSTDEST/msl/" + install_glob "veric" '*.v' "$VSTDEST/veric/" + install_glob "veric" '*.vo' "$VSTDEST/veric/" # Install VST documentation files install_glob "." 'LICENSE' "$VSTDEST" @@ -1821,12 +1763,20 @@ function install_addon_vst { install_glob "." '_CoqProject-export' "$VSTDEST/progs" } +function vst_patch_compcert_refs { + find . -type f -name '*.v' -print0 | xargs -0 sed -E -i \ + -e 's/(Require\s+(Import\s+|Export\s+)*)compcert\./\1VST.compcert./g' \ + -e 's/From compcert Require/From VST.compcert Require/g' +} + function make_addon_vst { installer_addon_dependency vst - if build_prep_overlay VST; then + if build_prep_overlay vst; then installer_addon_section vst "VST" "ATTENTION: SOME INCLUDED COMPCERT PARTS ARE NOT OPEN SOURCE! Verified Software Toolchain for verifying C code" "off" - log1 coq_set_timeouts_1000 - log1 make IGNORECOQVERSION=true $MAKE_OPT + # log1 coq_set_timeouts_1000 + log1 vst_patch_compcert_refs + # The usage of the shell variable ARCH in VST collides with the usage in this shellscript + logn make env -u ARCH make IGNORECOQVERSION=true $MAKE_OPT log1 install_addon_vst build_post fi @@ -1851,9 +1801,9 @@ function make_addon_coquelicot { function make_addon_aactactics { installer_addon_dependency aac - if build_prep_overlay aactactics; then + if build_prep_overlay aac_tactics; then installer_addon_section aac "AAC" "Coq plugin for extensible associative and commutative rewriting" "" - log1 make + log1 make $MAKE_OPT log2 make install build_post fi @@ -1894,7 +1844,7 @@ function make_addon_quickchick { installer_addon_dependency_end if build_prep_overlay quickchick; then installer_addon_section quickchick "QuickChick" "Coq plugin for randomized testing and counter example search" "" - log1 make + log1 make $MAKE_OPT log2 make install build_post fi @@ -1905,6 +1855,9 @@ function make_addon_quickchick { function make_addons { # Note: ':' is the empty command, which does not produce any output : > "/build/filelists/addon_dependencies.nsh" + : > "/build/filelists/addon_strings.nsh" + : > "/build/filelists/addon_descriptions.nsh" + : > "/build/filelists/addon_sections.nsh" for addon in $COQ_ADDONS; do "make_addon_$addon" diff --git a/dev/build/windows/patches_coq/VST.patch b/dev/build/windows/patches_coq/VST.patch new file mode 100644 index 0000000000..2c8c46373f --- /dev/null +++ b/dev/build/windows/patches_coq/VST.patch @@ -0,0 +1,15 @@ +diff --git a/Makefile b/Makefile +index 4a119042..fdfac13e 100755 +--- a/Makefile ++++ b/Makefile +@@ -76,8 +76,8 @@ endif + + COMPCERTDIRS=lib common $(ARCHDIRS) cfrontend flocq exportclight $(BACKEND) + +-COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT)/$(d) compcert.$(d)) +-EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT)/$(d) compcert.$(d)) ++COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT)/$(d) VST.compcert.$(d)) ++EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT)/$(d) VST.compcert.$(d)) + + # for SSReflect + ifdef MATHCOMP diff --git a/dev/build/windows/patches_coq/camlp4-4.02+6.patch b/dev/build/windows/patches_coq/camlp4-4.02+6.patch deleted file mode 100644 index 0cdb4a929b..0000000000 --- a/dev/build/windows/patches_coq/camlp4-4.02+6.patch +++ /dev/null @@ -1,11 +0,0 @@ ---- camlp4-4.02-6.orig/myocamlbuild.ml 2015-06-17 13:37:36.000000000 +0200 -+++ camlp4-4.02+6/myocamlbuild.ml 2016-10-13 13:57:35.512213600 +0200 -@@ -86,7 +86,7 @@ - let dep = "camlp4"/"boot"/exe in - let cmd = - let ( / ) = Filename.concat in -- "camlp4"/"boot"/exe -+ String.escaped (String.escaped ("camlp4"/"boot"/exe)) - in - (Some dep, cmd) - in diff --git a/dev/build/windows/patches_coq/coq-8.4pl2.patch b/dev/build/windows/patches_coq/coq-8.4pl2.patch deleted file mode 100644 index 45a66d0bfa..0000000000 --- a/dev/build/windows/patches_coq/coq-8.4pl2.patch +++ /dev/null @@ -1,11 +0,0 @@ ---- configure 2014-04-14 22:28:39.174177924 +0200 -+++ configure 2014-04-14 22:29:23.253025166 +0200 -@@ -335,7 +335,7 @@ - MAKEVERSION=`$MAKE -v | head -1 | cut -d" " -f3` - MAKEVERSIONMAJOR=`echo $MAKEVERSION | cut -d. -f1` - MAKEVERSIONMINOR=`echo $MAKEVERSION | cut -d. -f2` -- if [ "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 ]; then -+ if [ "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 ] || [ "$MAKEVERSIONMAJOR" -ge 4 ] ; then - echo "You have GNU Make $MAKEVERSION. Good!" - else - OK="no"
\ No newline at end of file diff --git a/dev/build/windows/patches_coq/coq-8.4pl6.patch b/dev/build/windows/patches_coq/coq-8.4pl6.patch deleted file mode 100644 index c3b7f8574e..0000000000 --- a/dev/build/windows/patches_coq/coq-8.4pl6.patch +++ /dev/null @@ -1,13 +0,0 @@ -coq-8.4pl6.orig ---- coq-8.4pl6.orig/configure 2015-04-09 15:59:35.000000000 +0200 -+++ coq-8.4pl6//configure 2016-11-09 13:29:42.235319800 +0100 -@@ -309,9 +309,6 @@ - # executable extension - - case "$ARCH,$CYGWIN" in -- win32,yes) -- EXE=".exe" -- DLLEXT=".so";; - win32,*) - EXE=".exe" - DLLEXT=".dll";; diff --git a/dev/build/windows/patches_coq/flexdll-0.34.patch b/dev/build/windows/patches_coq/flexdll-0.34.patch deleted file mode 100644 index 16389baca3..0000000000 --- a/dev/build/windows/patches_coq/flexdll-0.34.patch +++ /dev/null @@ -1,14 +0,0 @@ -reloc.ml ---- orig.flexdll-0.34/reloc.ml 2015-01-22 17:30:07.000000000 +0100 -+++ flexdll-0.34/reloc.ml 2016-10-12 11:59:16.885829700 +0200 -@@ -117,8 +117,8 @@ - - let new_cmdline () = - let rf = match !toolchain with -- | `MSVC | `MSVC64 | `LIGHTLD -> true -- | `MINGW | `MINGW64 | `GNAT | `CYGWIN | `CYGWIN64 -> false -+ | `MSVC | `MSVC64 | `LIGHTLD | `MINGW | `MINGW64 -> true -+ | `GNAT | `CYGWIN | `CYGWIN64 -> false - in - { - may_use_response_file = rf; diff --git a/dev/build/windows/patches_coq/flexdll-0.37.patch b/dev/build/windows/patches_coq/flexdll-0.37.patch new file mode 100644 index 0000000000..82806f9ea4 --- /dev/null +++ b/dev/build/windows/patches_coq/flexdll-0.37.patch @@ -0,0 +1,19 @@ +diff/patch file created on Tue, Feb 19, 2019 9:41:26 PM with: +difftar-folder.sh tarballs/flexdll-0.37.tar.gz flexdll-0.37 1 +TARFILE= tarballs/flexdll-0.37.tar.gz +FOLDER= flexdll-0.37 +TARSTRIP= 1 +TARPREFIX= flexdll-0.37/ +ORIGFOLDER= flexdll-0.37.orig +--- flexdll-0.37.orig/cmdline.ml 2017-10-25 10:40:46.000000000 +0200 ++++ flexdll-0.37/cmdline.ml 2019-02-19 21:41:18.157024900 +0100 +@@ -248,6 +248,9 @@ + String.sub s 0 2 :: String.sub s 2 (String.length s - 2) :: tr rest + | s :: rest when String.length s >= 5 && String.sub s 0 5 = "/link" -> + "-link" :: String.sub s 5 (String.length s - 5) :: tr rest ++ (* Convert gcc linker option prefix -Wl, to flexlink linker prefix -link *) ++ | s :: rest when String.length s >= 6 && String.sub s 0 5 = "-Wl,-" -> ++ "-link" :: String.sub s 4 (String.length s - 4) :: tr rest + | "-arg" :: x :: rest -> + tr (Array.to_list (Arg.read_arg x)) @ rest + | "-arg0" :: x :: rest -> diff --git a/dev/build/windows/patches_coq/glib-2.46.0.patch b/dev/build/windows/patches_coq/glib-2.46.0.patch deleted file mode 100644 index 9082460bf0..0000000000 --- a/dev/build/windows/patches_coq/glib-2.46.0.patch +++ /dev/null @@ -1,30 +0,0 @@ -diff -u -r glib-2.46.0/gio/glocalfile.c glib-2.46.0.patched/gio/glocalfile.c ---- glib-2.46.0/gio/glocalfile.c 2015-08-27 05:32:26.000000000 +0200 -+++ glib-2.46.0.patched/gio/glocalfile.c 2016-01-27 13:08:30.059736400 +0100 -@@ -2682,7 +2682,10 @@ - (!g_path_is_absolute (filename) || len > g_path_skip_root (filename) - filename)) - wfilename[len] = '\0'; - -- retval = _wstat32i64 (wfilename, &buf); -+ // MSoegtrop: _wstat32i64 is the wrong function for GLocalFileStat = struct _stati64 -+ // The correct function is _wstati64, see https://msdn.microsoft.com/en-us/library/14h5k7ff.aspx -+ // Also _wstat32i64 is a VC function, not a windows SDK function, see https://msdn.microsoft.com/en-us/library/aa273365(v=vs.60).aspx -+ retval = _wstati64 (wfilename, &buf); - save_errno = errno; - - g_free (wfilename); -diff -u -r glib-2.46.0/glib/gstdio.c glib-2.46.0.patched/glib/gstdio.c ---- glib-2.46.0/glib/gstdio.c 2015-02-26 13:57:09.000000000 +0100 -+++ glib-2.46.0.patched/glib/gstdio.c 2016-01-27 13:31:12.708987700 +0100 -@@ -493,7 +493,10 @@ - (!g_path_is_absolute (filename) || len > g_path_skip_root (filename) - filename)) - wfilename[len] = '\0'; - -- retval = _wstat (wfilename, buf); -+ // MSoegtrop: _wstat32i64 is the wrong function for GLocalFileStat = struct _stati64 -+ // The correct function is _wstati64, see https://msdn.microsoft.com/en-us/library/14h5k7ff.aspx -+ // Also _wstat32i64 is a VC function, not a windows SDK function, see https://msdn.microsoft.com/en-us/library/aa273365(v=vs.60).aspx -+ retval = _wstati64 (wfilename, buf); - save_errno = errno; - - g_free (wfilename); diff --git a/dev/build/windows/patches_coq/gtksourceview-2.11.2.patch b/dev/build/windows/patches_coq/gtksourceview-2.11.2.patch deleted file mode 100644 index 73a098d12a..0000000000 --- a/dev/build/windows/patches_coq/gtksourceview-2.11.2.patch +++ /dev/null @@ -1,213 +0,0 @@ -diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourceiter.c gtksourceview-2.11.2.patched/gtksourceview/gtksourceiter.c -*** gtksourceview-2.11.2.orig/gtksourceview/gtksourceiter.c 2010-05-30 12:24:14.000000000 +0200 ---- gtksourceview-2.11.2.patched/gtksourceview/gtksourceiter.c 2015-10-27 14:58:54.422888400 +0100 -*************** -*** 80,86 **** - /* If string contains prefix, check that prefix is not followed - * by a unicode mark symbol, e.g. that trailing 'a' in prefix - * is not part of two-char a-with-hat symbol in string. */ -! return type != G_UNICODE_COMBINING_MARK && - type != G_UNICODE_ENCLOSING_MARK && - type != G_UNICODE_NON_SPACING_MARK; - } ---- 80,86 ---- - /* If string contains prefix, check that prefix is not followed - * by a unicode mark symbol, e.g. that trailing 'a' in prefix - * is not part of two-char a-with-hat symbol in string. */ -! return type != G_UNICODE_SPACING_MARK && - type != G_UNICODE_ENCLOSING_MARK && - type != G_UNICODE_NON_SPACING_MARK; - } -diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcelanguagemanager.c gtksourceview-2.11.2.patched/gtksourceview/gtksourcelanguagemanager.c -*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcelanguagemanager.c 2010-05-30 12:24:14.000000000 +0200 ---- gtksourceview-2.11.2.patched/gtksourceview/gtksourcelanguagemanager.c 2015-10-27 14:55:30.294477600 +0100 -*************** -*** 274,280 **** - * containg a list of language files directories. - * The array is owned by @lm and must not be modified. - */ -! G_CONST_RETURN gchar* G_CONST_RETURN * - gtk_source_language_manager_get_search_path (GtkSourceLanguageManager *lm) - { - g_return_val_if_fail (GTK_IS_SOURCE_LANGUAGE_MANAGER (lm), NULL); ---- 274,280 ---- - * containg a list of language files directories. - * The array is owned by @lm and must not be modified. - */ -! const gchar* const * - gtk_source_language_manager_get_search_path (GtkSourceLanguageManager *lm) - { - g_return_val_if_fail (GTK_IS_SOURCE_LANGUAGE_MANAGER (lm), NULL); -*************** -*** 392,398 **** - * available languages or %NULL if no language is available. The array - * is owned by @lm and must not be modified. - */ -! G_CONST_RETURN gchar* G_CONST_RETURN * - gtk_source_language_manager_get_language_ids (GtkSourceLanguageManager *lm) - { - g_return_val_if_fail (GTK_IS_SOURCE_LANGUAGE_MANAGER (lm), NULL); ---- 392,398 ---- - * available languages or %NULL if no language is available. The array - * is owned by @lm and must not be modified. - */ -! const gchar* const * - gtk_source_language_manager_get_language_ids (GtkSourceLanguageManager *lm) - { - g_return_val_if_fail (GTK_IS_SOURCE_LANGUAGE_MANAGER (lm), NULL); -diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcelanguagemanager.h gtksourceview-2.11.2.patched/gtksourceview/gtksourcelanguagemanager.h -*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcelanguagemanager.h 2009-11-15 00:41:33.000000000 +0100 ---- gtksourceview-2.11.2.patched/gtksourceview/gtksourcelanguagemanager.h 2015-10-27 14:55:30.518500000 +0100 -*************** -*** 62,74 **** - - GtkSourceLanguageManager *gtk_source_language_manager_get_default (void); - -! G_CONST_RETURN gchar* G_CONST_RETURN * - gtk_source_language_manager_get_search_path (GtkSourceLanguageManager *lm); - - void gtk_source_language_manager_set_search_path (GtkSourceLanguageManager *lm, - gchar **dirs); - -! G_CONST_RETURN gchar* G_CONST_RETURN * - gtk_source_language_manager_get_language_ids (GtkSourceLanguageManager *lm); - - GtkSourceLanguage *gtk_source_language_manager_get_language (GtkSourceLanguageManager *lm, ---- 62,74 ---- - - GtkSourceLanguageManager *gtk_source_language_manager_get_default (void); - -! const gchar* const * - gtk_source_language_manager_get_search_path (GtkSourceLanguageManager *lm); - - void gtk_source_language_manager_set_search_path (GtkSourceLanguageManager *lm, - gchar **dirs); - -! const gchar* const * - gtk_source_language_manager_get_language_ids (GtkSourceLanguageManager *lm); - - GtkSourceLanguage *gtk_source_language_manager_get_language (GtkSourceLanguageManager *lm, -diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcestylescheme.c gtksourceview-2.11.2.patched/gtksourceview/gtksourcestylescheme.c -*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcestylescheme.c 2010-05-30 12:24:14.000000000 +0200 ---- gtksourceview-2.11.2.patched/gtksourceview/gtksourcestylescheme.c 2015-10-27 14:55:30.545502700 +0100 -*************** -*** 310,316 **** - * - * Since: 2.0 - */ -! G_CONST_RETURN gchar* G_CONST_RETURN * - gtk_source_style_scheme_get_authors (GtkSourceStyleScheme *scheme) - { - g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME (scheme), NULL); ---- 310,316 ---- - * - * Since: 2.0 - */ -! const gchar* const * - gtk_source_style_scheme_get_authors (GtkSourceStyleScheme *scheme) - { - g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME (scheme), NULL); -*************** -*** 318,324 **** - if (scheme->priv->authors == NULL) - return NULL; - -! return (G_CONST_RETURN gchar* G_CONST_RETURN *)scheme->priv->authors->pdata; - } - - /** ---- 318,324 ---- - if (scheme->priv->authors == NULL) - return NULL; - -! return (const gchar* const *)scheme->priv->authors->pdata; - } - - /** -diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcestylescheme.h gtksourceview-2.11.2.patched/gtksourceview/gtksourcestylescheme.h -*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcestylescheme.h 2010-03-29 15:02:56.000000000 +0200 ---- gtksourceview-2.11.2.patched/gtksourceview/gtksourcestylescheme.h 2015-10-27 14:55:30.565504700 +0100 -*************** -*** 61,67 **** - const gchar *gtk_source_style_scheme_get_name (GtkSourceStyleScheme *scheme); - const gchar *gtk_source_style_scheme_get_description(GtkSourceStyleScheme *scheme); - -! G_CONST_RETURN gchar* G_CONST_RETURN * - gtk_source_style_scheme_get_authors (GtkSourceStyleScheme *scheme); - - const gchar *gtk_source_style_scheme_get_filename (GtkSourceStyleScheme *scheme); ---- 61,67 ---- - const gchar *gtk_source_style_scheme_get_name (GtkSourceStyleScheme *scheme); - const gchar *gtk_source_style_scheme_get_description(GtkSourceStyleScheme *scheme); - -! const gchar* const * - gtk_source_style_scheme_get_authors (GtkSourceStyleScheme *scheme); - - const gchar *gtk_source_style_scheme_get_filename (GtkSourceStyleScheme *scheme); -diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcestyleschememanager.c gtksourceview-2.11.2.patched/gtksourceview/gtksourcestyleschememanager.c -*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcestyleschememanager.c 2010-05-30 12:24:14.000000000 +0200 ---- gtksourceview-2.11.2.patched/gtksourceview/gtksourcestyleschememanager.c 2015-10-27 14:55:30.583506500 +0100 -*************** -*** 515,521 **** - * of string containing the search path. - * The array is owned by the @manager and must not be modified. - */ -! G_CONST_RETURN gchar* G_CONST_RETURN * - gtk_source_style_scheme_manager_get_search_path (GtkSourceStyleSchemeManager *manager) - { - g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME_MANAGER (manager), NULL); ---- 515,521 ---- - * of string containing the search path. - * The array is owned by the @manager and must not be modified. - */ -! const gchar* const * - gtk_source_style_scheme_manager_get_search_path (GtkSourceStyleSchemeManager *manager) - { - g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME_MANAGER (manager), NULL); -*************** -*** 554,560 **** - * of string containing the ids of the available style schemes or %NULL if no - * style scheme is available. The array is owned by the @manager and must not be modified. - */ -! G_CONST_RETURN gchar* G_CONST_RETURN * - gtk_source_style_scheme_manager_get_scheme_ids (GtkSourceStyleSchemeManager *manager) - { - g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME_MANAGER (manager), NULL); ---- 554,560 ---- - * of string containing the ids of the available style schemes or %NULL if no - * style scheme is available. The array is owned by the @manager and must not be modified. - */ -! const gchar* const * - gtk_source_style_scheme_manager_get_scheme_ids (GtkSourceStyleSchemeManager *manager) - { - g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME_MANAGER (manager), NULL); -diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcestyleschememanager.h gtksourceview-2.11.2.patched/gtksourceview/gtksourcestyleschememanager.h -*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcestyleschememanager.h 2009-11-15 00:41:33.000000000 +0100 ---- gtksourceview-2.11.2.patched/gtksourceview/gtksourcestyleschememanager.h 2015-10-27 14:56:24.498897500 +0100 -*************** -*** 73,84 **** - void gtk_source_style_scheme_manager_prepend_search_path (GtkSourceStyleSchemeManager *manager, - const gchar *path); - -! G_CONST_RETURN gchar* G_CONST_RETURN * - gtk_source_style_scheme_manager_get_search_path (GtkSourceStyleSchemeManager *manager); - - void gtk_source_style_scheme_manager_force_rescan (GtkSourceStyleSchemeManager *manager); - -! G_CONST_RETURN gchar* G_CONST_RETURN * - gtk_source_style_scheme_manager_get_scheme_ids (GtkSourceStyleSchemeManager *manager); - - GtkSourceStyleScheme *gtk_source_style_scheme_manager_get_scheme (GtkSourceStyleSchemeManager *manager, ---- 73,84 ---- - void gtk_source_style_scheme_manager_prepend_search_path (GtkSourceStyleSchemeManager *manager, - const gchar *path); - -! const gchar* const * - gtk_source_style_scheme_manager_get_search_path (GtkSourceStyleSchemeManager *manager); - - void gtk_source_style_scheme_manager_force_rescan (GtkSourceStyleSchemeManager *manager); - -! const gchar* const * - gtk_source_style_scheme_manager_get_scheme_ids (GtkSourceStyleSchemeManager *manager); - - GtkSourceStyleScheme *gtk_source_style_scheme_manager_get_scheme (GtkSourceStyleSchemeManager *manager, diff --git a/dev/build/windows/patches_coq/lablgtk-2.18.6.patch b/dev/build/windows/patches_coq/lablgtk-2.18.6.patch deleted file mode 100644 index 23c303135d..0000000000 --- a/dev/build/windows/patches_coq/lablgtk-2.18.6.patch +++ /dev/null @@ -1,101 +0,0 @@ -diff/patch file created on Wed, Apr 25, 2018 11:08:05 AM with: -difftar-folder.sh ../coq-msoegtrop/dev/build/windows/source_cache/lablgtk-2.18.3.tar.gz lablgtk-2.18.3 1 -TARFILE= ../coq-msoegtrop/dev/build/windows/source_cache/lablgtk-2.18.3.tar.gz -FOLDER= lablgtk-2.18.3 -TARSTRIP= 1 -TARPREFIX= lablgtk-2.18.3/ -ORIGFOLDER= lablgtk-2.18.3.orig ---- lablgtk-2.18.3.orig/configure 2014-10-29 08:51:05.000000000 +0100 -+++ lablgtk-2.18.3/configure 2018-04-25 10:58:54.454501600 +0200 -@@ -2667,7 +2667,7 @@ - fi - - --if test "`$OCAMLFIND printconf stdlib`" != "`$CAMLC -where`"; then -+if test "`$OCAMLFIND printconf stdlib | tr '\\' '/'`" != "`$CAMLC -where | tr '\\' '/'`"; then - { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: Ignoring ocamlfind" >&5 - $as_echo "$as_me: WARNING: Ignoring ocamlfind" >&2;} - OCAMLFIND=no ---- lablgtk-2.18.3.orig/src/glib.mli 2014-10-29 08:51:06.000000000 +0100 -+++ lablgtk-2.18.3/src/glib.mli 2018-04-25 10:58:54.493555500 +0200 -@@ -75,6 +75,7 @@ - type condition = [ `ERR | `HUP | `IN | `NVAL | `OUT | `PRI] - type id - val channel_of_descr : Unix.file_descr -> channel -+ val channel_of_descr_socket : Unix.file_descr -> channel - val add_watch : - cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id - val remove : id -> unit ---- lablgtk-2.18.3.orig/src/glib.ml 2014-10-29 08:51:06.000000000 +0100 -+++ lablgtk-2.18.3/src/glib.ml 2018-04-25 10:58:54.479543500 +0200 -@@ -72,6 +72,8 @@ - type id - external channel_of_descr : Unix.file_descr -> channel - = "ml_g_io_channel_unix_new" -+ external channel_of_descr_socket : Unix.file_descr -> channel -+ = "ml_g_io_channel_unix_new_socket" - external remove : id -> unit = "ml_g_source_remove" - external add_watch : - cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id ---- lablgtk-2.18.3.orig/src/Makefile 2014-10-29 08:51:06.000000000 +0100 -+++ lablgtk-2.18.3/src/Makefile 2018-04-25 10:58:54.506522500 +0200 -@@ -461,9 +461,9 @@ - do rm -f "$(BINDIR)"/$$f; done - - lablgtk.cma liblablgtk2$(XA): $(COBJS) $(MLOBJS) -- $(LIBRARIAN) -o lablgtk -oc lablgtk2 $^ $(GTKLIBS) -+ $(LIBRARIAN) -ldopt "-link -Wl,-s" -o lablgtk -oc lablgtk2 $^ $(GTKLIBS) - lablgtk.cmxa: $(COBJS) $(MLOBJS:.cmo=.cmx) -- $(LIBRARIAN) -o lablgtk -oc lablgtk2 $^ $(GTKLIBS) -+ $(LIBRARIAN) -ldopt "-link -Wl,-s" -o lablgtk -oc lablgtk2 $^ $(GTKLIBS) - lablgtk.cmxs: DYNLINKLIBS=$(GTK_LIBS) - - lablgtkgl.cma liblablgtkgl2$(XA): $(GLCOBJS) $(GLMLOBJS) ---- lablgtk-2.18.3.orig/src/ml_glib.c 2014-10-29 08:51:06.000000000 +0100 -+++ lablgtk-2.18.3/src/ml_glib.c 2018-04-25 10:58:54.539535600 +0200 -@@ -25,6 +25,8 @@ - #include <string.h> - #include <locale.h> - #ifdef _WIN32 -+/* to kill a #warning: include winsock2.h before windows.h */ -+#include <winsock2.h> - #include "win32.h" - #include <wtypes.h> - #include <io.h> -@@ -38,6 +40,11 @@ - #include <caml/callback.h> - #include <caml/threads.h> - -+#ifdef _WIN32 -+/* for Socket_val */ -+#include <caml/unixsupport.h> -+#endif -+ - #include "wrappers.h" - #include "ml_glib.h" - #include "glib_tags.h" -@@ -325,14 +332,23 @@ - - #ifndef _WIN32 - ML_1 (g_io_channel_unix_new, Int_val, Val_GIOChannel_noref) -+CAMLprim value ml_g_io_channel_unix_new_socket (value arg1) { -+ return Val_GIOChannel_noref (g_io_channel_unix_new (Int_val (arg1))); -+} - - #else - CAMLprim value ml_g_io_channel_unix_new(value wh) - { - return Val_GIOChannel_noref -- (g_io_channel_unix_new -+ (g_io_channel_win32_new_fd - (_open_osfhandle((long)*(HANDLE*)Data_custom_val(wh), O_BINARY))); - } -+ -+CAMLprim value ml_g_io_channel_unix_new_socket(value wh) -+{ -+ return Val_GIOChannel_noref -+ (g_io_channel_win32_new_socket(Socket_val(wh))); -+} - #endif - - static gboolean ml_g_io_channel_watch(GIOChannel *s, GIOCondition c, diff --git a/dev/build/windows/patches_coq/lablgtk-2.18.3.patch b/dev/build/windows/patches_coq/lablgtk-3.0.beta5.patch index 23c303135d..1c6a038da9 100644 --- a/dev/build/windows/patches_coq/lablgtk-2.18.3.patch +++ b/dev/build/windows/patches_coq/lablgtk-3.0.beta5.patch @@ -1,33 +1,12 @@ -diff/patch file created on Wed, Apr 25, 2018 11:08:05 AM with: -difftar-folder.sh ../coq-msoegtrop/dev/build/windows/source_cache/lablgtk-2.18.3.tar.gz lablgtk-2.18.3 1 -TARFILE= ../coq-msoegtrop/dev/build/windows/source_cache/lablgtk-2.18.3.tar.gz -FOLDER= lablgtk-2.18.3 +diff/patch file created on Wed, Feb 20, 2019 11:29:48 AM with: +difftar-folder.sh tarballs/lablgtk-3.0.beta4.tar.gz lablgtk-3.0.beta4 1 +TARFILE= tarballs/lablgtk-3.0.beta4.tar.gz +FOLDER= lablgtk-3.0.beta4 TARSTRIP= 1 -TARPREFIX= lablgtk-2.18.3/ -ORIGFOLDER= lablgtk-2.18.3.orig ---- lablgtk-2.18.3.orig/configure 2014-10-29 08:51:05.000000000 +0100 -+++ lablgtk-2.18.3/configure 2018-04-25 10:58:54.454501600 +0200 -@@ -2667,7 +2667,7 @@ - fi - - --if test "`$OCAMLFIND printconf stdlib`" != "`$CAMLC -where`"; then -+if test "`$OCAMLFIND printconf stdlib | tr '\\' '/'`" != "`$CAMLC -where | tr '\\' '/'`"; then - { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: Ignoring ocamlfind" >&5 - $as_echo "$as_me: WARNING: Ignoring ocamlfind" >&2;} - OCAMLFIND=no ---- lablgtk-2.18.3.orig/src/glib.mli 2014-10-29 08:51:06.000000000 +0100 -+++ lablgtk-2.18.3/src/glib.mli 2018-04-25 10:58:54.493555500 +0200 -@@ -75,6 +75,7 @@ - type condition = [ `ERR | `HUP | `IN | `NVAL | `OUT | `PRI] - type id - val channel_of_descr : Unix.file_descr -> channel -+ val channel_of_descr_socket : Unix.file_descr -> channel - val add_watch : - cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id - val remove : id -> unit ---- lablgtk-2.18.3.orig/src/glib.ml 2014-10-29 08:51:06.000000000 +0100 -+++ lablgtk-2.18.3/src/glib.ml 2018-04-25 10:58:54.479543500 +0200 +TARPREFIX= lablgtk-3.0.beta4/ +ORIGFOLDER= lablgtk-3.0.beta4.orig +--- lablgtk-3.0.beta4.orig/src/glib.ml 2019-02-11 07:08:17.000000000 +0100 ++++ lablgtk-3.0.beta4/src/glib.ml 2019-02-20 11:28:28.439137100 +0100 @@ -72,6 +72,8 @@ type id external channel_of_descr : Unix.file_descr -> channel @@ -37,22 +16,18 @@ ORIGFOLDER= lablgtk-2.18.3.orig external remove : id -> unit = "ml_g_source_remove" external add_watch : cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id ---- lablgtk-2.18.3.orig/src/Makefile 2014-10-29 08:51:06.000000000 +0100 -+++ lablgtk-2.18.3/src/Makefile 2018-04-25 10:58:54.506522500 +0200 -@@ -461,9 +461,9 @@ - do rm -f "$(BINDIR)"/$$f; done - - lablgtk.cma liblablgtk2$(XA): $(COBJS) $(MLOBJS) -- $(LIBRARIAN) -o lablgtk -oc lablgtk2 $^ $(GTKLIBS) -+ $(LIBRARIAN) -ldopt "-link -Wl,-s" -o lablgtk -oc lablgtk2 $^ $(GTKLIBS) - lablgtk.cmxa: $(COBJS) $(MLOBJS:.cmo=.cmx) -- $(LIBRARIAN) -o lablgtk -oc lablgtk2 $^ $(GTKLIBS) -+ $(LIBRARIAN) -ldopt "-link -Wl,-s" -o lablgtk -oc lablgtk2 $^ $(GTKLIBS) - lablgtk.cmxs: DYNLINKLIBS=$(GTK_LIBS) - - lablgtkgl.cma liblablgtkgl2$(XA): $(GLCOBJS) $(GLMLOBJS) ---- lablgtk-2.18.3.orig/src/ml_glib.c 2014-10-29 08:51:06.000000000 +0100 -+++ lablgtk-2.18.3/src/ml_glib.c 2018-04-25 10:58:54.539535600 +0200 +--- lablgtk-3.0.beta4.orig/src/glib.mli 2019-02-11 07:08:17.000000000 +0100 ++++ lablgtk-3.0.beta4/src/glib.mli 2019-02-20 11:28:28.423592200 +0100 +@@ -75,6 +75,7 @@ + type condition = [ `ERR | `HUP | `IN | `NVAL | `OUT | `PRI] + type id + val channel_of_descr : Unix.file_descr -> channel ++ val channel_of_descr_socket : Unix.file_descr -> channel + val add_watch : + cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id + val remove : id -> unit +--- lablgtk-3.0.beta4.orig/src/ml_glib.c 2019-02-11 07:08:17.000000000 +0100 ++++ lablgtk-3.0.beta4/src/ml_glib.c 2019-02-20 11:28:28.455395900 +0100 @@ -25,6 +25,8 @@ #include <string.h> #include <locale.h> @@ -74,7 +49,7 @@ ORIGFOLDER= lablgtk-2.18.3.orig #include "wrappers.h" #include "ml_glib.h" #include "glib_tags.h" -@@ -325,14 +332,23 @@ +@@ -326,14 +333,23 @@ #ifndef _WIN32 ML_1 (g_io_channel_unix_new, Int_val, Val_GIOChannel_noref) diff --git a/dev/build/windows/patches_coq/pkg-config.c b/dev/build/windows/patches_coq/pkg-config.c new file mode 100755 index 0000000000..e4fdcd4d7d --- /dev/null +++ b/dev/build/windows/patches_coq/pkg-config.c @@ -0,0 +1,29 @@ +// MinGW personality wrapper for pkgconf +// This is an excutable replacement for the shell scripts /bin/ARCH-pkg-config +// Compile with e.g. +// gcc pkg-config.c -DARCH=x86_64-w64-mingw32 -o pkg-config.exe +// gcc pkg-config.c -DARCH=i686-w64-mingw32 -o pkg-config.exe +// ATTENTION: Do not compile with MinGW-gcc, compile with cygwin gcc! +// +// To test it execute e.g. +// $ ./pkg-config --path zlib +// /usr/x86_64-w64-mingw32/sys-root/mingw/lib/pkgconfig/zlib.pc + +#include <unistd.h> + +#define STRINGIFY1(arg) #arg +#define STRINGIFY(arg) STRINGIFY1(arg) + +int main(int argc, char *argv[]) +{ + // +1 for extra argument, +1 for trailing NULL + char * argvnew[argc+2]; + int id=0, is=0; + + argvnew[id++] = argv[is++]; + argvnew[id++] = "--personality="STRINGIFY(ARCH); + while( is<argc ) argvnew[id++] = argv[is++]; + argvnew[id++] = 0; + + return execv("/usr/bin/pkgconf", argvnew); +} diff --git a/dev/build/windows/patches_coq/quickchick.patch b/dev/build/windows/patches_coq/quickchick.patch index 1afa6e7f95..1afa6e7f95 100755..100644 --- a/dev/build/windows/patches_coq/quickchick.patch +++ b/dev/build/windows/patches_coq/quickchick.patch 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 index d210a04153..d210a04153 100755..100644 --- 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 diff --git a/dev/build/windows/patches_coq/sed-4.2.2.patch b/dev/build/windows/patches_coq/sed-4.2.2.patch index c7ccd53c7f..c7ccd53c7f 100755..100644 --- a/dev/build/windows/patches_coq/sed-4.2.2.patch +++ b/dev/build/windows/patches_coq/sed-4.2.2.patch |