aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--dev/build/windows/CAVEATS.txt22
-rw-r--r--dev/build/windows/MakeCoq_84pl6_abs_ocaml.bat10
-rw-r--r--dev/build/windows/MakeCoq_85pl2_abs_ocaml.bat10
-rw-r--r--dev/build/windows/MakeCoq_85pl3_abs_ocaml.bat10
-rw-r--r--dev/build/windows/MakeCoq_85pl3_installer.bat8
-rw-r--r--dev/build/windows/MakeCoq_85pl3_installer_32.bat8
-rw-r--r--dev/build/windows/MakeCoq_86git_abs_ocaml.bat10
-rw-r--r--dev/build/windows/MakeCoq_86git_abs_ocaml_gtksrc.bat11
-rw-r--r--dev/build/windows/MakeCoq_86git_installer.bat8
-rw-r--r--dev/build/windows/MakeCoq_86git_installer2.bat8
-rw-r--r--dev/build/windows/MakeCoq_86git_installer_32.bat8
-rw-r--r--dev/build/windows/MakeCoq_MinGW.bat445
-rw-r--r--dev/build/windows/MakeCoq_SetRootPath.bat16
-rw-r--r--dev/build/windows/MakeCoq_regtest_noproxy.bat18
-rw-r--r--dev/build/windows/MakeCoq_regtests.bat16
-rw-r--r--dev/build/windows/ReadMe.txt460
-rw-r--r--dev/build/windows/configure_profile.sh32
-rw-r--r--dev/build/windows/difftar-folder.sh86
-rw-r--r--dev/build/windows/makecoq_mingw.sh1271
-rw-r--r--dev/build/windows/patches_coq/ReplaceInFile.nsh67
-rw-r--r--dev/build/windows/patches_coq/StrRep.nsh60
-rw-r--r--dev/build/windows/patches_coq/camlp4-4.02+6.patch11
-rw-r--r--dev/build/windows/patches_coq/coq-8.4pl2.patch11
-rw-r--r--dev/build/windows/patches_coq/coq-8.4pl6.patch13
-rw-r--r--dev/build/windows/patches_coq/coq_new.nsi223
-rw-r--r--dev/build/windows/patches_coq/flexdll-0.34.patch14
-rw-r--r--dev/build/windows/patches_coq/glib-2.46.0.patch30
-rw-r--r--dev/build/windows/patches_coq/gtksourceview-2.11.2.patch213
-rw-r--r--dev/build/windows/patches_coq/isl-0.14.patch11
-rw-r--r--dev/build/windows/patches_coq/lablgtk-2.18.3.patch87
-rw-r--r--dev/build/windows/patches_coq/ln.c137
31 files changed, 3334 insertions, 0 deletions
diff --git a/dev/build/windows/CAVEATS.txt b/dev/build/windows/CAVEATS.txt
new file mode 100644
index 000000000..cb1ae3aaa
--- /dev/null
+++ b/dev/build/windows/CAVEATS.txt
@@ -0,0 +1,22 @@
+===== Environemt SIZE =====
+
+find and xargs can fail if the environment is to large. I think the limit is 8k.
+
+xargs --show-limits
+
+shows the actual environment size
+
+The configure_profile.sh script sets ORIGINAL_PATH (set by cygwin) to "" to
+avoid issues
+
+===== OCAMLLIB =====
+
+If the environment variable OCAMLLIB is defined, it takes precedence over the
+internal paths of ocaml tools. This usually messes up things considerably. A
+typical failure is
+
+Error: Error on dynamically loaded library: .\dlllablgtk2.dll: %1 is not a valid Win32 application.
+
+The configure_profile.sh script clears OCAMLLIB, but if you use the ocaml
+compiler from outside the provided cygwin shell, OCAMLLIB might be defined.
+
diff --git a/dev/build/windows/MakeCoq_84pl6_abs_ocaml.bat b/dev/build/windows/MakeCoq_84pl6_abs_ocaml.bat
new file mode 100644
index 000000000..bdcb01db9
--- /dev/null
+++ b/dev/build/windows/MakeCoq_84pl6_abs_ocaml.bat
@@ -0,0 +1,10 @@
+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
diff --git a/dev/build/windows/MakeCoq_85pl2_abs_ocaml.bat b/dev/build/windows/MakeCoq_85pl2_abs_ocaml.bat
new file mode 100644
index 000000000..2e4a692e9
--- /dev/null
+++ b/dev/build/windows/MakeCoq_85pl2_abs_ocaml.bat
@@ -0,0 +1,10 @@
+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
diff --git a/dev/build/windows/MakeCoq_85pl3_abs_ocaml.bat b/dev/build/windows/MakeCoq_85pl3_abs_ocaml.bat
new file mode 100644
index 000000000..6e4e440a2
--- /dev/null
+++ b/dev/build/windows/MakeCoq_85pl3_abs_ocaml.bat
@@ -0,0 +1,10 @@
+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
diff --git a/dev/build/windows/MakeCoq_85pl3_installer.bat b/dev/build/windows/MakeCoq_85pl3_installer.bat
new file mode 100644
index 000000000..c305e2f52
--- /dev/null
+++ b/dev/build/windows/MakeCoq_85pl3_installer.bat
@@ -0,0 +1,8 @@
+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
diff --git a/dev/build/windows/MakeCoq_85pl3_installer_32.bat b/dev/build/windows/MakeCoq_85pl3_installer_32.bat
new file mode 100644
index 000000000..d87ff5919
--- /dev/null
+++ b/dev/build/windows/MakeCoq_85pl3_installer_32.bat
@@ -0,0 +1,8 @@
+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
diff --git a/dev/build/windows/MakeCoq_86git_abs_ocaml.bat b/dev/build/windows/MakeCoq_86git_abs_ocaml.bat
new file mode 100644
index 000000000..f1d855a02
--- /dev/null
+++ b/dev/build/windows/MakeCoq_86git_abs_ocaml.bat
@@ -0,0 +1,10 @@
+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
diff --git a/dev/build/windows/MakeCoq_86git_abs_ocaml_gtksrc.bat b/dev/build/windows/MakeCoq_86git_abs_ocaml_gtksrc.bat
new file mode 100644
index 000000000..70ab42bc3
--- /dev/null
+++ b/dev/build/windows/MakeCoq_86git_abs_ocaml_gtksrc.bat
@@ -0,0 +1,11 @@
+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
diff --git a/dev/build/windows/MakeCoq_86git_installer.bat b/dev/build/windows/MakeCoq_86git_installer.bat
new file mode 100644
index 000000000..40506318e
--- /dev/null
+++ b/dev/build/windows/MakeCoq_86git_installer.bat
@@ -0,0 +1,8 @@
+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
diff --git a/dev/build/windows/MakeCoq_86git_installer2.bat b/dev/build/windows/MakeCoq_86git_installer2.bat
new file mode 100644
index 000000000..d184f0e30
--- /dev/null
+++ b/dev/build/windows/MakeCoq_86git_installer2.bat
@@ -0,0 +1,8 @@
+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
new file mode 100644
index 000000000..b9127c945
--- /dev/null
+++ b/dev/build/windows/MakeCoq_86git_installer_32.bat
@@ -0,0 +1,8 @@
+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
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
new file mode 100644
index 000000000..1e08cc5a3
--- /dev/null
+++ b/dev/build/windows/MakeCoq_MinGW.bat
@@ -0,0 +1,445 @@
+@ECHO OFF
+
+REM ========== COPYRIGHT/COPYLEFT ==========
+
+REM (C) 2016 Intel Deutschland GmbH
+REM Author: Michael Soegtrop
+
+REM Released to the public by Intel under the
+REM GNU Lesser General Public License Version 2.1 or later
+REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
+
+REM ========== NOTES ==========
+
+REM For Cygwin setup command line options
+REM see https://cygwin.com/faq/faq.html#faq.setup.cli
+
+REM ========== DEFAULT VALUES FOR PARAMETERS ==========
+
+REM For a description of all parameters, see ReadMe.txt
+
+SET BATCHFILE=%0
+SET BATCHDIR=%~dp0
+
+REM see -arch in ReadMe.txt, but values are x86_64 or i686 (not 64 or 32)
+SET ARCH=x86_64
+
+REM see -mode in ReadMe.txt
+SET INSTALLMODE=absolute
+
+REM see -installer in ReadMe.txt
+SET MAKEINSTALLER=N
+
+REM see -ocaml in ReadMe.txt
+SET INSTALLOCAML=N
+
+REM see -make in ReadMe.txt
+SET INSTALLMAKE=Y
+
+REM see -destcyg in ReadMe.txt
+SET DESTCYG=C:\bin\cygwin_coq
+
+REM see -destcoq in ReadMe.txt
+SET DESTCOQ=C:\bin\coq
+
+REM see -setup in ReadMe.txt
+SET SETUP=setup-x86_64.exe
+
+REM see -proxy in ReadMe.txt
+IF DEFINED HTTP_PROXY (
+ SET PROXY="%HTTP_PROXY:http://=%"
+) else (
+ SET PROXY=""
+)
+
+REM see -cygrepo in ReadMe.txt
+SET CYGWIN_REPOSITORY=http://ftp.inf.tu-dresden.de/software/windows/cygwin32
+
+REM see -cygcache in ReadMe.txt
+SET CYGWIN_LOCAL_CACHE_WFMT=%BATCHDIR%cygwin_cache
+
+REM see -cyglocal in ReadMe.txt
+SET CYGWIN_FROM_CACHE=N
+
+REM see -cygquiet in ReadMe.txt
+SET CYGWIN_QUIET=Y
+
+REM see -srccache in ReadMe.txt
+SET SOURCE_LOCAL_CACHE_WFMT=%BATCHDIR%source_cache
+
+REM see -coqver in ReadMe.txt
+SET COQ_VERSION=8.5pl3
+
+REM see -gtksrc in ReadMe.txt
+SET GTK_FROM_SOURCES=N
+
+REM see -threads in ReadMe.txt
+SET MAKE_THREADS=8
+
+REM ========== PARSE COMMAND LINE PARAMETERS ==========
+
+SHIFT
+
+:Parse
+
+IF "%0" == "-arch" (
+ IF "%1" == "32" (
+ SET ARCH=i686
+ SET SETUP=setup-x86.exe
+ ) ELSE (
+ IF "%1" == "64" (
+ SET ARCH=x86_64
+ SET SETUP=setup-x86_64.exe
+ ) ELSE (
+ ECHO "Invalid -arch, valid are 32 and 64"
+ GOTO :EOF
+ )
+ )
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%0" == "-mode" (
+ IF "%1" == "mingwincygwin" (
+ SET INSTALLMODE=%1
+ ) ELSE (
+ IF "%1" == "absolute" (
+ SET INSTALLMODE=%1
+ ) ELSE (
+ IF "%1" == "relocatable" (
+ SET INSTALLMODE=%1
+ ) ELSE (
+ ECHO "Invalid -mode, valid are mingwincygwin, absolute and relocatable"
+ GOTO :EOF
+ )
+ )
+ )
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%0" == "-installer" (
+ SET MAKEINSTALLER=%1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%0" == "-ocaml" (
+ SET INSTALLOCAML=%1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%0" == "-make" (
+ SET INSTALLMAKE=%1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%0" == "-destcyg" (
+ SET DESTCYG=%1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%0" == "-destcoq" (
+ SET DESTCOQ=%1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%0" == "-setup" (
+ SET SETUP=%1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%0" == "-proxy" (
+ SET PROXY="%1"
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%0" == "-cygrepo" (
+ SET CYGWIN_REPOSITORY="%1"
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%0" == "-cygcache" (
+ SET CYGWIN_LOCAL_CACHE_WFMT="%1"
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%0" == "-cyglocal" (
+ SET CYGWIN_FROM_CACHE=%1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%0" == "-cygquiet" (
+ SET CYGWIN_QUIET=%1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%0" == "-srccache" (
+ SET SOURCE_LOCAL_CACHE_WFMT="%1"
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%0" == "-coqver" (
+ SET COQ_VERSION=%1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%0" == "-gtksrc" (
+ SET GTK_FROM_SOURCES=%1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%0" == "-threads" (
+ SET MAKE_THREADS=%1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF NOT "%0" == "" (
+ ECHO Install cygwin and download, compile and install OCaml and Coq for MinGW
+ ECHO !!! Illegal parameter %0
+ ECHO Usage:
+ ECHO MakeCoq_MinGW
+ CALL :PrintPars
+ goto :EOF
+)
+
+IF NOT EXIST %SETUP% (
+ ECHO The cygwin setup program %SETUP% doesn't exist. You must download it from https://cygwin.com/install.html.
+ GOTO :EOF
+)
+
+REM ========== ADJUST PARAMETERS ==========
+
+IF "%INSTALLMODE%" == "mingwincygwin" (
+ SET DESTCOQ=%DESTCYG%\usr\%ARCH%-w64-mingw32\sys-root\mingw
+)
+
+IF "%MAKEINSTALLER%" == "Y" (
+ SET INSTALLMODE=relocatable
+ SET INSTALLOCAML=Y
+ SET INSTALLMAKE=Y
+)
+
+REM ========== CONFIRM PARAMETERS ==========
+
+CALL :PrintPars
+REM Note: DOS batch replaces variables on parsing, so one can't use a variable just set in an () block
+IF "%COQREGTESTING%"=="Y" (GOTO :DontAsk)
+ SET /p ANSWER=Is this correct? y/n
+ IF NOT "%ANSWER%"=="y" (GOTO :EOF)
+:DontAsk
+
+REM ========== DERIVED VARIABLES ==========
+
+SET CYGWIN_INSTALLDIR_WFMT=%DESTCYG%
+SET RESULT_INSTALLDIR_WFMT=%DESTCOQ%
+SET TARGET_ARCH=%ARCH%-w64-mingw32
+SET BASH=%CYGWIN_INSTALLDIR_WFMT%\bin\bash
+
+REM Convert pathes to various formats
+REM WFMT = windows format (C:\..) Used in this batch file.
+REM CFMT = cygwin format (\cygdrive\c\..) Used for Cygwin PATH varible, which is : separated, so C: doesn't work.
+REM MFMT = MinGW format (C:/...) Used for the build, because \\ requires escaping. Mingw can handle \ and /.
+
+SET CYGWIN_INSTALLDIR_MFMT=%CYGWIN_INSTALLDIR_WFMT:\=/%
+SET RESULT_INSTALLDIR_MFMT=%RESULT_INSTALLDIR_WFMT:\=/%
+SET SOURCE_LOCAL_CACHE_MFMT=%SOURCE_LOCAL_CACHE_WFMT:\=/%
+
+SET CYGWIN_INSTALLDIR_CFMT=%CYGWIN_INSTALLDIR_MFMT:C:/=/cygdrive/c/%
+SET RESULT_INSTALLDIR_CFMT=%RESULT_INSTALLDIR_MFMT:C:/=/cygdrive/c/%
+SET SOURCE_LOCAL_CACHE_CFMT=%SOURCE_LOCAL_CACHE_MFMT:C:/=/cygdrive/c/%
+
+SET CYGWIN_INSTALLDIR_CFMT=%CYGWIN_INSTALLDIR_CFMT:D:/=/cygdrive/d/%
+SET RESULT_INSTALLDIR_CFMT=%RESULT_INSTALLDIR_CFMT:D:/=/cygdrive/d/%
+SET SOURCE_LOCAL_CACHE_CFMT=%SOURCE_LOCAL_CACHE_CFMT:D:/=/cygdrive/d/%
+
+SET CYGWIN_INSTALLDIR_CFMT=%CYGWIN_INSTALLDIR_CFMT:E:/=/cygdrive/e/%
+SET RESULT_INSTALLDIR_CFMT=%RESULT_INSTALLDIR_CFMT:E:/=/cygdrive/e/%
+SET SOURCE_LOCAL_CACHE_CFMT=%SOURCE_LOCAL_CACHE_CFMT:E:/=/cygdrive/e/%
+
+ECHO CYGWIN INSTALL DIR (WIN) = %CYGWIN_INSTALLDIR_WFMT%
+ECHO CYGWIN INSTALL DIR (MINGW) = %CYGWIN_INSTALLDIR_MFMT%
+ECHO CYGWIN INSTALL DIR (CYGWIN) = %CYGWIN_INSTALLDIR_CFMT%
+ECHO RESULT INSTALL DIR (WIN) = %RESULT_INSTALLDIR_WFMT%
+ECHO RESULT INSTALL DIR (MINGW) = %RESULT_INSTALLDIR_MFMT%
+ECHO RESULT INSTALL DIR (CYGWIN) = %RESULT_INSTALLDIR_CFMT%
+
+REM WARNING: Add a space after the = in case you want set this to empty, otherwise the variable will be unset
+SET MAKE_OPT=-j %MAKE_THREADS%
+
+REM ========== DERIVED CYGWIN SETUP OPTIONS ==========
+
+REM WARNING: Add a space after the = otherwise the variable will be unset
+SET CYGWIN_OPT=
+
+IF "%CYGWIN_FROM_CACHE%" == "Y" (
+ SET CYGWIN_OPT= %CYGWIN_OPT% -L
+)
+
+IF "%CYGWIN_QUIET%" == "Y" (
+ SET CYGWIN_OPT= %CYGWIN_OPT% -q --no-admin
+)
+
+IF "%GTK_FROM_SOURCES%"=="N" (
+ SET CYGWIN_OPT= %CYGWIN_OPT% -P mingw64-%ARCH%-gtk2.0,mingw64-%ARCH%-gtksourceview2.0
+)
+
+ECHO ========== INSTALL CYGWIN ==========
+
+REM Cygwin setup sets proper ACLs (permissions) for folders it CREATES.
+REM Otherwise chmod won't work and e.g. the ocaml build will fail.
+REM Cygwin setup does not touch the ACLs of existing folders.
+REM => 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
+
+REM Run Cygwin Setup
+
+SET RUNSETUP=Y
+IF EXIST "%CYGWIN_INSTALLDIR_WFMT%\etc\setup\installed.db" (
+ SET RUNSETUP=N
+)
+IF NOT "%CYGWIN_QUIET%" == "Y" (
+ SET RUNSETUP=Y
+)
+
+IF "%RUNSETUP%"=="Y" (
+ %SETUP% ^
+ --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 ^
+ -P gcc-core,gcc-g++ ^
+ -P gdb,liblzma5 ^
+ -P patch,automake1.14,automake1.15 ^
+ -P mingw64-%ARCH%-binutils,mingw64-%ARCH%-gcc-core,mingw64-%ARCH%-gcc-g++,mingw64-%ARCH%-pkg-config,mingw64-%ARCH%-windows_default_manifest ^
+ -P mingw64-%ARCH%-headers,mingw64-%ARCH%-runtime,mingw64-%ARCH%-pthreads,mingw64-%ARCH%-zlib ^
+ -P libiconv-devel,libunistring-devel,libncurses-devel ^
+ -P gettext-devel,libgettextpo-devel ^
+ -P libglib2.0-devel,libgdk_pixbuf2.0-devel ^
+ -P libfontconfig1 ^
+ -P gtk-update-icon-cache ^
+ -P libtool,automake ^
+ -P intltool ^
+ > "%LOGFILE%" ^
+ || GOTO :Error
+
+ MKDIR %CYGWIN_INSTALLDIR_WFMT%\build
+ MKDIR %CYGWIN_INSTALLDIR_WFMT%\build\buildlogs
+ MOVE "%LOGFILE%" %CYGWIN_INSTALLDIR_WFMT%\build\buildlogs\cygwinsetup.log || GOTO :Error
+)
+
+
+IF NOT "%CYGWIN_QUIET%" == "Y" (
+ REM Like most setup programs, cygwin setup starts the real setup as a separate process, so wait for it.
+ REM This is not required with the -cygquiet=Y and the resulting --no-admin option.
+ :waitsetup
+ tasklist /fi "imagename eq %SETUP%" | find ":" > NUL
+ IF ERRORLEVEL 1 GOTO waitsetup
+)
+
+ECHO ========== CONFIGURE CYGWIN USER ACCOUNT ==========
+
+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
+
+ECHO ========== BUILD COQ ==========
+
+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
+
+%BASH% --login %CYGWIN_INSTALLDIR_CFMT%\build\makecoq_mingw.sh || GOTO :Error
+
+ECHO ========== FINISHED ==========
+
+GOTO :EOF
+
+ECHO ========== BATCH FUNCTIONS ==========
+
+:PrintPars
+ REM 01234567890123456789012345678901234567890123456789012345678901234567890123456789
+ ECHO -arch ^<i686 or x86_64^> Set cygwin, ocaml and coq to 32 or 64 bit
+ ECHO -mode ^<mingwincygwin = install coq in default cygwin mingw sysroot^>
+ ECHO ^<absoloute = install coq in -destcoq absulute path^>
+ ECHO ^<relocatable = install relocatable coq in -destcoq path^>
+ ECHO -installer^<Y or N^> create a windows installer (will be in /build/coq/dev/nsis)
+ ECHO -ocaml ^<Y or N^> install OCaml in Coq folder (Y) or just in cygwin folder (N)
+ ECHO -make ^<Y or N^> install GNU Make in Coq folder (Y) or not (N)
+ ECHO -destcyg ^<path to cygwin destination folder^>
+ ECHO -destcoq ^<path to coq destination folder (mode=absoloute/relocatable)^>
+ ECHO -setup ^<cygwin setup program name^> (auto adjusted to -arch)
+ ECHO -proxy ^<internet proxy^>
+ ECHO -cygrepo ^<cygwin download repository^>
+ ECHO -cygcache ^<local cygwin repository/cache^>
+ ECHO -cyglocal ^<Y or N^> install cygwin from cache
+ ECHO -cygquiet ^<Y or N^> install cygwin without user interaction
+ ECHO -srccache ^<local source code repository/cache^>
+ ECHO -coqver ^<Coq version to install^>
+ ECHO -gtksrc ^<Y or N^> build GTK ^(90 min^) or use cygwin version
+ ECHO -threads ^<1..N^> Number of make threads
+ ECHO(
+ ECHO See ReadMe.txt for a detailed description of all parameters
+ ECHO(
+ ECHO Parameter values (default or currently set):
+ ECHO -arch = %ARCH%
+ ECHO -mode = %INSTALLMODE%
+ ECHO -ocaml = %INSTALLOCAML%
+ ECHO -installer= %MAKEINSTALLER%
+ ECHO -make = %INSTALLMAKE%
+ ECHO -destcyg = %DESTCYG%
+ ECHO -destcoq = %DESTCOQ%
+ ECHO -setup = %SETUP%
+ ECHO -proxy = %PROXY%
+ ECHO -cygrepo = %CYGWIN_REPOSITORY%
+ ECHO -cygcache = %CYGWIN_LOCAL_CACHE_WFMT%
+ ECHO -cyglocal = %CYGWIN_FROM_CACHE%
+ ECHO -cygquiet = %CYGWIN_QUIET%
+ ECHO -srccache = %SOURCE_LOCAL_CACHE_WFMT%
+ ECHO -coqver = %COQ_VERSION%
+ ECHO -gtksrc = %GTK_FROM_SOURCES%
+ ECHO -threads = %MAKE_THREADS%
+ GOTO :EOF
+
+:Error
+ECHO Building Coq failed with error code %errorlevel%
+EXIT /b %errorlevel%
diff --git a/dev/build/windows/MakeCoq_SetRootPath.bat b/dev/build/windows/MakeCoq_SetRootPath.bat
new file mode 100644
index 000000000..3a3711724
--- /dev/null
+++ b/dev/build/windows/MakeCoq_SetRootPath.bat
@@ -0,0 +1,16 @@
+@ ECHO OFF
+
+REM Figure out a root path for coq and cygwin
+
+REM For the \nul trick for testing folders see
+REM https://support.microsoft.com/en-us/kb/65994
+
+IF EXIST D:\bin\nul (
+ SET ROOTPATH=D:\bin
+) else if EXIST C:\bin (
+ SET ROOTPATH=C:\bin
+) else (
+ SET ROOTPATH=C:
+)
+
+ECHO ROOTPATH set to %ROOTPATH%
diff --git a/dev/build/windows/MakeCoq_regtest_noproxy.bat b/dev/build/windows/MakeCoq_regtest_noproxy.bat
new file mode 100644
index 000000000..2b0b83fed
--- /dev/null
+++ b/dev/build/windows/MakeCoq_regtest_noproxy.bat
@@ -0,0 +1,18 @@
+call MakeCoq_SetRootPath
+
+SET HTTP_PROXY=
+EXPORT HTTP_PROXY=
+MKDIR C:\Temp\srccache
+
+call MakeCoq_MinGW.bat ^
+ -arch=64 ^
+ -mode=absolute ^
+ -ocaml=Y ^
+ -make=Y ^
+ -coqver 8.5pl2 ^
+ -srccache C:\Temp\srccache ^
+ -cygquiet=Y ^
+ -destcyg %ROOTPATH%\cygwin_coq64_85pl2_abs ^
+ -destcoq %ROOTPATH%\coq64_85pl2_abs
+
+pause \ No newline at end of file
diff --git a/dev/build/windows/MakeCoq_regtests.bat b/dev/build/windows/MakeCoq_regtests.bat
new file mode 100644
index 000000000..6e36d0140
--- /dev/null
+++ b/dev/build/windows/MakeCoq_regtests.bat
@@ -0,0 +1,16 @@
+SET COQREGTESTING=Y
+
+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 Current stable
+call MakeCoq_85pl3_abs_ocaml.bat
+call MakeCoq_85pl3_installer.bat
+call MakeCoq_85pl3_installer_32.bat
+
+REM Old but might still be used
+call MakeCoq_85pl2_abs_ocaml.bat
+call MakeCoq_84pl6_abs_ocaml.bat
diff --git a/dev/build/windows/ReadMe.txt b/dev/build/windows/ReadMe.txt
new file mode 100644
index 000000000..0faf5bc53
--- /dev/null
+++ b/dev/build/windows/ReadMe.txt
@@ -0,0 +1,460 @@
+==================== Purpose / Goal ====================
+
+The main purpose of these scripts is to build Coq for Windows in a reproducible
+and at least by this script documented way without using binary libraries and
+executables from various sources. These scripts use only MinGW libraries
+provided by Cygwin or compile things from sources. For some libraries there are
+options to build them from sources or to use the Cygwin version.
+
+Another goal (which is not yet achieved) is to have a Coq installer for
+Windows, which includes all tools required for native compute and Coq plugin
+development without Cygwin.
+
+Coq requires OCaml for this and OCaml requires binutils, gcc and a posix shell.
+Since the standard Windows OCaml installation requires Cygwin to deliver some of
+these components, you might be able to imagine that this is not so easy.
+
+These scripts can produce the following:
+
+- Coq running on MinGW
+
+- OCaml producing MinGW code and running on MinGW
+
+- GCC producing MinGW code and running on MinGW
+
+- binutils producing MinGW code and running on MinGW
+
+With "running on MinGW" I mean that the tools accept paths like
+"C:\myfolder\myfile.txt" and that they don't link to a Cygwin or msys DLL. The
+MinGW gcc and binutils provided by Cygwin produce MinGW code, but they run only
+on Cygwin.
+
+With "producing MinGW code" I mean that the programs created by the tools accept
+paths like "C:\myfolder\myfile.txt" and that they don't link to a Cygwin or msys
+DLL.
+
+The missing piece is a posix shell running on plain Windows (without msys or
+Cygwin DLL) and not beeing a binary from obscure sources. I am working on it ...
+
+Since compiling gcc and binutils takes a while and it is not of much use without
+a shell, the building of these components is currently disabled. OCaml is built
+anyway, because this MinGW/MinGW OCaml (rather than a Cygwin/MinGW OCaml) is
+used to compile Coq.
+
+Until the shell is there, the Cygwin created by these scripts is required to run
+OCaml tools. When everything is finished, this will no longer be required.
+
+==================== Usage ====================
+
+The Script MakeCoq_MinGW does:
+- download Cygwin (except the Setup.exe or Setup64.exe)
+- install Cygwin
+- either installs MinGW GTK via Cygwin or compiles it fom sources
+- download, compile and install OCaml, CamlP5, Menhir, lablgtk
+- download, compile and install Coq
+- create a Windows installer (NSIS based)
+
+The parameters are described below. Mostly paths and the HTTP proxy need to be
+set.
+
+There are two main usages:
+
+- Compile and install OCaml and Coq in a given folder
+
+ This works reliably, because absolute library paths can be compiled into Coq
+ and OCaml.
+
+ WARNING: See the "Purpose / Goal" section above for status.
+
+ See MakeCoq_85pl2_abs_ocaml.bat for parameters.
+
+- Create a Windows installer.
+
+ This works well for Coq but not so well for OCaml.
+
+ WARNING: See the "Purpose / Goal" section above for status.
+
+ See MakeCoq_85pl2_installer.bat for parameters.
+
+There is also an option to compile OCaml and Coq inside Cygwin, but this is
+currently not recommended. The resulting Coq and OCaml work, but Coq is slow
+because it scans the largish Cygwin share folder. This will be fixed in a future
+version.
+
+Procedure:
+
+- Unzip contents of CoqSetup.zip in a folder
+
+- Adjust parameters in MakeCoq_85pl2_abs_ocaml.bat or in MakeCoq_85pl2_installer.bat.
+
+- Download Cygwin setup from https://Cygwin.com/install.html
+ For 32 bit Coq : setup-x86.exe (https://Cygwin.com/setup-x86.exe)
+ For 64 bit Coq : setup-x86_64.exe (https://Cygwin.com/setup-x86_64.exe)
+
+- Run MakeCoq_85pl3_abs_ocaml.bat or MakeCoq_85pl3_installer.bat
+
+- Check MakeCoq_regtests.bat to see what combinations of options are tested
+
+==================== MakeCoq_MinGW Parameters ====================
+
+===== -arch =====
+
+Set the target architecture.
+
+Possible values:
+
+32: Install/build Cygwin, ocaml and coq for 32 bit windows
+
+64: Install/build Cygwin, ocaml and coq for 64 bit windows
+
+Default value: 64
+
+
+===== -mode =====
+
+Set the installation mode / target folder structure.
+
+Possible values:
+
+mingwinCygwin: Install coq in the default Cygwin mingw sysroot folder.
+ This is %DESTCYG%\usr\%ARCH%-w64-mingw32\sys-root\mingw.
+ Todo: The coq share folder should be configured to e.g. /share/coq.
+ As is, coqc scans the complete share folder, which slows it down 5x for short files.
+
+absoloute: Install coq in the absolute path given with -destcoq.
+ The resulting Coq will not be relocatable.
+ That is the root folder must not be renamed/moved.
+
+relocatable: Install coq in the absolute path given with -destcoq.
+ The resulting Coq will be relocatable.
+ That is the root folder may be renamed/moved.
+ If OCaml is installed, please note that OCaml cannot be build really relocatable.
+ If the root folder is moved, the environment variable OCAMLLIB must be set to the libocaml sub folder.
+ Also the file <root>\libocaml\ld.conf must be adjusted.
+
+Default value: absolute
+
+
+===== -installer =====
+
+Create a Windows installer (it will be in build/coq-8.xplx/dev/nsis)
+
+Possible values:
+
+Y: Create a windows installer - this forces -mode=relocatable.
+
+N: Don't create a windows installer - use the created Coq installation as is.
+
+Default value: N
+
+
+===== -ocaml =====
+
+Install OCaml for later use with Coq or just for building.
+
+Possible values:
+
+Y: Install OCaml in the same root as Coq (as given with -coqdest)
+ This also copies all .o, .cmo, .a, .cmxa files in the lib folder required for compiling plugins.
+
+N: Install OCaml in the default Cygwin mingw sysroot folder.
+ This is %DESTCYG%\usr\%ARCH%-w64-mingw32\sys-root\mingw.
+
+Default value: N
+
+
+===== -make =====
+
+Build and install MinGW GNU make
+
+Possible values:
+
+Y: Install MinGW GNU make in the same root as Coq (as given with -coqdest).
+
+N: Don't build or install MinGW GNU make.
+ For building everything always Cygwin GNU make is used.
+
+Default value: Y
+
+
+===== -destcyg =====
+
+Destination folder in which Cygwin is installed.
+
+This must be an absolute path in Windows format (with drive letter and \\).
+
+>>>>> This folder may be deleted after the Coq build is finished! <<<<<
+
+Default value: C:\bin\Cygwin_coq
+
+
+===== -destcoq =====
+
+Destination folder in which Coq is installed.
+
+This must be an absolute path in Windows format (with drive letter and \\).
+
+This option is not required if -mode mingwinCygwin is used.
+
+Default value: C:\bin\coq
+
+
+===== -setup =====
+
+Name/path of the Cygwin setup program.
+
+The Cygwin setup program is called setup-x86.exe or setup-x86_64.exe.
+It can be downloaded from: https://Cygwin.com/install.html.
+
+Default value: setup-x86.exe or setup-x86_64.exe, depending on -arch.
+
+
+===== -proxy =====
+
+Internet proxy setting for downloading Cygwin, ocaml and coq.
+
+The format is <server>:<port>, e.g. proxy.mycompany.com:911
+
+The same proxy is used for HTTP, HTTPS and FTP.
+If you need separate proxies for separate protocols, you please put your proxies directly into configure_profile.sh (line 11..13).
+
+Default value: Value of HTTP_PROXY environment variable or none if this variable does not exist.
+
+ATTENTION: With the --proxy setting of the Cygwin setup, it is possible to
+supply a proxy server, but if this parameter is "", Cygwin setup might use proxy
+settings from previous setups. If you once did a Cygwin setup behind a firewall
+and now want to do a Cygwin setup without a firewall, use the -cygquiet=N
+setting to perform a GUI install, where you can adjust the proxy setting.
+
+===== -cygrepo =====
+
+The online repository, from which Cygwin packages are downloaded.
+
+Note: although most repositories end with Cygwin32, they are good for 32 and 64 bit Cygwin.
+
+Default value: http://ftp.inf.tu-dresden.de/software/windows/Cygwin32
+
+>>>>> If you are not in Europe, you might want to change this! <<<<<
+
+
+===== -cygcache =====
+
+The local cache folder for Cygwin repositories.
+
+You can also copy files here from a backup/reference and set -cyglocal.
+The setup will then not download/update from the internet but only use the local cache.
+
+Default value: <folder of MakeCoq_MinGW.bat>\Cygwin_cache
+
+
+===== -cyglocal =====
+
+Control if the Cygwin setup uses the latest version from the internet or the version as is in the local folder.
+
+Possible values:
+
+Y: Install exactly the Cygwin version from the local repository cache.
+ Don't update from the internet.
+
+N: Download the latest Cygwin version from the internet.
+ Update the local repository cache with the latest version.
+
+Default value: N
+
+
+===== -cygquiet =====
+
+Control if the Cygwin setup runs quitely or interactive.
+
+Possible values:
+
+Y: Install Cygwin quitely without user interaction.
+
+N: Install Cygwin interactively (allows to select additional packages).
+
+Default value: Y
+
+
+===== -srccache =====
+
+The local cache folder for ocaml/coq/... sources.
+
+Default value: <folder of MakeCoq_MinGW.bat>\source_cache
+
+
+===== -coqver =====
+
+The version of Coq to download and compile.
+
+Possible values: 8.4pl6, 8.5pl2, 8.5pl3, git-v8.6
+ Others might work, but are untested.
+ 8.4 is only tested in mode=absoloute
+
+Default value: 8.5pl3
+
+If git- is prepended, the Coq sources are loaded from git.
+
+ATTENTION: with default options, the scripts cache source tar balls in two
+places, the <destination>/build/tarballs folder and the <scripts>/source_cache
+folder. If you modified something in git, you need to delete the cached tar ball
+in both places!
+
+===== -gtksrc =====
+
+Control if GTK and its prerequisites are build from sources or if binary MinGW packages from Cygwin are used
+
+Possible values:
+
+Y: Build GTK from sources, takes about 90 minutes extra.
+ This is useful, if you want to debug/fix GTK or library issues.
+
+N: Use prebuilt MinGW libraries from Cygwin
+
+
+===== -threads =====
+
+Control the maximum number of make threads for modules which support parallel make.
+
+Possible values: 1..N.
+ Should not be more than 1.5x the number of cores.
+ Should not be more than available RAM/2GB (e.g. 4 for 8GB)
+
+
+==================== TODO ====================
+
+- Installer doesn't remove OCAMLLIB environment variables (it is in the script, but doesn't seem to work)
+- CoqIDE doesn't find theme files
+- Finish / test mingw_in_Cygwin mode (coqide doesn't start, coqc slow cause of scanning complete share folder)
+- Possibly create/login as specific user to bash (not sure if it makes sense - nead to create additional bash login link then)
+- maybe move share/doc/menhir somehwere else (reduces coqc startup time)
+- Use original installed file list for removing files in uninstaller
+
+==================== Issues with relocation ====================
+
+Coq and OCaml are built in a specific folder and are not really intended for relocation e.g. by an installer.
+Some absolute paths in config files are patched in coq_new.nsi.
+
+Coq is made fairly relocatable by first configuring it with PREFIX=./ and then PREFIX=<installdir>.
+OCaml is made relocatable mostly by defining the OCAMLLIB environment variable and by patching some files.
+If you have issues with one of the remaining (unpatched) files below, please let me know.
+
+Text files patched by the installer:
+
+./ocamllib/ld.conf
+./etc/findlib.conf:destdir="D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib"
+./etc/findlib.conf:path="D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib"
+
+Text files containing the install folder path after install:
+
+./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
+./libocaml/site-lib/findlib/Makefile.config:OCAML_SITELIB=D:/bin/coq64_buildtest_reloc_ocaml20\libocaml\site-lib
+./libocaml/site-lib/findlib/Makefile.config:OCAMLFIND_BIN=D:/bin/coq64_buildtest_reloc_ocaml20\bin
+./libocaml/site-lib/findlib/Makefile.config:OCAMLFIND_CONF=D:/bin/coq64_buildtest_reloc_ocaml20\etc\findlib.conf
+./libocaml/topfind:#directory "D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib/findlib";;
+./libocaml/topfind: Topdirs.dir_load Format.err_formatter "D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib/findlib/findlib.cma";
+./libocaml/topfind: Topdirs.dir_load Format.err_formatter "D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib/findlib/findlib_top.cma";
+./libocaml/topfind:(* #load "D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib/findlib/findlib.cma";; *)
+./libocaml/topfind:(* #load "D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib/findlib/findlib_top.cma";; *)
+./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:
+
+$ find . -type f -exec grep "Cygwin_coq64_buildtest_reloc_ocaml20" {} /dev/null \;
+Binary file ./bin/coqtop.byte.exe matches
+Binary file ./bin/coqtop.exe matches
+Binary file ./bin/ocamldoc.exe matches
+Binary file ./bin/ocamldoc.opt.exe matches
+Binary file ./libocaml/ocamldoc/odoc_info.a matches
+Binary file ./libocaml/ocamldoc/odoc_info.cma matches
+
+Binary files containing the install folder path after install:
+
+$ find . -type f -exec grep "coq64_buildtest_reloc_ocaml20" {} /dev/null \;
+Binary file ./bin/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
+Binary file ./bin/coqdoc.exe matches
+Binary file ./bin/coqide.exe matches
+Binary file ./bin/coqmktop.exe matches
+Binary file ./bin/coqtop.byte.exe matches
+Binary file ./bin/coqtop.exe matches
+Binary file ./bin/coqworkmgr.exe matches
+Binary file ./bin/coq_makefile.exe matches
+Binary file ./bin/menhir matches
+Binary file ./bin/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
+Binary file ./bin/ocamldep.exe matches
+Binary file ./bin/ocamldep.opt.exe matches
+Binary file ./bin/ocamldoc.exe matches
+Binary file ./bin/ocamldoc.opt.exe matches
+Binary file ./bin/ocamlfind.exe matches
+Binary file ./bin/ocamlmklib.exe matches
+Binary file ./bin/ocamlmktop.exe matches
+Binary file ./bin/ocamlobjinfo.exe matches
+Binary file ./bin/ocamlopt.exe matches
+Binary file ./bin/ocamlopt.opt.exe matches
+Binary file ./bin/ocamlprof.exe matches
+Binary file ./bin/ocamlrun.exe matches
+Binary file ./bin/ocpp5.exe matches
+Binary file ./lib/config/coq_config.cmo matches
+Binary file ./lib/config/coq_config.o matches
+Binary file ./lib/grammar/grammar.cma matches
+Binary file ./lib/ide/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
+Binary file ./libocaml/expunge.exe matches
+Binary file ./libocaml/extract_crc.exe matches
+Binary file ./libocaml/libcamlrun.a matches
+Binary file ./libocaml/ocamlbuild/ocamlbuildlib.a matches
+Binary file ./libocaml/ocamlbuild/ocamlbuildlib.cma matches
+Binary file ./libocaml/ocamldoc/odoc_info.a matches
+Binary file ./libocaml/ocamldoc/odoc_info.cma matches
+Binary file ./libocaml/site-lib/findlib/findlib.a matches
+Binary file ./libocaml/site-lib/findlib/findlib.cma matches
+Binary file ./libocaml/site-lib/findlib/findlib.cmxs matches
diff --git a/dev/build/windows/configure_profile.sh b/dev/build/windows/configure_profile.sh
new file mode 100644
index 000000000..09a9cf35a
--- /dev/null
+++ b/dev/build/windows/configure_profile.sh
@@ -0,0 +1,32 @@
+#!/bin/bash
+
+rcfile=~/.bash_profile
+donefile=~/.bash_profile.upated
+
+if [ ! -f $donefile ] ; then
+
+ echo >> $rcfile
+
+ if [ -n "$1" ]; then
+ echo export http_proxy="http://$1" >> $rcfile
+ echo export https_proxy="http://$1" >> $rcfile
+ echo export ftp_proxy="http://$1" >> $rcfile
+ fi
+
+ mkdir -p $RESULT_INSTALLDIR_CFMT/bin
+
+ # A tightly controlled path helps to avoid issues
+ # Note: the order is important: first have the cygwin binaries, then the mingw binaries in the path!
+ # Note: /bin is mounted at /usr/bin and /lib at /usr/lib and it is common to use /usr/bin in PATH
+ # See cat /proc/mounts
+ echo "export PATH=/usr/local/bin:/usr/bin:$RESULT_INSTALLDIR_CFMT/bin:/usr/$TARGET_ARCH/sys-root/mingw/bin:/cygdrive/c/Windows/system32:/cygdrive/c/Windows" >> $rcfile
+
+ # find and xargs complain if the environment is larger than (I think) 8k.
+ # ORIGINAL_PATH (set by cygwin) can be a few k and exceed the limit
+ echo unset ORIGINAL_PATH >> $rcfile
+
+ # Other installations of OCaml will mess up things
+ echo unset OCAMLLIB >> $rcfile
+
+ touch $donefile
+fi \ No newline at end of file
diff --git a/dev/build/windows/difftar-folder.sh b/dev/build/windows/difftar-folder.sh
new file mode 100644
index 000000000..65278d5c9
--- /dev/null
+++ b/dev/build/windows/difftar-folder.sh
@@ -0,0 +1,86 @@
+#!/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
+#
+# With very valuable help on building GTK from
+# https://wiki.gnome.org/Projects/GTK+/Win32/MSVCCompilationOfGTKStack
+# http://www.gaia-gis.it/spatialite-3.0.0-BETA/mingw64_how_to.html
+
+###################### Script safety and debugging settings ######################
+
+set -o nounset
+
+# Print usage
+
+if [ "$#" -lt 1 ] ; 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.'
+ exit 1
+fi
+
+# Parse parameters
+
+tarfile=$1
+
+if [ "$#" -ge 2 ] ; then
+ folder=$2
+else
+ folder=.
+fi
+
+if [ "$#" -ge 3 ] ; then
+ strip=$3
+else
+ strip=0
+fi
+
+# Get path prefix if --strip is used
+
+if [ "$strip" -gt 0 ] ; then
+ prefix=`tar -t -f $tarfile | head -1`
+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
+mkdir -p "$orig"
+
+
+# Make sure tar uses english output (for Mod time differs)
+export LC_ALL=C
+
+# Search all files with a deviating modification time using tar --diff
+tar --diff -a -f "$tarfile" --strip $strip --directory "$folder" | grep "Mod time differs" | while read -r file ; do
+ # Substitute ': Mod time differs' with nothing
+ file=${file/: Mod time differs/}
+ # Check if file exists
+ if [ -f "$folder/$file" ] ; then
+ # Extract original file
+ tar -x -a -f "$tarfile" --strip $strip --directory "$orig" "$prefix$file"
+ # Compute diff
+ diff -u "$orig/$file" "$folder/$file"
+ fi
+done \ No newline at end of file
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
new file mode 100644
index 000000000..bfc7ce4dd
--- /dev/null
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -0,0 +1,1271 @@
+#!/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
+#
+# With very valuable help on building GTK from
+# https://wiki.gnome.org/Projects/GTK+/Win32/MSVCCompilationOfGTKStack
+# http://www.gaia-gis.it/spatialite-3.0.0-BETA/mingw64_how_to.html
+
+###################### Script safety and debugging settings ######################
+
+set -o nounset
+set -o errexit
+set -x
+
+# Set this to 1 if all module directories shall be removed before build (no incremental make)
+RMDIR_BEFORE_BUILD=1
+
+###################### NOTES #####################
+
+# - This file goes together with MakeCoq_ForMignGW.bat, which sets up cygwin
+# with all required packages and then calls this script.
+#
+# - This script uses set -o errexit, so if anything fails, the script will stop
+#
+# - cygwin provided mingw64 packages like mingw64-x86_64-zlib are installed to
+# /usr/$TARGET_ARCH/sys-root/mingw, so we use this as install prefix
+#
+# - if mingw64-x86_64-pkg-config is installed BEFORE building libpng or pixman,
+# the .pc files are properly created in /usr/$TARGET_ARCH/sys-root/mingw/lib/pkgconfig
+#
+# - pango and some others uses pkg-config executable names without path, which doesn't work in cross compile mode
+# There are several possible solutions
+# 1.) patch build files to get the prefix from pkg-config and use $prefix/bin/ as path
+# - doesn't work for pango because automake goes wild
+# - mingw tools are not able to handle cygwin path (they need absolute windows paths)
+# 2.) export PATH=$PATH:/usr/$TARGET_ARCH/sys-root/mingw/bin
+# - a bit dangerous because this exposes much more than required
+# - mingw tools are not able to handle cygwin path (they need absolute windows paths)
+# 3.) Install required tools via cygwin modules libglib2.0-devel and libgdk_pixbuf2.0-devel
+# - Possibly version compatibility issues
+# - Possibly mingw/cygwin compatibility issues, e.g. when building font or terminfo databases
+# 4.) Build required tools for mingw and cygwin
+# - Possibly mingw/cygwin compatibility issues, e.g. when building font or terminfo databases
+#
+# We use method 3 below
+# Method 2 can be tried by putting the cross tools in the path before the cygwin tools (in configure_profile.sh)
+#
+# - It is tricky to build 64 bit binaries with 32 bit cross tools and vice versa.
+# This is because the linker needs to load DLLs from C:\windows\system32, which contains
+# both 32 bit and 64 bit DLLs, and which one you get depends by some black magic on if the using
+# app is a 32 bit or 64 bit app. So better build 32 bit mingw with 32 bit cygwin and 64 with 64.
+# Alternatively the required 32 bit or 64 bit DLLs need to be copied with a 32 bit/64bit cp to some
+# folder without such black magic.
+#
+# - The file selection for the Coq Windows Installer is done with make install (unlike the original script)
+# Relocatble builds are first configured with prefix=./ then build and then
+# reconfigured with prefix=<installroot> before make install.
+
+
+###################### ARCHITECTURES #####################
+
+# The OS on which the build of the tool/lib runs
+BUILD=`gcc -dumpmachine`
+
+# The OS on which the tool runs
+# "`find /bin -name "*mingw32-gcc.exe"`" -dumpmachine
+HOST=$TARGET_ARCH
+
+# The OS for which the tool creates code/for which the libs are
+TARGET=$TARGET_ARCH
+
+# Cygwin uses different arch name for 32 bit than mingw/gcc
+case $ARCH in
+ x86_64) CYGWINARCH=x86_64 ;;
+ i686) CYGWINARCH=x86 ;;
+ *) false ;;
+esac
+
+###################### PATHS #####################
+
+# Name and create some 'global' folders
+PATCHES=/build/patches
+BUILDLOGS=/build/buildlogs
+FLAGFILES=/build/flagfiles
+TARBALLS=/build/tarballs
+FILELISTS=/build/filelists
+
+mkdir -p $BUILDLOGS
+mkdir -p $FLAGFILES
+mkdir -p $TARBALLS
+mkdir -p $FILELISTS
+cd /build
+
+
+# sysroot prefix for the above /build/host/target combination
+PREFIX=$CYGWIN_INSTALLDIR_MFMT/usr/$TARGET_ARCH/sys-root/mingw
+
+# Install / Prefix folder for COQ
+PREFIXCOQ=$RESULT_INSTALLDIR_MFMT
+
+# Install / Prefix folder for OCaml
+if [ "$INSTALLOCAML" == "Y" ]; then
+ PREFIXOCAML=$PREFIXCOQ
+else
+ PREFIXOCAML=$PREFIX
+fi
+
+mkdir -p $PREFIX/bin
+mkdir -p $PREFIXCOQ/bin
+mkdir -p $PREFIXOCAML/bin
+
+###################### Copy Cygwin Setup Info #####################
+
+# Copy Cygwin repo ini file and installed files db to tarballs folder.
+# Both files together document the exact selection and version of cygwin packages.
+# Do this as early as possible to avoid changes by other setups (the repo folder is shared).
+
+# Escape URL to folder name
+CYGWIN_REPO_FOLDER=${CYGWIN_REPOSITORY}/
+CYGWIN_REPO_FOLDER=${CYGWIN_REPO_FOLDER//:/%3a}
+CYGWIN_REPO_FOLDER=${CYGWIN_REPO_FOLDER//\//%2f}
+
+# Copy files
+cp $CYGWIN_LOCAL_CACHE_WFMT/$CYGWIN_REPO_FOLDER/$CYGWINARCH/setup.ini $TARBALLS
+cp /etc/setup/installed.db $TARBALLS
+
+###################### LOGGING #####################
+
+# The folder which receives log files
+mkdir -p buildlogs
+LOGS=`pwd`/buildlogs
+
+# The current log target (first part of the log file name)
+LOGTARGET=other
+
+log1() {
+ "$@" > $LOGS/$LOGTARGET-$1.log 2> $LOGS/$LOGTARGET-$1.err
+}
+
+log2() {
+ "$@" > $LOGS/$LOGTARGET-$1-$2.log 2> $LOGS/$LOGTARGET-$1-$2.err
+}
+
+log_1_3() {
+ "$@" > $LOGS/$LOGTARGET-$1-$3.log 2> $LOGS/$LOGTARGET-$1-$3.err
+}
+
+logn() {
+ LOGTARGETEX=$1
+ shift
+ "$@" > $LOGS/$LOGTARGET-$LOGTARGETEX.log 2> $LOGS/$LOGTARGET-$LOGTARGETEX.err
+}
+
+###################### UTILITY FUNCTIONS #####################
+
+# ------------------------------------------------------------------------------
+# Get a source tar ball, expand and patch it
+# - get source archive from $SOURCE_LOCAL_CACHE_CFMT or online using wget
+# - create build folder
+# - extract source archive
+# - patch source file if patch exists
+#
+# Parameters
+# $1 file server name including protocol prefix
+# $2 file name (without extension)
+# $3 file extension
+# $4 number of path levels to strip from tar (usually 1)
+# $5 module name (if different from archive)
+# $6 expand folder name (if different from module name)
+# ------------------------------------------------------------------------------
+
+function get_expand_source_tar {
+ # Handle optional parameters
+ if [ "$#" -ge 4 ] ; then
+ strip=$4
+ else
+ strip=1
+ fi
+
+ if [ "$#" -ge 5 ] ; then
+ name=$5
+ else
+ name=$2
+ fi
+
+ if [ "$#" -ge 6 ] ; then
+ folder=$6
+ else
+ folder=$name
+ fi
+
+ # Set logging target
+ logtargetold=$LOGTARGET
+ LOGTARGET=$name
+
+ # Get the source archive either from the source cache or online
+ if [ ! -f $TARBALLS/$name.$3 ] ; then
+ if [ -f $SOURCE_LOCAL_CACHE_CFMT/$name.$3 ] ; then
+ cp $SOURCE_LOCAL_CACHE_CFMT/$name.$3 $TARBALLS
+ else
+ wget $1/$2.$3
+ if [ ! "$2.$3" == "$name.$3" ] ; then
+ mv $2.$3 $name.$3
+ fi
+ mv $name.$3 $TARBALLS
+ # Save the source archive in the source cache
+ if [ -d $SOURCE_LOCAL_CACHE_CFMT ] ; then
+ cp $TARBALLS/$name.$3 $SOURCE_LOCAL_CACHE_CFMT
+ fi
+ fi
+ fi
+
+ # Remove build directory (clean build)
+ if [ $RMDIR_BEFORE_BUILD -eq 1 ] ; then
+ rm -f -r $folder
+ fi
+
+ # Create build directory and cd
+ mkdir -p $folder
+ cd $folder
+
+ # Extract source archive
+ if [ "$3" == "zip" ] ; then
+ log1 unzip $TARBALLS/$name.$3
+ if [ "$strip" == "1" ] ; then
+ # Ok, this is dirty, but it works and it fails if there are name clashes
+ mv */* .
+ else
+ echo "Unzip strip count not supported"
+ return 1
+ fi
+ else
+ logn untar tar xvaf $TARBALLS/$name.$3 --strip $strip
+ fi
+
+ # Patch if patch file exists
+ if [ -f $PATCHES/$name.patch ] ; then
+ log1 patch -p1 -i $PATCHES/$name.patch
+ fi
+
+ # Go back to base folder
+ cd ..
+
+ LOGTARGET=$logtargetold
+}
+
+# ------------------------------------------------------------------------------
+# Prepare a module build
+# - check if build is already done (name.finished file exists) - if so return 1
+# - create name.started
+# - get source archive from $SOURCE_LOCAL_CACHE_CFMT or online using wget
+# - create build folder
+# - cd to build folder and extract source archive
+# - create bin_special subfolder and add it to $PATH
+# - remember things for build_post
+#
+# Parameters
+# $1 file server name including protocol prefix
+# $2 file name (without extension)
+# $3 file extension
+# $4 [optional] number of path levels to strip from tar (usually 1)
+# $5 [optional] module name (if different from archive)
+# ------------------------------------------------------------------------------
+
+function build_prep {
+ # Handle optional parameters
+ if [ "$#" -ge 4 ] ; then
+ strip=$4
+ else
+ strip=1
+ fi
+
+ if [ "$#" -ge 5 ] ; then
+ name=$5
+ else
+ name=$2
+ fi
+
+ # Check if build is already done
+ if [ ! -f flagfiles/$name.finished ] ; then
+ BUILD_PACKAGE_NAME=$name
+ BUILD_OLDPATH=$PATH
+ BUILD_OLDPWD=`pwd`
+ LOGTARGET=$name
+
+ touch flagfiles/$name.started
+
+ get_expand_source_tar $1 $2 $3 $strip $name
+
+ cd $name
+
+ # Create a folder and add it to path, where we can put special binaries
+ # The path is restored in build_post
+ mkdir bin_special
+ PATH=`pwd`/bin_special:$PATH
+
+ return 0
+ else
+ return 1
+ fi
+}
+
+# ------------------------------------------------------------------------------
+# Finalize a module build
+# - create name.finished
+# - go back to base folder
+# ------------------------------------------------------------------------------
+
+function build_post {
+ if [ ! -f flagfiles/$BUILD_PACKAGE_NAME.finished ]; then
+ cd $BUILD_OLDPWD
+ touch flagfiles/$BUILD_PACKAGE_NAME.finished
+ PATH=$BUILD_OLDPATH
+ LOGTARGET=other
+ fi
+}
+
+# ------------------------------------------------------------------------------
+# Build and install a module using the standard configure/make/make install process
+# - prepare build (as above)
+# - configure
+# - make
+# - make install
+# - finalize build (as above)
+#
+# parameters
+# $1 file server name including protocol prefix
+# $2 file name (without extension)
+# $3 file extension
+# $4 patch function to call between untar and configure (or true if none)
+# $5.. extra configure arguments
+# ------------------------------------------------------------------------------
+
+function build_conf_make_inst {
+ if build_prep $1 $2 $3 ; then
+ $4
+ logn configure ./configure --build=$BUILD --host=$HOST --target=$TARGET --prefix=$PREFIX "${@:5}"
+ log1 make $MAKE_OPT
+ log2 make install
+ log2 make clean
+ build_post
+ fi
+}
+
+# ------------------------------------------------------------------------------
+# Install all files given by a glob pattern to a given folder
+#
+# parameters
+# $1 glob pattern (in '')
+# $2 target folder
+# ------------------------------------------------------------------------------
+
+function install_glob {
+ # Check if any files matching the pattern exist
+ if [ "$(echo $1)" != "$1" ] ; then
+ install -D -t $2 $1
+ fi
+}
+
+
+# ------------------------------------------------------------------------------
+# Recursively Install all files given by a glob pattern to a given folder
+#
+# parameters
+# $1 source path
+# $2 pattern (in '')
+# $3 target folder
+# ------------------------------------------------------------------------------
+
+function install_rec {
+ ( cd $1 && find -type f -name "$2" -exec install -D -T $1/{} $3/{} \; )
+}
+
+# ------------------------------------------------------------------------------
+# Write a file list of the target folder
+# The file lists are used to create file lists for the windows installer
+#
+# parameters
+# $1 name of file list
+# ------------------------------------------------------------------------------
+
+function list_files {
+ if [ ! -e "/build/filelists/$1" ] ; then
+ ( cd $PREFIXCOQ && find -type f | sort > /build/filelists/$1 )
+ fi
+}
+
+# ------------------------------------------------------------------------------
+# Compute the set difference of two file lists
+#
+# parameters
+# $1 name of list A-B (set difference of set A minus set B)
+# $2 name of list A
+# $3 name of list B
+# ------------------------------------------------------------------------------
+
+function diff_files {
+ # See http://www.catonmat.net/blog/set-operations-in-unix-shell/ for file list set operations
+ comm -23 <(sort "/build/filelists/$2") <(sort "/build/filelists/$3") > "/build/filelists/$1"
+}
+
+# ------------------------------------------------------------------------------
+# Filter a list of files with a regular expression
+#
+# parameters
+# $1 name of output file list
+# $2 name of input file list
+# $3 name of filter regexp
+# ------------------------------------------------------------------------------
+
+function filter_files {
+ egrep "$3" "/build/filelists/$2" > "/build/filelists/$1"
+}
+
+# ------------------------------------------------------------------------------
+# Convert a file list to NSIS installer format
+#
+# parameters
+# $1 name of file list file (output file is the same with extension .nsi)
+# ------------------------------------------------------------------------------
+
+function files_to_nsis {
+ # Split the path in the file list into path and filename and create SetOutPath and File instructions
+ # Note: File /oname cannot be used, because it does not create the paths as SetOutPath does
+ # Note: I didn't check if the redundant SetOutPath instructions have a bad impact on installer size or install time
+ cat "/build/filelists/$1" | tr '/' '\\' | sed -r 's/^\.(.*)\\([^\\]+)$/SetOutPath $INSTDIR\\\1\nFile ${COQ_SRC_PATH}\\\1\\\2/' > "/build/filelists/$1.nsh"
+}
+
+
+###################### MODULE BUILD FUNCTIONS #####################
+
+##### LIBPNG #####
+
+function make_libpng {
+ build_conf_make_inst http://prdownloads.sourceforge.net/libpng libpng-1.6.18 tar.gz true
+}
+
+##### PIXMAN #####
+
+function make_pixman {
+ build_conf_make_inst http://cairographics.org/releases pixman-0.32.8 tar.gz true
+}
+
+##### FREETYPE #####
+
+function make_freetype {
+ build_conf_make_inst http://sourceforge.net/projects/freetype/files/freetype2/2.6.1 freetype-2.6.1 tar.bz2 true
+}
+
+##### EXPAT #####
+
+function make_expat {
+ build_conf_make_inst http://sourceforge.net/projects/expat/files/expat/2.1.0 expat-2.1.0 tar.gz true
+}
+
+##### FONTCONFIG #####
+
+function make_fontconfig {
+ make_freetype
+ make_expat
+ # CONFIGURE PARAMETERS
+ # build/install fails without --disable-docs
+ build_conf_make_inst http://www.freedesktop.org/software/fontconfig/release fontconfig-2.11.94 tar.gz true --disable-docs
+}
+
+##### ICONV #####
+
+function make_libiconv {
+ build_conf_make_inst http://ftp.gnu.org/pub/gnu/libiconv libiconv-1.14 tar.gz true
+}
+
+##### UNISTRING #####
+
+function make_libunistring {
+ build_conf_make_inst http://ftp.gnu.org/gnu/libunistring libunistring-0.9.5 tar.xz true
+}
+
+##### NCURSES #####
+
+function make_ncurses {
+ # NOTE: ncurses is not required below. This is just kept for documentary purposes in case I need it later.
+ #
+ # NOTE: make install fails building the terminfo database because
+ # : ${TIC_PATH:=unknown} in run_tic.sh
+ # As a result pkg-config .pc files are not generated
+ # Also configure of gettext gives two "considers"
+ # checking where terminfo library functions come from... not found, consider installing GNU ncurses
+ # checking where termcap library functions come from... not found, consider installing GNU ncurses
+ # gettext make/make install work anyway
+ #
+ # CONFIGURE PARAMETERS
+ # --enable-term-driver --enable-sp-funcs is rewuired for mingw (see README.MinGW)
+ # additional changes
+ # ADD --with-pkg-config
+ # ADD --enable-pc-files
+ # ADD --without-manpages
+ # REM --with-pthread
+ build_conf_make_inst http://ftp.gnu.org/gnu/ncurses ncurses-5.9 tar.gz true --disable-home-terminfo --enable-reentrant --enable-sp-funcs --enable-term-driver --enable-interop --with-pkg-config --enable-pc-files --without-manpages
+}
+
+##### GETTEXT #####
+
+function make_gettext {
+ # Cygwin packet dependencies: (not 100% sure) libiconv-devel,libunistring-devel,libncurses-devel
+ # Cygwin packet dependencies for gettext users: (not 100% sure) gettext-devel,libgettextpo-devel
+ # gettext configure complains that ncurses is also required, but it builds without it
+ # Ncurses is tricky to install/configure for mingw64, so I dropped ncurses
+ make_libiconv
+ make_libunistring
+ build_conf_make_inst http://ftp.gnu.org/pub/gnu/gettext gettext-0.19 tar.gz true
+}
+
+##### LIBFFI #####
+
+function make_libffi {
+ # NOTE: The official download server is down ftp://sourceware.org/pub/libffi/libffi-3.2.1.tar.gz
+ build_conf_make_inst http://www.mirrorservice.org/sites/sourceware.org/pub/libffi libffi-3.2.1 tar.gz true
+}
+
+##### LIBEPOXY #####
+
+function make_libepoxy {
+ build_conf_make_inst https://github.com/anholt/libepoxy/releases/download/v1.3.1 libepoxy-1.3.1 tar.bz2 true
+}
+
+##### LIBPCRE #####
+
+function make_libpcre {
+ build_conf_make_inst ftp://ftp.csx.cam.ac.uk/pub/software/programming/pcre pcre-8.39 tar.bz2 true
+}
+
+function make_libpcre2 {
+ build_conf_make_inst ftp://ftp.csx.cam.ac.uk/pub/software/programming/pcre pcre2-10.22 tar.bz2 true
+}
+
+##### GLIB #####
+
+function make_glib {
+ # Cygwin packet dependencies: mingw64-x86_64-zlib
+ make_gettext
+ make_libffi
+ make_libpcre
+ # build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/glib/2.46 glib-2.46.0 tar.xz true
+ build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/glib/2.47 glib-2.47.5 tar.xz true
+}
+
+##### ATK #####
+
+function make_atk {
+ make_gettext
+ make_glib
+ build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/atk/2.18 atk-2.18.0 tar.xz true
+}
+
+##### PIXBUF #####
+
+function make_gdk-pixbuf {
+ # Cygwin packet dependencies: mingw64-x86_64-zlib
+ make_libpng
+ make_gettext
+ make_glib
+ # CONFIGURE PARAMETERS
+ # --with-included-loaders=yes statically links the image file format handlers
+ # This avoids "Cannot open pixbuf loader module file '/usr/x86_64-w64-mingw32/sys-root/mingw/lib/gdk-pixbuf-2.0/2.10.0/loaders.cache': No such file or directory"
+ build_conf_make_inst http://ftp.gnome.org/pub/GNOME/sources/gdk-pixbuf/2.32 gdk-pixbuf-2.32.1 tar.xz true --with-included-loaders=yes
+}
+
+##### CAIRO #####
+
+function make_cairo {
+ # Cygwin packet dependencies: mingw64-x86_64-zlib
+ make_libpng
+ make_glib
+ make_pixman
+ make_fontconfig
+ build_conf_make_inst http://cairographics.org/releases cairo-1.14.2 tar.xz true
+}
+
+##### PANGO #####
+
+function make_pango {
+ make_cairo
+ make_glib
+ make_fontconfig
+ build_conf_make_inst http://ftp.gnome.org/pub/GNOME/sources/pango/1.38 pango-1.38.0 tar.xz true
+}
+
+##### GTK2 #####
+
+function patch_gtk2 {
+ rm gtk/gtk.def
+}
+
+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.28 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.16 gtk+-3.16.7 tar.xz true
+
+ # make all incl. tests and examples runs through fine
+ # make install fails with issue with
+ #
+ # make[5]: Entering directory '/home/soegtrop/GTK/gtk+-3.16.7/demos/gtk-demo'
+ # test -n "" || ../../gtk/gtk-update-icon-cache --ignore-theme-index --force "/usr/x86_64-w64-mingw32/sys-root/mingw/share/icons/hicolor"
+ # gtk-update-icon-cache.exe: Failed to open file /usr/x86_64-w64-mingw32/sys-root/mingw/share/icons/hicolor/.icon-theme.cache : No such file or directory
+ # Makefile:1373: recipe for target 'install-update-icon-cache' failed
+ # make[5]: *** [install-update-icon-cache] Error 1
+ # make[5]: Leaving directory '/home/soegtrop/GTK/gtk+-3.16.7/demos/gtk-demo'
+}
+
+##### LIBXML2 #####
+
+function make_libxml2 {
+ # Cygwin packet dependencies: libtool automake
+ # Note: latest release version 2.9.2 fails during configuring lzma, so using 2.9.1
+ # Note: python binding requires <sys/select.h> which doesn't exist on cygwin
+ if build_prep https://git.gnome.org/browse/libxml2/snapshot libxml2-2.9.1 tar.xz ; then
+ # ./autogen.sh --build=$BUILD --host=$HOST --target=$TARGET --prefix=$PREFIX --disable-shared --without-python
+ # shared library required by gtksourceview
+ ./autogen.sh --build=$BUILD --host=$HOST --target=$TARGET --prefix=$PREFIX --without-python
+ log1 make $MAKE_OPT all
+ log2 make install
+ log2 make clean
+ build_post
+ fi
+}
+
+##### GTK-SOURCEVIEW2 #####
+
+function make_gtk_sourceview2 {
+ # 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_libxml2
+ build_conf_make_inst https://download.gnome.org/sources/gtksourceview/2.11 gtksourceview-2.11.2 tar.bz2 true
+ fi
+}
+
+##### FLEXDLL FLEXLINK #####
+
+# Note: there is a circular dependency between flexlink and ocaml (resolved in Ocaml 4.03.)
+# For MinGW it is not even possible to first build an Ocaml without flexlink support,
+# Because Makefile.nt doesn't support this. So we have to use a binary flexlink.
+# One could of cause do a bootstrap run ...
+
+# Install flexdll objects
+
+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
+ elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then
+ cp flexdll*_mingw64.o /usr/$TARGET_ARCH/bin
+ cp flexdll*_mingw64.o $PREFIXOCAML/bin
+ else
+ echo "Unknown target architecture"
+ return 1
+ fi
+}
+
+# Install flexlink
+
+function install_flexlink {
+ cp flexlink.exe /usr/$TARGET_ARCH/bin
+
+ cp flexlink.exe $PREFIXOCAML/bin
+}
+
+# Get binary flexdll flexlink for building OCaml
+# An alternative is to first build an OCaml without shared library support and build flexlink with it
+
+function get_flex_dll_link_bin {
+ if build_prep http://alain.frisch.fr/flexdll flexdll-bin-0.34 zip 1 ; then
+ install_flexdll
+ install_flexlink
+ build_post
+ fi
+}
+
+# Build flexdll and flexlink from sources after building OCaml
+
+function make_flex_dll_link {
+ if build_prep http://alain.frisch.fr/flexdll flexdll-0.34 tar.gz ; then
+ if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then
+ log1 make $MAKE_OPT build_mingw flexlink.exe
+ elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then
+ log1 make $MAKE_OPT build_mingw64 flexlink.exe
+ else
+ echo "Unknown target architecture"
+ return 1
+ fi
+ install_flexdll
+ install_flexlink
+ log2 make clean
+ build_post
+ fi
+}
+
+##### LN replacement #####
+
+# Note: this does support symlinks, but symlinks require special user rights on Windows.
+# ocamlbuild uses symlinks to link the executables in the build folder to the base folder.
+# For this purpose hard links are better.
+
+function make_ln {
+ if [ ! -f flagfiles/myln.finished ] ; then
+ touch flagfiles/myln.started
+ mkdir -p myln
+ cd myln
+ cp $PATCHES/ln.c .
+ $TARGET_ARCH-gcc -DUNICODE -D_UNICODE -DIGNORE_SYMBOLIC -mconsole -o ln.exe ln.c
+ install -D ln.exe $PREFIXCOQ/bin/ln.exe
+ cd ..
+ touch flagfiles/myln.finished
+ fi
+}
+
+##### OCAML #####
+
+function make_ocaml {
+ get_flex_dll_link_bin
+ if build_prep http://caml.inria.fr/pub/distrib/ocaml-4.02 ocaml-4.02.3 tar.gz 1 ; then
+ # if build_prep http://caml.inria.fr/pub/distrib/ocaml-4.01 ocaml-4.01.0 tar.gz 1 ; then
+ # See README.win32
+ cp config/m-nt.h config/m.h
+ cp config/s-nt.h config/s.h
+ if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then
+ cp config/Makefile.mingw config/Makefile
+ elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then
+ cp config/Makefile.mingw64 config/Makefile
+ else
+ echo "Unknown target architecture"
+ return 1
+ fi
+
+ # Prefix is fixed in make file - replace it with the real one
+ 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
+ # If we refer to the make variable ${PREFIX} below, camlp4 ends up having a wrong path:
+ # D:\bin\coq64_buildtest_abs_ocaml4\bin>ocamlc -where => D:/bin/coq64_buildtest_abs_ocaml4/libocaml
+ # D:\bin\coq64_buildtest_abs_ocaml4\bin>camlp4 -where => ${PREFIX}/libocaml\camlp4
+ # So we put an explicit path in there
+ sed -i "s|^LIBDIR=.*|LIBDIR=$PREFIXOCAML/libocaml|" config/Makefile
+
+ # Note: ocaml doesn't support -j 8, so don't pass MAKE_OPT
+ # I verified that 4.02.3 still doesn't support parallel build
+ log2 make world -f Makefile.nt
+ log2 make bootstrap -f Makefile.nt
+ log2 make opt -f Makefile.nt
+ log2 make opt.opt -f Makefile.nt
+ log2 make install -f Makefile.nt
+ # TODO log2 make clean -f Makefile.nt Temporarily disabled for ocamlbuild development
+
+ # Move license files and other into into special folder
+ if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then
+ mkdir -p $PREFIXOCAML/license_readme/ocaml
+ # 4.01 installs these files, 4.02 doesn't. So delete them and copy them from the sources.
+ rm -f *.txt
+ cp LICENSE $PREFIXOCAML/license_readme/ocaml/License.txt
+ cp INSTALL $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
+ fi
+ make_flex_dll_link
+}
+
+##### 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
+ # Note: findlib doesn't support -j 8, so don't pass MAKE_OPT
+ log2 make all
+ log2 make opt
+ log2 make install
+ log2 make clean
+ build_post
+ fi
+}
+
+##### MENHIR Ocaml Parser Generator #####
+
+function make_menhir {
+ make_ocaml
+ make_findlib
+ # if build_prep http://gallium.inria.fr/~fpottier/menhir menhir-20151112 tar.gz 1 ; then
+ # For Ocaml 4.02
+ # if build_prep http://gallium.inria.fr/~fpottier/menhir menhir-20151012 tar.gz 1 ; then
+ # 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
+ build_post
+ 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.02+6 tar.gz 1 camlp4-4.02+6 ; 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 http://camlp5.gforge.inria.fr/distrib/src camlp5-6.14 tgz 1 ; 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
+ 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/
+ 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
+ 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
+
+ # lablgtk shows occasional errors with -j, so don't pass $MAKE_OPT
+
+ # See https://sympa.inria.fr/sympa/arc/caml-list/2015-10/msg00204.html for the make || true + strip
+ logn make-world-pre make world || true
+ $TARGET_ARCH-strip.exe --strip-unneeded src/dlllablgtk2.dll
+
+ log2 make world
+ log2 make install
+ log2 make clean
+ build_post
+ fi
+}
+
+##### Ocaml Stdint #####
+
+function make_stdint {
+ 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
+ build_post
+ fi
+}
+
+##### COQ #####
+
+# Copy one DLLfrom cygwin MINGW packages to Coq install folder
+
+function copy_coq_dll {
+ if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then
+ cp /usr/${ARCH}-w64-mingw32/sys-root/mingw/bin/$1 $PREFIXCOQ/bin/$1
+ fi
+}
+
+# Copy required DLLs from cygwin MINGW packages to Coq install folder
+
+function copy_coq_dlls {
+ # HOW TO CREATE THE DLL LIST
+ # With the list empty, after the build/install is finished, open coqide in dependency walker.
+ # See http://www.dependencywalker.com/
+ # Make sure to use the 32 bit / 64 bit version of depends matching the target architecture.
+ # Select all missing DLLs from the module list, right click "copy filenames"
+ # Delay loaded DLLs from Windows can be ignored (hour-glass icon at begin of line)
+ # Do this recursively until there are no further missing DLLs (File close + reopen)
+ # For running this quickly, just do "cd coq-<ver> ; call 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_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 LIBPANGO-1.0-0.DLL
+ copy_coq_dll LIBPANGOCAIRO-1.0-0.DLL
+ copy_coq_dll LIBPANGOWIN32-1.0-0.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
+
+ # 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
+ 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
+ fi;
+
+ # Architecture dependent files
+ case $ARCH in
+ x86_64) copy_coq_dll LIBGCC_S_SEH-1.DLL ;;
+ i686) copy_coq_dll LIBGCC_S_SJLJ-1.DLL ;;
+ *) false ;;
+ esac
+
+ # Win pthread version change
+ copy_coq_dll LIBWINPTHREAD-1.DLL
+}
+
+function copy_coq_objects {
+ # copy objects only from folders which exist in the target lib directory
+ find . -type d | while read 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
+ fi
+ done
+}
+
+# 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
+
+ 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
+
+ # 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
+ fi
+ mkdir -p $PREFIXCOQ/ide
+ mv $PREFIXCOQ/share/coq/*.png $PREFIXCOQ/ide
+ rmdir $PREFIXCOQ/share/coq
+ fi
+}
+
+# Copy license and other info files
+
+function copy_coq_license {
+ if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then
+ install -D doc/LICENSE $PREFIXCOQ/license_readme/coq/LicenseDoc.txt
+ install -D LICENSE $PREFIXCOQ/license_readme/coq/License.txt
+ install -D plugins/micromega/LICENSE.sos $PREFIXCOQ/license_readme/coq/LicenseMicromega.txt
+ 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
+ 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
+}
+
+# Main function for creating Coq
+
+function make_coq {
+ make_ocaml
+ make_lablgtk
+ make_camlp5
+ 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 ;;
+ 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
+ else
+ logn configure ./configure -debug -with-doc no -prefix $PREFIXCOQ
+ fi
+
+ # The windows resource compiler binary name is hard coded
+ sed -i "s/i686-w64-mingw32-windres/$TARGET_ARCH-windres/" Makefile.build
+ sed -i "s/i686-w64-mingw32-windres/$TARGET_ARCH-windres/" Makefile.ide || true
+
+ # 8.4x doesn't support parallel make
+ if [[ $COQ_VERSION == 8.4* ]] ; then
+ log1 make
+ else
+ log1 make $MAKE_OPT
+ fi
+
+ if [ "$INSTALLMODE" == "relocatable" ]; then
+ ./configure -debug -with-doc no -prefix $PREFIXCOQ -libdir $PREFIXCOQ/lib -mandir $PREFIXCOQ/man
+ fi
+
+ log2 make install
+ log1 copy_coq_dlls
+ if [ "$INSTALLOCAML" == "Y" ]; then
+ log1 copy_coq_objects
+ fi
+
+ copq_coq_gtk
+ copy_coq_license
+
+ # make clean seems to br broken for 8.5pl2
+ # 1.) find | xargs fails on cygwin, can be fixed by sed -i 's|\| xargs rm -f|-exec rm -fv \{\} \+|' Makefile
+ # 2.) clean of test suites fails with "cannot run complexity tests (no bogomips found)"
+ # make clean
+
+ build_post
+ fi
+}
+
+##### GNU Make for MinGW #####
+
+function make_mingw_make {
+ if build_prep http://ftp.gnu.org/gnu/make make-4.2 tar.bz2 ; then
+ # The config.h.win32 file is fine - don't edit it
+ # We need to copy the mingw gcc here as "gcc" - then the batch file will use it
+ cp /usr/bin/${ARCH}-w64-mingw32-gcc-5.4.0.exe ./gcc.exe
+ # By some magic cygwin bash can run batch files
+ logn build ./build_w32.bat gcc
+ # Copy make to Coq folder
+ cp GccRel/gnumake.exe $PREFIXCOQ/bin/make.exe
+ build_post
+ fi
+}
+
+##### GNU binutils for native OCaml #####
+
+function make_binutils {
+ if build_prep http://ftp.gnu.org/gnu/binutils binutils-2.27 tar.gz ; then
+ logn configure ./configure --build=$BUILD --host=$HOST --target=$TARGET --prefix=$PREFIXCOQ --program-prefix=$TARGET-
+ log1 make $MAKE_OPT
+ log2 make install
+ # log2 make clean
+ build_post
+ fi
+}
+
+##### GNU GCC for native OCaml #####
+
+function make_gcc {
+ # Note: the bz2 file is smaller, but decompressing bz2 really takes ages
+ if build_prep ftp://ftp.fu-berlin.de/unix/languages/gcc/releases/gcc-5.4.0 gcc-5.4.0 tar.gz ; then
+ # This is equivalent to "contrib/download_prerequisites" but uses caching
+ # Update versions when updating gcc version
+ get_expand_source_tar ftp://gcc.gnu.org/pub/gcc/infrastructure mpfr-2.4.2 tar.bz2 1 mpfr-2.4.2 mpfr
+ get_expand_source_tar ftp://gcc.gnu.org/pub/gcc/infrastructure gmp-4.3.2 tar.bz2 1 gmp-4.3.2 gmp
+ get_expand_source_tar ftp://gcc.gnu.org/pub/gcc/infrastructure mpc-0.8.1 tar.gz 1 mpc-0.8.1 mpc
+ get_expand_source_tar ftp://gcc.gnu.org/pub/gcc/infrastructure isl-0.14 tar.bz2 1 isl-0.14 isl
+
+ # For whatever reason gcc needs this (although it never puts anything into it)
+ # Error: "The directory that should contain system headers does not exist:"
+ # mkdir -p /mingw/include without --with-sysroot
+ mkdir -p $PREFIXCOQ/mingw/include
+
+ # See https://gcc.gnu.org/install/configure.html
+ logn configure ./configure --build=$BUILD --host=$HOST --target=$TARGET \
+ --prefix=$PREFIXCOQ --program-prefix=$TARGET- --disable-win32-registry --with-sysroot=$PREFIXCOQ \
+ --enable-languages=c --disable-nls \
+ --disable-libsanitizer --disable-libssp --disable-libquadmath --disable-libgomp --disable-libvtv --disable-lto
+ # --disable-decimal-float seems to be required
+ # --with-sysroot=$PREFIX results in configure error that this is not an absolute path
+ log1 make $MAKE_OPT
+ log2 make install
+ # log2 make clean
+ build_post
+ fi
+}
+
+##### Get sources for Cygwin MinGW packages #####
+
+function get_cygwin_mingw_sources {
+ if [ ! -f flagfiles/cygwin_mingw_sources.finished ] ; then
+ touch flagfiles/cygwin_mingw_sources.started
+
+ # Find all installed files with mingw in the name and download the corresponding source code file from cygwin
+ # Steps:
+ # grep /etc/setup/installed.db for mingw => mingw64-x86_64-gcc-g++ mingw64-x86_64-gcc-g++-5.4.0-2.tar.bz2 1
+ # remove archive ending and trailing number => mingw64-x86_64-gcc-g++ mingw64-x86_64-gcc-g++-5.4.0-2
+ # replace space with / => ${ARCHIVE} = mingw64-x86_64-gcc-g++/mingw64-x86_64-gcc-g++-5.4.0-2
+ # escape + signs using ${var//pattern/replace} => ${ARCHIVEESC} = mingw64-x86_64-gcc-g++/mingw64-x86_64-gcc-g\+\+-5.4.0-2
+ # grep cygwin setup.ini for installed line + next line (the -A 1 option includes and "after context" of 1 line)
+ # Note that the folders of the installed binaries and source are different. So we cannot grep just for the source line.
+ # We could strip off the path and just grep for the file, though.
+ # => install: x86_64/release/mingw64-x86_64-gcc/mingw64-x86_64-gcc-g++/mingw64-x86_64-gcc-g++-5.4.0-2.tar.xz 10163848 2f8cb7ba3e16ac8ce0455af01de490ded09061b1b06a9a8e367426635b5a33ce230e04005f059d4ea7b52580757da1f6d5bae88eba6b9da76d1bd95e8844b705
+ # source: x86_64/release/mingw64-x86_64-gcc/mingw64-x86_64-gcc-5.4.0-2-src.tar.xz 95565368 03f22997b7173b243fff65ea46a39613a2e4e75fc7e6cf0fa73b7bcb86071e15ba6d0ca29d330c047fb556a5e684cad57cd2f5adb6e794249e4b01fe27f92c95
+ # Take the 2nd field of the last line => ${SOURCE} = x86_64/release/mingw64-x86_64-gcc/mingw64-x86_64-gcc-5.4.0-2-src.tar.xz
+ # Remove that path part => ${SOURCEFILE} = mingw64-x86_64-gcc-5.4.0-2-src.tar.xz
+
+ grep "mingw" /etc/setup/installed.db | sed 's/\.tar\.bz2 [0-1]$//' | sed 's/ /\//' | while read ARCHIVE ; do
+ local ARCHIVEESC=${ARCHIVE//+/\\+}
+ local SOURCE=`egrep -A 1 "install: ($CYGWINARCH|noarch)/release/[-+_/a-z0-9]*$ARCHIVEESC" $TARBALLS/setup.ini | tail -1 | cut -d " " -f 2`
+ local SOURCEFILE=${SOURCE##*/}
+
+ # Get the source file (either from the source cache or online)
+ if [ ! -f $TARBALLS/$SOURCEFILE ] ; then
+ if [ -f $SOURCE_LOCAL_CACHE_CFMT/$SOURCEFILE ] ; then
+ cp $SOURCE_LOCAL_CACHE_CFMT/$SOURCEFILE $TARBALLS
+ else
+ wget "$CYGWIN_REPOSITORY/$SOURCE"
+ mv $SOURCEFILE $TARBALLS
+ # Save the source archive in the source cache
+ if [ -d $SOURCE_LOCAL_CACHE_CFMT ] ; then
+ cp $TARBALLS/$SOURCEFILE $SOURCE_LOCAL_CACHE_CFMT
+ fi
+ fi
+ fi
+
+ done
+
+ touch flagfiles/cygwin_mingw_sources.finished
+ fi
+}
+
+##### Coq Windows Installer #####
+
+function make_coq_installer {
+ make_coq
+ make_mingw_make
+ 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
+ # ocal_coq: as above + coq
+
+ # Create coq file list as ocaml_coq / ocaml
+ diff_files coq ocaml_coq ocaml
+
+ # Filter out object files
+ filter_files coq_objects coq '\.(cmxa|cmi|cma|cmo|a|o)$'
+
+ # Filter out plugin object files
+ filter_files coq_objects_plugins coq_objects '/lib/plugins/.*\.(cmxa|cmi|cma|cmo|a|o)$'
+
+ # Coq objects objects required for plugin development = coq objects except those for pre installed plugins
+ diff_files coq_plugindev coq_objects coq_objects_plugins
+
+ # Coq files, except objects needed only for plugin development
+ diff_files coq_base coq coq_plugindev
+
+ # Convert section files to NSIS format
+ files_to_nsis coq_base
+ files_to_nsis coq_plugindev
+ files_to_nsis ocaml
+
+ # Get and extract NSIS Binaries
+ if build_prep http://downloads.sourceforge.net/project/nsis/NSIS%202/2.51 nsis-2.51 zip ; then
+ NSIS=`pwd`/makensis.exe
+ chmod u+x "$NSIS"
+ # Change to Coq folder
+ cd ../coq-${COQ_VERSION}
+ # 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`
+ cd dev/nsis
+ logn nsis-installer "$NSIS" -DVERSION=$VERSION -DARCH=$ARCH -DCOQ_SRC_PATH=$PREFIXCOQ -DCOQ_ICON=..\\..\\ide\\coq.ico coq_new.nsi
+
+ build_post
+ fi
+}
+
+###################### TOP LEVEL BUILD #####################
+
+make_gtk2
+make_gtk_sourceview2
+
+make_ocaml
+make_findlib
+make_lablgtk
+make_camlp4
+make_camlp5
+make_menhir
+make_stdint
+list_files ocaml
+make_coq
+
+if [ "$INSTALLMAKE" == "Y" ] ; then
+ make_mingw_make
+fi
+
+list_files ocaml_coq
+
+if [ "$MAKEINSTALLER" == "Y" ] ; then
+ make_coq_installer
+fi
+
diff --git a/dev/build/windows/patches_coq/ReplaceInFile.nsh b/dev/build/windows/patches_coq/ReplaceInFile.nsh
new file mode 100644
index 000000000..27c7eb2fd
--- /dev/null
+++ b/dev/build/windows/patches_coq/ReplaceInFile.nsh
@@ -0,0 +1,67 @@
+; From NSIS Wiki http://nsis.sourceforge.net/ReplaceInFile
+; Modifications:
+; - Replace only once per line
+; - Don't keep original as .old
+; - Use StrRep instead of StrReplace (seems to be cleaner)
+
+Function Func_ReplaceInFile
+ ClearErrors
+
+ Exch $0 ; REPLACEMENT
+ Exch
+ Exch $1 ; SEARCH_TEXT
+ Exch 2
+ Exch $2 ; SOURCE_FILE
+
+ Push $R0 ; SOURCE_FILE file handle
+ Push $R1 ; temporary file handle
+ Push $R2 ; unique temporary file name
+ Push $R3 ; a line to search and replace / save
+ Push $R4 ; shift puffer
+
+ IfFileExists $2 +1 error ; Check if file exists and open it
+ FileOpen $R0 $2 "r"
+
+ GetTempFileName $R2 ; Create temporary output file
+ FileOpen $R1 $R2 "w"
+
+ loop: ; Loop over lines of file
+ FileRead $R0 $R3 ; Read line
+ IfErrors finished
+ Push "$R3" ; Replacine string in line once
+ Push "$1"
+ Push "$0"
+ Call Func_StrRep
+ Pop $R3
+ FileWrite $R1 "$R3" ; Write result
+ Goto loop
+
+ finished:
+ FileClose $R1 ; Close files
+ FileClose $R0
+ Delete "$2" ; Delete original file and rename temporary file to target
+ Rename "$R2" "$2"
+ ClearErrors
+ Goto out
+
+ error:
+ SetErrors
+
+ out:
+ Pop $R4
+ Pop $R3
+ Pop $R2
+ Pop $R1
+ Pop $R0
+ Pop $2
+ Pop $0
+ Pop $1
+FunctionEnd
+
+!macro ReplaceInFile SOURCE_FILE SEARCH_TEXT REPLACEMENT
+ Push "${SOURCE_FILE}"
+ Push "${SEARCH_TEXT}"
+ Push "${REPLACEMENT}"
+ Call Func_ReplaceInFile
+!macroend
+
diff --git a/dev/build/windows/patches_coq/StrRep.nsh b/dev/build/windows/patches_coq/StrRep.nsh
new file mode 100644
index 000000000..d94a9f88b
--- /dev/null
+++ b/dev/build/windows/patches_coq/StrRep.nsh
@@ -0,0 +1,60 @@
+; From NSIS Wiki http://nsis.sourceforge.net/StrRep
+; Slightly modified
+
+Function Func_StrRep
+ Exch $R2 ;new
+ Exch 1
+ Exch $R1 ;old
+ Exch 2
+ Exch $R0 ;string
+ Push $R3
+ Push $R4
+ Push $R5
+ Push $R6
+ Push $R7
+ Push $R8
+ Push $R9
+
+ StrCpy $R3 0
+ StrLen $R4 $R1
+ StrLen $R6 $R0
+ StrLen $R9 $R2
+ loop:
+ StrCpy $R5 $R0 $R4 $R3
+ StrCmp $R5 $R1 found
+ StrCmp $R3 $R6 done
+ IntOp $R3 $R3 + 1 ;move offset by 1 to check the next character
+ Goto loop
+ found:
+ StrCpy $R5 $R0 $R3
+ IntOp $R8 $R3 + $R4
+ StrCpy $R7 $R0 "" $R8
+ StrCpy $R0 $R5$R2$R7
+ StrLen $R6 $R0
+ IntOp $R3 $R3 + $R9 ;move offset by length of the replacement string
+ Goto loop
+ done:
+
+ Pop $R9
+ Pop $R8
+ Pop $R7
+ Pop $R6
+ Pop $R5
+ Pop $R4
+ Pop $R3
+ Push $R0
+ Push $R1
+ Pop $R0
+ Pop $R1
+ Pop $R0
+ Pop $R2
+ Exch $R1
+FunctionEnd
+
+!macro StrRep output string old new
+ Push `${string}`
+ Push `${old}`
+ Push `${new}`
+ Call Func_StrRep
+ Pop ${output}
+!macroend
diff --git a/dev/build/windows/patches_coq/camlp4-4.02+6.patch b/dev/build/windows/patches_coq/camlp4-4.02+6.patch
new file mode 100644
index 000000000..0cdb4a929
--- /dev/null
+++ b/dev/build/windows/patches_coq/camlp4-4.02+6.patch
@@ -0,0 +1,11 @@
+--- 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
new file mode 100644
index 000000000..45a66d0bf
--- /dev/null
+++ b/dev/build/windows/patches_coq/coq-8.4pl2.patch
@@ -0,0 +1,11 @@
+--- 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
new file mode 100644
index 000000000..c3b7f8574
--- /dev/null
+++ b/dev/build/windows/patches_coq/coq-8.4pl6.patch
@@ -0,0 +1,13 @@
+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/coq_new.nsi b/dev/build/windows/patches_coq/coq_new.nsi
new file mode 100644
index 000000000..b88aa066d
--- /dev/null
+++ b/dev/build/windows/patches_coq/coq_new.nsi
@@ -0,0 +1,223 @@
+; This script is used to build the Windows install program for Coq.
+
+; NSIS Modern User Interface
+; Written by Joost Verburg
+; Modified by Julien Narboux, Pierre Letouzey, Enrico Tassi and Michael Soegtrop
+
+; The following command line defines are expected:
+; VERSION Coq version, e.g. 8.5-pl2
+; ARCH The target architecture, either x86_64 or i686
+; COQ_SRC_PATH path of Coq installation in Windows or MinGW format (either \\ or /, but with drive letter)
+; COQ_ICON path of Coq icon file in Windows or MinGW format
+
+; Enable compression after debugging.
+; SetCompress off
+SetCompressor lzma
+
+!define MY_PRODUCT "Coq" ;Define your own software name here
+!define OUTFILE "coq-installer-${VERSION}-${ARCH}.exe"
+
+!include "MUI2.nsh"
+!include "FileAssociation.nsh"
+!include "StrRep.nsh"
+!include "ReplaceInFile.nsh"
+!include "winmessages.nsh"
+
+Var COQ_SRC_PATH_BS ; COQ_SRC_PATH with \ instead of /
+Var COQ_SRC_PATH_DBS ; COQ_SRC_PATH with \\ instead of /
+Var INSTDIR_DBS ; INSTDIR with \\ instead of \
+
+;--------------------------------
+;Configuration
+
+ Name "Coq"
+
+ ;General
+ OutFile "${OUTFILE}"
+
+ ;Folder selection page
+ InstallDir "C:\${MY_PRODUCT}"
+
+ ;Remember install folder
+ InstallDirRegKey HKCU "Software\${MY_PRODUCT}" ""
+
+;--------------------------------
+;Modern UI Configuration
+
+ !define MUI_ICON "${COQ_ICON}"
+
+ !insertmacro MUI_PAGE_WELCOME
+ !insertmacro MUI_PAGE_LICENSE "${COQ_SRC_PATH}/license_readme/coq/License.txt"
+ !insertmacro MUI_PAGE_COMPONENTS
+ !define MUI_DIRECTORYPAGE_TEXT_TOP "Select where to install Coq. The path MUST NOT include spaces."
+ !insertmacro MUI_PAGE_DIRECTORY
+ !insertmacro MUI_PAGE_INSTFILES
+ !insertmacro MUI_PAGE_FINISH
+
+ !insertmacro MUI_UNPAGE_WELCOME
+ !insertmacro MUI_UNPAGE_CONFIRM
+ !insertmacro MUI_UNPAGE_INSTFILES
+ !insertmacro MUI_UNPAGE_FINISH
+
+;--------------------------------
+;Languages
+
+ !insertmacro MUI_LANGUAGE "English"
+
+;--------------------------------
+;Language Strings
+
+ ;Description
+ LangString DESC_1 ${LANG_ENGLISH} "This package contains Coq and CoqIDE."
+ LangString DESC_2 ${LANG_ENGLISH} "This package contains an OCaml compiler for Coq native compute and plugin development."
+ LangString DESC_3 ${LANG_ENGLISH} "This package contains the development files needed in order to build a plugin for Coq."
+ LangString DESC_4 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for the current user."
+ LangString DESC_5 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for all users."
+
+;--------------------------------
+; Check for white spaces
+Function .onVerifyInstDir
+ StrLen $0 "$INSTDIR"
+ StrCpy $1 0
+ ${While} $1 < $0
+ StrCpy $3 $INSTDIR 1 $1
+ StrCmp $3 " " SpacesInPath
+ IntOp $1 $1 + 1
+ ${EndWhile}
+ Goto done
+ SpacesInPath:
+ Abort
+ done:
+FunctionEnd
+
+;--------------------------------
+;Installer Sections
+
+
+Section "Coq" Sec1
+
+ SetOutPath "$INSTDIR\"
+ !include "..\..\..\filelists\coq_base.nsh"
+
+ ${registerExtension} "$INSTDIR\bin\coqide.exe" ".v" "Coq Script File"
+
+ ;Store install folder
+ WriteRegStr HKCU "Software\${MY_PRODUCT}" "" $INSTDIR
+
+ ;Create uninstaller
+ WriteUninstaller "$INSTDIR\Uninstall.exe"
+ WriteRegStr HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
+ "DisplayName" "Coq Version ${VERSION}"
+ WriteRegStr HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
+ "UninstallString" '"$INSTDIR\Uninstall.exe"'
+ WriteRegStr HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
+ "DisplayVersion" "${VERSION}"
+ WriteRegDWORD HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
+ "NoModify" "1"
+ WriteRegDWORD HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
+ "NoRepair" "1"
+ WriteRegStr HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
+ "URLInfoAbout" "http://coq.inria.fr"
+
+ ; Create start menu entries
+ ; SetOutPath is required for the path in the .lnk files
+ SetOutPath "$INSTDIR"
+ CreateDirectory "$SMPROGRAMS\Coq"
+ ; The first shortcut set here is treated as main application by Windows 7/8.
+ ; Use CoqIDE as main application
+ CreateShortCut "$SMPROGRAMS\Coq\CoqIde.lnk" "$INSTDIR\bin\coqide.exe"
+ CreateShortCut "$SMPROGRAMS\Coq\Coq.lnk" "$INSTDIR\bin\coqtop.exe"
+ WriteINIStr "$SMPROGRAMS\Coq\The Coq HomePage.url" "InternetShortcut" "URL" "http://coq.inria.fr"
+ WriteINIStr "$SMPROGRAMS\Coq\The Coq Standard Library.url" "InternetShortcut" "URL" "http://coq.inria.fr/library"
+ CreateShortCut "$SMPROGRAMS\Coq\Uninstall.lnk" "$INSTDIR\Uninstall.exe" "" "$INSTDIR\Uninstall.exe" 0
+
+SectionEnd
+
+;OCAML Section "Ocaml for native compute and plugin development" Sec2
+;OCAML SetOutPath "$INSTDIR\"
+;OCAML !include "..\..\..\filelists\ocaml.nsh"
+;OCAML
+;OCAML ; Create a few slash / backslash variants of the source and install path
+;OCAML ; Note: NSIS has variables, written as $VAR and defines, written as ${VAR}
+;OCAML !insertmacro StrRep $COQ_SRC_PATH_BS ${COQ_SRC_PATH} "/" "\"
+;OCAML !insertmacro StrRep $COQ_SRC_PATH_DBS ${COQ_SRC_PATH} "/" "\\"
+;OCAML !insertmacro StrRep $INSTDIR_DBS $INSTDIR "\" "\\"
+;OCAML
+;OCAML ; Replace absolute paths in some OCaml config files
+;OCAML ; These are not all, see ReadMe.txt
+;OCAML !insertmacro ReplaceInFile "$INSTDIR\libocaml\ld.conf" "/" "\"
+;OCAML !insertmacro ReplaceInFile "$INSTDIR\libocaml\ld.conf" "$COQ_SRC_PATH_BS" "$INSTDIR"
+;OCAML !insertmacro ReplaceInFile "$INSTDIR\etc\findlib.conf" "$COQ_SRC_PATH_DBS" "$INSTDIR_DBS"
+;OCAML SectionEnd
+
+Section "Coq files for plugin developers" Sec3
+ SetOutPath "$INSTDIR\"
+ !include "..\..\..\filelists\coq_plugindev.nsh"
+SectionEnd
+
+;OCAML Section "OCAMLLIB current user" Sec4
+;OCAML WriteRegStr HKCU "Environment" "OCAMLLIB" "$INSTDIR\libocaml"
+;OCAML ; This is required, so that a newly started shell gets the new environment variable
+;OCAML ; But it really takes a few seconds
+;OCAML DetailPrint "Broadcasting OCAMLLIB environment variable change (current user)"
+;OCAML SendMessage ${HWND_BROADCAST} ${WM_WININICHANGE} 0 "STR:Environment" /TIMEOUT=1000
+;OCAML SectionEnd
+
+;OCAML Section "OCAMLLIB all users" Sec5
+;OCAML WriteRegStr HKLM "SYSTEM\CurrentControlSet\Control\Session Manager\Environment" "OCAMLLIB" "$INSTDIR\libocaml"
+;OCAML ; This is required, so that a newly started shell gets the new environment variable
+;OCAML ; But it really takes a few seconds
+;OCAML DetailPrint "Broadcasting OCAMLLIB environment variable change (all users)"
+;OCAML SendMessage ${HWND_BROADCAST} ${WM_WININICHANGE} 0 "STR:Environment" /TIMEOUT=1000
+;OCAML SectionEnd
+
+;--------------------------------
+;Descriptions
+
+!insertmacro MUI_FUNCTION_DESCRIPTION_BEGIN
+ !insertmacro MUI_DESCRIPTION_TEXT ${Sec1} $(DESC_1)
+ ;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec2} $(DESC_2)
+ !insertmacro MUI_DESCRIPTION_TEXT ${Sec3} $(DESC_3)
+ ;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec4} $(DESC_4)
+ ;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec5} $(DESC_5)
+!insertmacro MUI_FUNCTION_DESCRIPTION_END
+
+;--------------------------------
+;Uninstaller Section
+
+Section "Uninstall"
+ ; Files and folders
+ RMDir /r "$INSTDIR\bin"
+ RMDir /r "$INSTDIR\dev"
+ RMDir /r "$INSTDIR\etc"
+ RMDir /r "$INSTDIR\lib"
+ RMDir /r "$INSTDIR\libocaml"
+ RMDir /r "$INSTDIR\share"
+ RMDir /r "$INSTDIR\ide"
+ RMDir /r "$INSTDIR\gtk-2.0"
+ RMDir /r "$INSTDIR\latex"
+ RMDir /r "$INSTDIR\license_readme"
+ RMDir /r "$INSTDIR\man"
+ RMDir /r "$INSTDIR\emacs"
+
+ ; Start Menu
+ Delete "$SMPROGRAMS\Coq\Coq.lnk"
+ Delete "$SMPROGRAMS\Coq\CoqIde.lnk"
+ Delete "$SMPROGRAMS\Coq\Uninstall.lnk"
+ Delete "$SMPROGRAMS\Coq\The Coq HomePage.url"
+ Delete "$SMPROGRAMS\Coq\The Coq Standard Library.url"
+ Delete "$INSTDIR\Uninstall.exe"
+
+ ; Registry keys
+ DeleteRegKey HKCU "Software\${MY_PRODUCT}"
+ DeleteRegKey HKLM "SOFTWARE\Coq"
+ DeleteRegKey HKLM "SOFTWARE\Microsoft\Windows\CurrentVersion\Uninstall\Coq"
+ DeleteRegKey HKCU "Environment\OCAMLLIB"
+ DeleteRegKey HKLM "SYSTEM\CurrentControlSet\Control\Session Manager\Environment\OCAMLLIB"
+ ${unregisterExtension} ".v" "Coq Script File"
+
+ ; Root folders
+ RMDir "$INSTDIR"
+ RMDir "$SMPROGRAMS\Coq"
+
+SectionEnd
diff --git a/dev/build/windows/patches_coq/flexdll-0.34.patch b/dev/build/windows/patches_coq/flexdll-0.34.patch
new file mode 100644
index 000000000..16389baca
--- /dev/null
+++ b/dev/build/windows/patches_coq/flexdll-0.34.patch
@@ -0,0 +1,14 @@
+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/glib-2.46.0.patch b/dev/build/windows/patches_coq/glib-2.46.0.patch
new file mode 100644
index 000000000..9082460bf
--- /dev/null
+++ b/dev/build/windows/patches_coq/glib-2.46.0.patch
@@ -0,0 +1,30 @@
+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
new file mode 100644
index 000000000..73a098d12
--- /dev/null
+++ b/dev/build/windows/patches_coq/gtksourceview-2.11.2.patch
@@ -0,0 +1,213 @@
+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/isl-0.14.patch b/dev/build/windows/patches_coq/isl-0.14.patch
new file mode 100644
index 000000000..f3b8ead1a
--- /dev/null
+++ b/dev/build/windows/patches_coq/isl-0.14.patch
@@ -0,0 +1,11 @@
+--- orig.isl-0.14/configure 2014-10-26 08:36:32.000000000 +0100
++++ isl-0.14/configure 2016-10-10 18:16:01.430224500 +0200
+@@ -8134,7 +8134,7 @@
+ lt_sysroot=`$CC --print-sysroot 2>/dev/null`
+ fi
+ ;; #(
+- /*)
++ /*|[A-Z]:\\*|[A-Z]:/*)
+ lt_sysroot=`echo "$with_sysroot" | sed -e "$sed_quote_subst"`
+ ;; #(
+ no|'')
diff --git a/dev/build/windows/patches_coq/lablgtk-2.18.3.patch b/dev/build/windows/patches_coq/lablgtk-2.18.3.patch
new file mode 100644
index 000000000..0691c1fc8
--- /dev/null
+++ b/dev/build/windows/patches_coq/lablgtk-2.18.3.patch
@@ -0,0 +1,87 @@
+diff -u -r lablgtk-2.18.3/configure lablgtk-2.18.3.patched/configure
+--- lablgtk-2.18.3/configure 2014-10-29 08:51:05.000000000 +0100
++++ lablgtk-2.18.3.patched/configure 2015-10-29 08:58:08.543985500 +0100
+@@ -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
+
+diff -u -r lablgtk-2.18.3/src/glib.mli lablgtk-2.18.3.patched/src/glib.mli
+--- lablgtk-2.18.3/src/glib.mli 2014-10-29 08:51:06.000000000 +0100
++++ lablgtk-2.18.3.patched/src/glib.mli 2016-01-25 09:50:59.884715200 +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
+
+diff -u -r lablgtk-2.18.3/src/glib.ml lablgtk-2.18.3.patched/src/glib.ml
+--- lablgtk-2.18.3/src/glib.ml 2014-10-29 08:51:06.000000000 +0100
++++ lablgtk-2.18.3.patched/src/glib.ml 2016-01-25 09:50:59.891715900 +0100
+@@ -72,6 +72,8 @@
+ type id
+ external channel_of_descr : Unix.file_descr -> channel
+ = "ml_g_io_channel_unix_new"
++ external channel_of_descr_socket : Unix.file_descr -> channel
++ = "ml_g_io_channel_unix_new_socket"
+ external remove : id -> unit = "ml_g_source_remove"
+ external add_watch :
+ cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id
+
+diff -u -r lablgtk-2.18.3/src/ml_glib.c lablgtk-2.18.3.patched/src/ml_glib.c
+--- lablgtk-2.18.3/src/ml_glib.c 2014-10-29 08:51:06.000000000 +0100
++++ lablgtk-2.18.3.patched/src/ml_glib.c 2016-01-25 09:50:59.898716600 +0100
+@@ -25,6 +25,8 @@
+ #include <string.h>
+ #include <locale.h>
+ #ifdef _WIN32
++/* to kill a #warning: include winsock2.h before windows.h */
++#include <winsock2.h>
+ #include "win32.h"
+ #include <wtypes.h>
+ #include <io.h>
+@@ -38,6 +40,11 @@
+ #include <caml/callback.h>
+ #include <caml/threads.h>
+
++#ifdef _WIN32
++/* for Socket_val */
++#include <caml/unixsupport.h>
++#endif
++
+ #include "wrappers.h"
+ #include "ml_glib.h"
+ #include "glib_tags.h"
+@@ -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/ln.c b/dev/build/windows/patches_coq/ln.c
new file mode 100644
index 000000000..5e02c72bb
--- /dev/null
+++ b/dev/build/windows/patches_coq/ln.c
@@ -0,0 +1,137 @@
+// (C) 2016 Intel Deutschland GmbH
+// Author: Michael Soegtrop
+// Released to the public under CC0
+// See https://creativecommons.org/publicdomain/zero/1.0/
+
+// Windows drop in repacement for Linux ln
+// Supports command form "ln TARGET LINK_NAME"
+// Supports -s and -f options
+// Does not support hard links to folders (but symlinks are ok)
+
+#include <windows.h>
+#include <stdio.h>
+#include <tchar.h>
+
+// Cygwin MinGW doesn't have this Vista++ function in windows.h
+#ifdef UNICODE
+ WINBASEAPI BOOLEAN APIENTRY CreateSymbolicLinkW ( LPCWSTR, LPCWSTR, DWORD );
+ #define CreateSymbolicLink CreateSymbolicLinkW
+ #define CommandLineToArgv CommandLineToArgvW
+#else
+ WINBASEAPI BOOLEAN APIENTRY CreateSymbolicLinkA ( LPCSTR, LPCSTR, DWORD );
+ #define CreateSymbolicLink CreateSymbolicLinkA
+ #define CommandLineToArgv CommandLineToArgvA
+#endif
+#define SYMBOLIC_LINK_FLAG_DIRECTORY 1
+
+int WINAPI WinMain( HINSTANCE hInstance, HINSTANCE hPrevInstance, LPSTR lpCmdLineA, int nShowCmd )
+{
+ int iarg;
+ BOOL symbolic = FALSE;
+ BOOL force = FALSE;
+ BOOL folder;
+ const _TCHAR *target;
+ const _TCHAR *link;
+ LPTSTR lpCmdLine;
+ int argc;
+ LPTSTR *argv;
+
+ // Parse command line
+ // This is done explicitly here for two reasons
+ // 1.) MinGW doesn't seem to support _tmain, wWinMain and the like
+ // 2.) We want to make sure that CommandLineToArgv is used
+ lpCmdLine = GetCommandLine();
+ argv = CommandLineToArgv( lpCmdLine, &argc );
+
+ // Get target and link name
+ if( argc<3 )
+ {
+ _ftprintf( stderr, _T("Expecting at least 2 arguments, got %d\n"), argc-1 );
+ return 1;
+ }
+ target = argv[argc-2];
+ link = argv[argc-1];
+
+ // Parse options
+ // The last two arguments are interpreted as file names
+ // All other arguments must be -s or -f os multi letter options like -sf
+ for(iarg=1; iarg<argc-2; iarg++ )
+ {
+ const _TCHAR *pos = argv[iarg];
+ if( *pos != _T('-') )
+ {
+ _ftprintf( stderr, _T("Command line option expected in argument %d\n"), iarg );
+ return 1;
+ }
+ pos ++;
+
+ while( *pos )
+ {
+ switch( *pos )
+ {
+ case _T('s') : symbolic = TRUE; break;
+ case _T('f') : force = TRUE; break;
+ default :
+ _ftprintf( stderr, _T("Unknown option '%c'\n"), *pos );
+ return 1;
+ }
+ pos ++;
+ }
+ }
+
+ #ifdef IGNORE_SYMBOLIC
+ symbolic = FALSE;
+ #endif
+
+ // Check if link already exists - delete it if force is given or abort
+ {
+ if( GetFileAttributes(link) != INVALID_FILE_ATTRIBUTES )
+ {
+ if( force )
+ {
+ if( !DeleteFile( link ) )
+ {
+ _ftprintf( stderr, _T("Error deleting file '%s'\n"), link );
+ return 1;
+ }
+ }
+ else
+ {
+ _ftprintf( stderr, _T("File '%s' exists!\n"), link );
+ return 1;
+ }
+ }
+ }
+
+ // Check if target is a folder
+ folder = ( (GetFileAttributes(target) & FILE_ATTRIBUTE_DIRECTORY) ) != 0;
+
+ // Create link
+ if(symbolic)
+ {
+ if( !CreateSymbolicLink( link, target, folder ? SYMBOLIC_LINK_FLAG_DIRECTORY : 0 ) )
+ {
+ _ftprintf( stderr, _T("Error creating symbolic link '%s' -> '%s'!\n"), link, target );
+ return 1;
+ }
+ }
+ else
+ {
+ if( folder )
+ {
+ _ftprintf( stderr, _T("Cannot create hard link to folder") );
+ return 1;
+ }
+ else
+ {
+ if( !CreateHardLink( link, target, NULL ) )
+ {
+ _ftprintf( stderr, _T("Error creating hard link '%s' -> '%s'!\n"), link, target );
+ return 1;
+ }
+ }
+ }
+
+ // Everything is fine
+ return 0;
+} \ No newline at end of file