aboutsummaryrefslogtreecommitdiff
path: root/dev/build
diff options
context:
space:
mode:
Diffstat (limited to 'dev/build')
-rwxr-xr-xdev/build/windows/MakeCoq_MinGW.bat976
-rwxr-xr-xdev/build/windows/makecoq_mingw.sh492
-rw-r--r--dev/build/windows/patches_coq/coq_new.nsi188
-rwxr-xr-xdev/build/windows/patches_coq/quickchick.patch26
4 files changed, 1097 insertions, 585 deletions
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
index 61cf6bc4cc..33feeed45c 100755
--- a/dev/build/windows/MakeCoq_MinGW.bat
+++ b/dev/build/windows/MakeCoq_MinGW.bat
@@ -1,488 +1,488 @@
-@ECHO OFF
-
-REM ========== COPYRIGHT/COPYLEFT ==========
-
-REM (C) 2016 Intel Deutschland GmbH
-REM Author: Michael Soegtrop
-
-REM Released to the public by Intel under the
-REM GNU Lesser General Public License Version 2.1 or later
-REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
-
-REM ========== NOTES ==========
-
-REM For Cygwin setup command line options
-REM see https://cygwin.com/faq/faq.html#faq.setup.cli
-
-REM ========== DEFAULT VALUES FOR PARAMETERS ==========
-
-REM For a description of all parameters, see ReadMe.txt
-
-SET BATCHFILE=%~0
-SET BATCHDIR=%~dp0
-
-REM see -arch in ReadMe.txt, but values are x86_64 or i686 (not 64 or 32)
-SET ARCH=x86_64
-
-REM see -mode in ReadMe.txt
-SET INSTALLMODE=absolute
-
-REM see -installer in ReadMe.txt
-SET MAKEINSTALLER=N
-
-REM see -ocaml in ReadMe.txt
-SET INSTALLOCAML=N
-
-REM see -make in ReadMe.txt
-SET INSTALLMAKE=N
-
-REM see -destcyg in ReadMe.txt
-SET DESTCYG=C:\bin\cygwin_coq
-
-REM see -destcoq in ReadMe.txt
-SET DESTCOQ=C:\bin\coq
-
-REM see -setup in ReadMe.txt
-SET SETUP=setup-x86_64.exe
-
-REM see -proxy in ReadMe.txt
-IF DEFINED HTTP_PROXY (
- SET PROXY=%HTTP_PROXY:http://=%
-) else (
- REM One can't set a variable to empty in DOS, but you can set it to a space this way.
- REM The quotes are just there to make the space visible and to protect from "remove trailing spaces".
- SET "PROXY= "
-)
-
-REM see -cygrepo in ReadMe.txt
-SET CYGWIN_REPOSITORY=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 see -addon in ReadMe.txt
-SET "COQ_ADDONS= "
-
-REM ========== PARSE COMMAND LINE PARAMETERS ==========
-
-SHIFT
-
-:Parse
-
-IF "%~0" == "-arch" (
- IF "%~1" == "32" (
- SET ARCH=i686
- SET SETUP=setup-x86.exe
- ) ELSE (
- IF "%~1" == "64" (
- SET ARCH=x86_64
- SET SETUP=setup-x86_64.exe
- ) ELSE (
- ECHO "Invalid -arch, valid are 32 and 64"
- GOTO :EOF
- )
- )
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-mode" (
- IF "%~1" == "mingwincygwin" (
- SET INSTALLMODE=%~1
- ) ELSE (
- IF "%~1" == "absolute" (
- SET INSTALLMODE=%~1
- ) ELSE (
- IF "%~1" == "relocatable" (
- SET INSTALLMODE=%~1
- ) ELSE (
- ECHO "Invalid -mode, valid are mingwincygwin, absolute and relocatable"
- GOTO :EOF
- )
- )
- )
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-installer" (
- SET MAKEINSTALLER=%~1
- CALL :CheckYN -installer %~1 || GOTO ErrorExit
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-ocaml" (
- SET INSTALLOCAML=%~1
- CALL :CheckYN -installer %~1 || GOTO ErrorExit
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-make" (
- SET INSTALLMAKE=%~1
- CALL :CheckYN -installer %~1 || GOTO ErrorExit
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-destcyg" (
- SET DESTCYG=%~1
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-destcoq" (
- SET DESTCOQ=%~1
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-setup" (
- SET SETUP=%~1
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-proxy" (
- SET PROXY=%~1
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-cygrepo" (
- SET CYGWIN_REPOSITORY=%~1
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-cygcache" (
- SET CYGWIN_LOCAL_CACHE_WFMT=%~1
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-cyglocal" (
- SET CYGWIN_FROM_CACHE=%~1
- CALL :CheckYN -cyglocal %~1 || GOTO ErrorExit
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-cygquiet" (
- SET CYGWIN_QUIET=%~1
- CALL :CheckYN -cygquiet %~1 || GOTO ErrorExit
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-srccache" (
- SET SOURCE_LOCAL_CACHE_WFMT=%~1
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-coqver" (
- SET COQ_VERSION=%~1
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-gtksrc" (
- SET GTK_FROM_SOURCES=%~1
- CALL :CheckYN -gtksrc %~1 || GOTO ErrorExit
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-threads" (
- SET MAKE_THREADS=%~1
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-IF "%~0" == "-addon" (
- SET "COQ_ADDONS=%COQ_ADDONS% %~1"
- SHIFT
- SHIFT
- GOTO Parse
-)
-
-
-IF NOT "%~0" == "" (
- ECHO Install cygwin and download, compile and install OCaml and Coq for MinGW
- ECHO !!! Illegal parameter %~0
- ECHO Usage:
- ECHO MakeCoq_MinGW
- CALL :PrintPars
- GOTO :EOF
-)
-
-IF NOT EXIST %SETUP% (
- ECHO The cygwin setup program %SETUP% doesn't exist. You must download it from https://cygwin.com/install.html.
- ECHO If the setup is in a different folder, set the full path to %SETUP% using the -setup option.
- GOTO :EOF
-)
-
-REM ========== ADJUST PARAMETERS ==========
-
-IF "%INSTALLMODE%" == "mingwincygwin" (
- SET DESTCOQ=%DESTCYG%\usr\%ARCH%-w64-mingw32\sys-root\mingw
-)
-
-IF "%MAKEINSTALLER%" == "Y" (
- SET INSTALLMODE=relocatable
-)
-
-REM ========== CONFIRM PARAMETERS ==========
-
-CALL :PrintPars
-REM Note: DOS batch replaces variables on parsing, so one can't use a variable just set in an () block
-IF "%COQREGTESTING%"=="Y" (GOTO DontAsk)
- SET /p ANSWER="Is this correct? y/n "
- IF NOT "%ANSWER%"=="y" (GOTO :EOF)
-:DontAsk
-
-REM ========== DERIVED VARIABLES ==========
-
-SET CYGWIN_INSTALLDIR_WFMT=%DESTCYG%
-SET RESULT_INSTALLDIR_WFMT=%DESTCOQ%
-SET TARGET_ARCH=%ARCH%-w64-mingw32
-SET BASH=%CYGWIN_INSTALLDIR_WFMT%\bin\bash
-
-REM Convert 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 One can't set a variable to empty in DOS, but you can set it to a space this way.
-REM The quotes are just there to make the space visible and to protect from "remove trailing spaces".
-SET "CYGWIN_OPT= "
-
-IF "%CYGWIN_FROM_CACHE%" == "Y" (
- SET CYGWIN_OPT= %CYGWIN_OPT% -L
-)
-
-IF "%CYGWIN_QUIET%" == "Y" (
- SET CYGWIN_OPT= %CYGWIN_OPT% -q --no-admin
-)
-
-IF "%GTK_FROM_SOURCES%"=="N" (
- SET CYGWIN_OPT= %CYGWIN_OPT% -P mingw64-%ARCH%-gtk2.0,mingw64-%ARCH%-gtksourceview2.0
-)
-
-REM Cygwin setup sets proper ACLs (permissions) for folders it CREATES.
-REM Otherwise chmod won't work and e.g. the ocaml build will fail.
-REM Cygwin setup does not touch the ACLs of existing folders.
-
-REM Run Cygwin Setup
-
-SET RUNSETUP=Y
-IF EXIST "%CYGWIN_INSTALLDIR_WFMT%\etc\setup\installed.db" (
- SET RUNSETUP=N
-)
-IF NOT "%CYGWIN_QUIET%" == "Y" (
- SET RUNSETUP=Y
-)
-
-IF "%COQREGTESTING%" == "Y" (
- ECHO "========== REMOVE EXISTING CYGWIN =========="
- DEL /S /F /Q "%CYGWIN_INSTALLDIR_WFMT%" > NUL
- SET RUNSETUP=Y
-)
-
-SET "EXTRAPACKAGES= "
-
-IF NOT "%APPVEYOR%" == "True" (
- SET EXTRAPACKAGES=-P wget,curl,git,gcc-core,gcc-g++,automake1.5
-)
-
-ECHO "========== INSTALL CYGWIN =========="
-
-IF "%RUNSETUP%"=="Y" (
- %SETUP% ^
- --proxy "%PROXY%" ^
- --site "%CYGWIN_REPOSITORY%" ^
- --root "%CYGWIN_INSTALLDIR_WFMT%" ^
- --local-package-dir "%CYGWIN_LOCAL_CACHE_WFMT%" ^
- --no-shortcuts ^
- %CYGWIN_OPT% ^
- -P make,unzip ^
- -P gdb,liblzma5 ^
- -P patch,automake1.14 ^
- -P 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 ^
- %EXTRAPACKAGES% ^
- || GOTO ErrorExit
-
- MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build"
- MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\buildlogs"
-)
-
-IF NOT "%CYGWIN_QUIET%" == "Y" (
- REM Like most setup programs, cygwin setup starts the real setup as a separate process, so wait for it.
- REM This is not required with the -cygquiet=Y and the resulting --no-admin option.
- :waitsetup
- tasklist /fi "imagename eq %SETUP%" | find ":" > NUL
- IF ERRORLEVEL 1 GOTO waitsetup
-)
-
-ECHO ========== CONFIGURE CYGWIN USER ACCOUNT ==========
-
-REM In case this batch file is called from a cygwin bash (e.g. a git repo) we need to clear
-REM HOME (otherwise we get to the home directory of the other installation)
-REM PROFILEREAD (this is set to true if the /etc/profile has been read, which creates user)
-SET "HOME="
-SET "PROFILEREAD="
-
-copy "%BATCHDIR%\configure_profile.sh" "%CYGWIN_INSTALLDIR_WFMT%\var\tmp" || GOTO ErrorExit
-%BASH% --login "%CYGWIN_INSTALLDIR_CFMT%\var\tmp\configure_profile.sh" "%PROXY%" || GOTO ErrorExit
-
-ECHO ========== BUILD COQ ==========
-
-MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build"
-MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\patches"
-
-COPY "%BATCHDIR%\makecoq_mingw.sh" "%CYGWIN_INSTALLDIR_WFMT%\build" || GOTO ErrorExit
-COPY "%BATCHDIR%\patches_coq\*.*" "%CYGWIN_INSTALLDIR_WFMT%\build\patches" || GOTO ErrorExit
-
-%BASH% --login "%CYGWIN_INSTALLDIR_CFMT%\build\makecoq_mingw.sh" || GOTO ErrorExit
-
-ECHO ========== FINISHED ==========
-
-GOTO :EOF
-
-ECHO ========== BATCH FUNCTIONS ==========
-
-:PrintPars
- REM 01234567890123456789012345678901234567890123456789012345678901234567890123456789
- ECHO -arch ^<i686 or x86_64^> Set cygwin, ocaml and coq to 32 or 64 bit
- ECHO -mode ^<mingwincygwin = install coq in default cygwin mingw sysroot^>
- ECHO ^<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 -addon ^<name^> Enable building selected addon (can be repeated)
- ECHO(
- ECHO See ReadMe.txt for a detailed description of all parameters
- ECHO(
- ECHO Parameter values (default or currently set):
- ECHO -arch = %ARCH%
- ECHO -mode = %INSTALLMODE%
- ECHO -ocaml = %INSTALLOCAML%
- ECHO -installer= %MAKEINSTALLER%
- ECHO -make = %INSTALLMAKE%
- ECHO -destcyg = %DESTCYG%
- ECHO -destcoq = %DESTCOQ%
- ECHO -setup = %SETUP%
- ECHO -proxy = %PROXY%
- ECHO -cygrepo = %CYGWIN_REPOSITORY%
- ECHO -cygcache = %CYGWIN_LOCAL_CACHE_WFMT%
- ECHO -cyglocal = %CYGWIN_FROM_CACHE%
- ECHO -cygquiet = %CYGWIN_QUIET%
- ECHO -srccache = %SOURCE_LOCAL_CACHE_WFMT%
- ECHO -coqver = %COQ_VERSION%
- ECHO -gtksrc = %GTK_FROM_SOURCES%
- ECHO -threads = %MAKE_THREADS%
- ECHO -addon = %COQ_ADDONS%
- GOTO :EOF
-
-:CheckYN
- REM Reset errorlevel to 0
- CMD /c "EXIT /b 0"
- IF "%2" == "Y" (
- REM OK Y
- ) ELSE IF "%2" == "N" (
- REM OK N
- ) ELSE (
- ECHO ERROR Parameter %1 must be Y or N, but is %2
- GOTO ErrorExit
- )
- GOTO :EOF
-
-:ErrorExit
- ECHO ERROR MakeCoq_MinGW.bat failed
- EXIT /b 1
+@ECHO OFF
+
+REM ========== COPYRIGHT/COPYLEFT ==========
+
+REM (C) 2016 Intel Deutschland GmbH
+REM Author: Michael Soegtrop
+
+REM Released to the public by Intel under the
+REM GNU Lesser General Public License Version 2.1 or later
+REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
+
+REM ========== NOTES ==========
+
+REM For Cygwin setup command line options
+REM see https://cygwin.com/faq/faq.html#faq.setup.cli
+
+REM ========== DEFAULT VALUES FOR PARAMETERS ==========
+
+REM For a description of all parameters, see ReadMe.txt
+
+SET BATCHFILE=%~0
+SET BATCHDIR=%~dp0
+
+REM see -arch in ReadMe.txt, but values are x86_64 or i686 (not 64 or 32)
+SET ARCH=x86_64
+
+REM see -mode in ReadMe.txt
+SET INSTALLMODE=absolute
+
+REM see -installer in ReadMe.txt
+SET MAKEINSTALLER=N
+
+REM see -ocaml in ReadMe.txt
+SET INSTALLOCAML=N
+
+REM see -make in ReadMe.txt
+SET INSTALLMAKE=N
+
+REM see -destcyg in ReadMe.txt
+SET DESTCYG=C:\bin\cygwin_coq
+
+REM see -destcoq in ReadMe.txt
+SET DESTCOQ=C:\bin\coq
+
+REM see -setup in ReadMe.txt
+SET SETUP=setup-x86_64.exe
+
+REM see -proxy in ReadMe.txt
+IF DEFINED HTTP_PROXY (
+ SET PROXY=%HTTP_PROXY:http://=%
+) else (
+ REM One can't set a variable to empty in DOS, but you can set it to a space this way.
+ REM The quotes are just there to make the space visible and to protect from "remove trailing spaces".
+ SET "PROXY= "
+)
+
+REM see -cygrepo in ReadMe.txt
+SET CYGWIN_REPOSITORY=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 see -addon in ReadMe.txt
+SET "COQ_ADDONS= "
+
+REM ========== PARSE COMMAND LINE PARAMETERS ==========
+
+SHIFT
+
+:Parse
+
+IF "%~0" == "-arch" (
+ IF "%~1" == "32" (
+ SET ARCH=i686
+ SET SETUP=setup-x86.exe
+ ) ELSE (
+ IF "%~1" == "64" (
+ SET ARCH=x86_64
+ SET SETUP=setup-x86_64.exe
+ ) ELSE (
+ ECHO "Invalid -arch, valid are 32 and 64"
+ GOTO :EOF
+ )
+ )
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-mode" (
+ IF "%~1" == "mingwincygwin" (
+ SET INSTALLMODE=%~1
+ ) ELSE (
+ IF "%~1" == "absolute" (
+ SET INSTALLMODE=%~1
+ ) ELSE (
+ IF "%~1" == "relocatable" (
+ SET INSTALLMODE=%~1
+ ) ELSE (
+ ECHO "Invalid -mode, valid are mingwincygwin, absolute and relocatable"
+ GOTO :EOF
+ )
+ )
+ )
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-installer" (
+ SET MAKEINSTALLER=%~1
+ CALL :CheckYN -installer %~1 || GOTO ErrorExit
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-ocaml" (
+ SET INSTALLOCAML=%~1
+ CALL :CheckYN -installer %~1 || GOTO ErrorExit
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-make" (
+ SET INSTALLMAKE=%~1
+ CALL :CheckYN -installer %~1 || GOTO ErrorExit
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-destcyg" (
+ SET DESTCYG=%~1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-destcoq" (
+ SET DESTCOQ=%~1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-setup" (
+ SET SETUP=%~1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-proxy" (
+ SET PROXY=%~1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-cygrepo" (
+ SET CYGWIN_REPOSITORY=%~1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-cygcache" (
+ SET CYGWIN_LOCAL_CACHE_WFMT=%~1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-cyglocal" (
+ SET CYGWIN_FROM_CACHE=%~1
+ CALL :CheckYN -cyglocal %~1 || GOTO ErrorExit
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-cygquiet" (
+ SET CYGWIN_QUIET=%~1
+ CALL :CheckYN -cygquiet %~1 || GOTO ErrorExit
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-srccache" (
+ SET SOURCE_LOCAL_CACHE_WFMT=%~1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-coqver" (
+ SET COQ_VERSION=%~1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-gtksrc" (
+ SET GTK_FROM_SOURCES=%~1
+ CALL :CheckYN -gtksrc %~1 || GOTO ErrorExit
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-threads" (
+ SET MAKE_THREADS=%~1
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+IF "%~0" == "-addon" (
+ SET "COQ_ADDONS=%COQ_ADDONS% %~1"
+ SHIFT
+ SHIFT
+ GOTO Parse
+)
+
+
+IF NOT "%~0" == "" (
+ ECHO Install cygwin and download, compile and install OCaml and Coq for MinGW
+ ECHO !!! Illegal parameter %~0
+ ECHO Usage:
+ ECHO MakeCoq_MinGW
+ CALL :PrintPars
+ GOTO :EOF
+)
+
+IF NOT EXIST %SETUP% (
+ ECHO The cygwin setup program %SETUP% doesn't exist. You must download it from https://cygwin.com/install.html.
+ ECHO If the setup is in a different folder, set the full path to %SETUP% using the -setup option.
+ GOTO :EOF
+)
+
+REM ========== ADJUST PARAMETERS ==========
+
+IF "%INSTALLMODE%" == "mingwincygwin" (
+ SET DESTCOQ=%DESTCYG%\usr\%ARCH%-w64-mingw32\sys-root\mingw
+)
+
+IF "%MAKEINSTALLER%" == "Y" (
+ SET INSTALLMODE=relocatable
+)
+
+REM ========== CONFIRM PARAMETERS ==========
+
+CALL :PrintPars
+REM Note: DOS batch replaces variables on parsing, so one can't use a variable just set in an () block
+IF "%COQREGTESTING%"=="Y" (GOTO DontAsk)
+ SET /p ANSWER="Is this correct? y/n "
+ IF NOT "%ANSWER%"=="y" (GOTO :EOF)
+:DontAsk
+
+REM ========== DERIVED VARIABLES ==========
+
+SET CYGWIN_INSTALLDIR_WFMT=%DESTCYG%
+SET RESULT_INSTALLDIR_WFMT=%DESTCOQ%
+SET TARGET_ARCH=%ARCH%-w64-mingw32
+SET BASH=%CYGWIN_INSTALLDIR_WFMT%\bin\bash
+
+REM Convert 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 One can't set a variable to empty in DOS, but you can set it to a space this way.
+REM The quotes are just there to make the space visible and to protect from "remove trailing spaces".
+SET "CYGWIN_OPT= "
+
+IF "%CYGWIN_FROM_CACHE%" == "Y" (
+ SET CYGWIN_OPT= %CYGWIN_OPT% -L
+)
+
+IF "%CYGWIN_QUIET%" == "Y" (
+ SET CYGWIN_OPT= %CYGWIN_OPT% -q --no-admin
+)
+
+IF "%GTK_FROM_SOURCES%"=="N" (
+ SET CYGWIN_OPT= %CYGWIN_OPT% -P mingw64-%ARCH%-gtk2.0,mingw64-%ARCH%-gtksourceview2.0
+)
+
+REM Cygwin setup sets proper ACLs (permissions) for folders it CREATES.
+REM Otherwise chmod won't work and e.g. the ocaml build will fail.
+REM Cygwin setup does not touch the ACLs of existing folders.
+
+REM Run Cygwin Setup
+
+SET RUNSETUP=Y
+IF EXIST "%CYGWIN_INSTALLDIR_WFMT%\etc\setup\installed.db" (
+ SET RUNSETUP=N
+)
+IF NOT "%CYGWIN_QUIET%" == "Y" (
+ SET RUNSETUP=Y
+)
+
+IF "%COQREGTESTING%" == "Y" (
+ ECHO "========== REMOVE EXISTING CYGWIN =========="
+ DEL /S /F /Q "%CYGWIN_INSTALLDIR_WFMT%" > NUL
+ SET RUNSETUP=Y
+)
+
+SET "EXTRAPACKAGES= "
+
+IF NOT "%APPVEYOR%" == "True" (
+ SET EXTRAPACKAGES=-P wget,curl,git,gcc-core,gcc-g++,automake1.5
+)
+
+ECHO "========== INSTALL CYGWIN =========="
+
+IF "%RUNSETUP%"=="Y" (
+ %SETUP% ^
+ --proxy "%PROXY%" ^
+ --site "%CYGWIN_REPOSITORY%" ^
+ --root "%CYGWIN_INSTALLDIR_WFMT%" ^
+ --local-package-dir "%CYGWIN_LOCAL_CACHE_WFMT%" ^
+ --no-shortcuts ^
+ %CYGWIN_OPT% ^
+ -P make,unzip ^
+ -P gdb,liblzma5 ^
+ -P patch,automake1.14 ^
+ -P 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 ^
+ %EXTRAPACKAGES% ^
+ || GOTO ErrorExit
+
+ MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build"
+ MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\buildlogs"
+)
+
+IF NOT "%CYGWIN_QUIET%" == "Y" (
+ REM Like most setup programs, cygwin setup starts the real setup as a separate process, so wait for it.
+ REM This is not required with the -cygquiet=Y and the resulting --no-admin option.
+ :waitsetup
+ tasklist /fi "imagename eq %SETUP%" | find ":" > NUL
+ IF ERRORLEVEL 1 GOTO waitsetup
+)
+
+ECHO ========== CONFIGURE CYGWIN USER ACCOUNT ==========
+
+REM In case this batch file is called from a cygwin bash (e.g. a git repo) we need to clear
+REM HOME (otherwise we get to the home directory of the other installation)
+REM PROFILEREAD (this is set to true if the /etc/profile has been read, which creates user)
+SET "HOME="
+SET "PROFILEREAD="
+
+copy "%BATCHDIR%\configure_profile.sh" "%CYGWIN_INSTALLDIR_WFMT%\var\tmp" || GOTO ErrorExit
+%BASH% --login "%CYGWIN_INSTALLDIR_CFMT%\var\tmp\configure_profile.sh" "%PROXY%" || GOTO ErrorExit
+
+ECHO ========== BUILD COQ ==========
+
+MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build"
+MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\patches"
+
+COPY "%BATCHDIR%\makecoq_mingw.sh" "%CYGWIN_INSTALLDIR_WFMT%\build" || GOTO ErrorExit
+COPY "%BATCHDIR%\patches_coq\*.*" "%CYGWIN_INSTALLDIR_WFMT%\build\patches" || GOTO ErrorExit
+
+%BASH% --login "%CYGWIN_INSTALLDIR_CFMT%\build\makecoq_mingw.sh" || GOTO ErrorExit
+
+ECHO ========== FINISHED ==========
+
+GOTO :EOF
+
+ECHO ========== BATCH FUNCTIONS ==========
+
+:PrintPars
+ REM 01234567890123456789012345678901234567890123456789012345678901234567890123456789
+ ECHO -arch ^<i686 or x86_64^> Set cygwin, ocaml and coq to 32 or 64 bit
+ ECHO -mode ^<mingwincygwin = install coq in default cygwin mingw sysroot^>
+ ECHO ^<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 -addon ^<name^> Enable building selected addon (can be repeated)
+ ECHO(
+ ECHO See ReadMe.txt for a detailed description of all parameters
+ ECHO(
+ ECHO Parameter values (default or currently set):
+ ECHO -arch = %ARCH%
+ ECHO -mode = %INSTALLMODE%
+ ECHO -ocaml = %INSTALLOCAML%
+ ECHO -installer= %MAKEINSTALLER%
+ ECHO -make = %INSTALLMAKE%
+ ECHO -destcyg = %DESTCYG%
+ ECHO -destcoq = %DESTCOQ%
+ ECHO -setup = %SETUP%
+ ECHO -proxy = %PROXY%
+ ECHO -cygrepo = %CYGWIN_REPOSITORY%
+ ECHO -cygcache = %CYGWIN_LOCAL_CACHE_WFMT%
+ ECHO -cyglocal = %CYGWIN_FROM_CACHE%
+ ECHO -cygquiet = %CYGWIN_QUIET%
+ ECHO -srccache = %SOURCE_LOCAL_CACHE_WFMT%
+ ECHO -coqver = %COQ_VERSION%
+ ECHO -gtksrc = %GTK_FROM_SOURCES%
+ ECHO -threads = %MAKE_THREADS%
+ ECHO -addon = %COQ_ADDONS%
+ GOTO :EOF
+
+:CheckYN
+ REM Reset errorlevel to 0
+ CMD /c "EXIT /b 0"
+ IF "%2" == "Y" (
+ REM OK Y
+ ) ELSE IF "%2" == "N" (
+ REM OK N
+ ) ELSE (
+ ECHO ERROR Parameter %1 must be Y or N, but is %2
+ GOTO ErrorExit
+ )
+ GOTO :EOF
+
+:ErrorExit
+ ECHO ERROR MakeCoq_MinGW.bat failed
+ EXIT /b 1
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 23eb6fbc63..c3d895784e 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -2,7 +2,7 @@
###################### COPYRIGHT/COPYLEFT ######################
-# (C) 2016 Intel Deutschland GmbH
+# (C) 2016..2018 Intel Deutschland GmbH
# Author: Michael Soegtrop
#
# Released to the public by Intel under the
@@ -159,19 +159,19 @@ if [ "${COQREGTESTING:-N}" == "Y" ] ; then
# Log command output - take log target name from command name (like log1 make => log target is "<module>-make")
log1() {
{ local -; set +x; } 2> /dev/null
- "$@" >"$LOGS/$LOGTARGET-$1.log" 2>"$LOGS/$LOGTARGET-$1.err"
+ "$@" >"$LOGS/$LOGTARGET-$1_log.txt" 2>"$LOGS/$LOGTARGET-$1_err.txt"
}
# Log command output - take log target name from command name and first argument (like log2 make install => log target is "<module>-make-install")
log2() {
{ local -; set +x; } 2> /dev/null
- "$@" >"$LOGS/$LOGTARGET-$1-$2.log" 2>"$LOGS/$LOGTARGET-$1-$2.err"
+ "$@" >"$LOGS/$LOGTARGET-$1-$2_log.txt" 2>"$LOGS/$LOGTARGET-$1-$2_err.txt"
}
# Log command output - take log target name from command name and second argument (like log_1_3 ocaml setup.ml -configure => log target is "<module>-ocaml--configure")
log_1_3() {
{ local -; set +x; } 2> /dev/null
- "$@" >"$LOGS/$LOGTARGET-$1-$3.log" 2>"$LOGS/$LOGTARGET-$1-$3.err"
+ "$@" >"$LOGS/$LOGTARGET-$1-$3_log.txt" 2>"$LOGS/$LOGTARGET-$1-$3_err.txt"
}
# Log command output - log target name is first argument (like logn untar tar xvaf ... => log target is "<module>-untar")
@@ -179,26 +179,26 @@ if [ "${COQREGTESTING:-N}" == "Y" ] ; then
{ local -; set +x; } 2> /dev/null
LOGTARGETEX=$1
shift
- "$@" >"$LOGS/$LOGTARGET-$LOGTARGETEX.log" 2>"$LOGS/$LOGTARGET-$LOGTARGETEX.err"
+ "$@" >"$LOGS/$LOGTARGET-${LOGTARGETEX}_log.txt" 2>"$LOGS/$LOGTARGET-${LOGTARGETEX}_err.txt"
}
else
# If COQREGTESTING, log to log files and console
# Log command output - take log target name from command name (like log1 make => log target is "<module>-make")
log1() {
{ local -; set +x; } 2> /dev/null
- "$@" > >(tee "$LOGS/$LOGTARGET-$1.log" | sed -e "s/^/$LOGTARGET-$1.log: /") 2> >(tee "$LOGS/$LOGTARGET-$1.err" | sed -e "s/^/$LOGTARGET-$1.err: /" 1>&2)
+ "$@" > >(tee "$LOGS/$LOGTARGET-$1_log.txt" | sed -e "s/^/$LOGTARGET-$1_log.txt: /") 2> >(tee "$LOGS/$LOGTARGET-$1_err.txt" | sed -e "s/^/$LOGTARGET-$1_err.txt: /" 1>&2)
}
# Log command output - take log target name from command name and first argument (like log2 make install => log target is "<module>-make-install")
log2() {
{ local -; set +x; } 2> /dev/null
- "$@" > >(tee "$LOGS/$LOGTARGET-$1-$2.log" | sed -e "s/^/$LOGTARGET-$1-$2.log: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$2.err" | sed -e "s/^/$LOGTARGET-$1-$2.err: /" 1>&2)
+ "$@" > >(tee "$LOGS/$LOGTARGET-$1-$2_log.txt" | sed -e "s/^/$LOGTARGET-$1-$2_log.txt: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$2_err.txt" | sed -e "s/^/$LOGTARGET-$1-$2_err.txt: /" 1>&2)
}
# Log command output - take log target name from command name and second argument (like log_1_3 ocaml setup.ml -configure => log target is "<module>-ocaml--configure")
log_1_3() {
{ local -; set +x; } 2> /dev/null
- "$@" > >(tee "$LOGS/$LOGTARGET-$1-$3.log" | sed -e "s/^/$LOGTARGET-$1-$3.log: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$3.err" | sed -e "s/^/$LOGTARGET-$1-$3.err: /" 1>&2)
+ "$@" > >(tee "$LOGS/$LOGTARGET-$1-$3_log.txt" | sed -e "s/^/$LOGTARGET-$1-$3_log.txt: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$3_err.txt" | sed -e "s/^/$LOGTARGET-$1-$3_err.txt: /" 1>&2)
}
# Log command output - log target name is first argument (like logn untar tar xvaf ... => log target is "<module>-untar")
@@ -206,7 +206,7 @@ else
{ local -; set +x; } 2> /dev/null
LOGTARGETEX=$1
shift
- "$@" > >(tee "$LOGS/$LOGTARGET-$LOGTARGETEX.log" | sed -e "s/^/$LOGTARGET-$LOGTARGETEX.log: /") 2> >(tee "$LOGS/$LOGTARGET-$LOGTARGETEX.err" | sed -e "s/^/$LOGTARGET-$LOGTARGETEX.err: /" 1>&2)
+ "$@" > >(tee "$LOGS/$LOGTARGET-${LOGTARGETEX}_log.txt" | sed -e "s/^/$LOGTARGET-${LOGTARGETEX}_log.txt: /") 2> >(tee "$LOGS/$LOGTARGET-${LOGTARGETEX}_err.txt" | sed -e "s/^/$LOGTARGET-${LOGTARGETEX}_err.txt: /" 1>&2)
}
fi
@@ -238,9 +238,10 @@ fi
# $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)
+# $4 [optional] number of path levels to strip from tar (usually 1)
+# $5 [optional] module name (if different from archive)
+# $6 [optional] expand folder name (if different from module name)
+# $7 [optional] module base name (used as 2nd choice for patches, defaults to $5)
# ------------------------------------------------------------------------------
function get_expand_source_tar {
@@ -263,6 +264,12 @@ function get_expand_source_tar {
folder=$name
fi
+ if [ "$#" -ge 7 ] ; then
+ basename=$7
+ else
+ basename=$name
+ fi
+
# Set logging target
logtargetold=$LOGTARGET
LOGTARGET=$name
@@ -314,8 +321,11 @@ function get_expand_source_tar {
fi
# Patch if patch file exists
+ # First try specific patch file name then generic patch file name
if [ -f "$PATCHES/$name.patch" ] ; then
log1 patch -p1 -i "$PATCHES/$name.patch"
+ elif [ -f "$PATCHES/$basename.patch" ] ; then
+ log1 patch -p1 -i "$PATCHES/$basename.patch"
fi
# Go back to base folder
@@ -340,6 +350,7 @@ function get_expand_source_tar {
# $3 file extension
# $4 [optional] number of path levels to strip from tar (usually 1)
# $5 [optional] module name (if different from archive)
+# $6 [optional] module base name (used as 2nd choice for patches, defaults to $5)
# ------------------------------------------------------------------------------
function build_prep {
@@ -356,6 +367,15 @@ function build_prep {
name=$2
fi
+ if [ "$#" -ge 6 ] ; then
+ basename=$6
+ else
+ basename=$name
+ fi
+
+ # Set installer section to not set by default
+ installersection=
+
# Check if build is already done
if [ ! -f "$FLAGFILES/$name.finished" ] ; then
BUILD_PACKAGE_NAME=$name
@@ -365,7 +385,7 @@ function build_prep {
touch "$FLAGFILES/$name.started"
- get_expand_source_tar "$1" "$2" "$3" "$strip" "$name"
+ get_expand_source_tar "$1" "$2" "$3" "$strip" "$name" "$name" "$basename"
cd "$name"
@@ -381,6 +401,61 @@ function build_prep {
}
# ------------------------------------------------------------------------------
+# Like build_prep, but gets the data from an entry in ci-basic-overlay.sh
+# This assumes the following definitions exist in ci-basic-overlay.sh,
+# or in a file in the user-overlays folder:
+# $1_CI_REF
+# $1_CI_ARCHIVEURL
+# $1_CI_GITURL
+# ATTENTION: variables in ci-basic-overlay.sh are loaded by load_overlay_data.
+# load_overlay_data is is called at the end of make_coq (even if the build is skipped)
+#
+# Parameters
+# $1 base name of module in ci-basic-overlay.sh, e.g. mathcomp, bignums, ...
+# ------------------------------------------------------------------------------
+
+function build_prep_overlay {
+ urlvar=$1_CI_ARCHIVEURL
+ gitvar=$1_CI_GITURL
+ refvar=$1_CI_REF
+ url=${!urlvar}
+ git=${!gitvar}
+ ref=${!refvar}
+ ver=$(git ls-remote "$git" "refs/heads/$ref" | cut -f 1)
+ if [[ "$ver" == "" ]]; then
+ # $1_CI_REF must have been a tag or hash, not a branch
+ ver="$ref"
+ fi
+ build_prep "$url" "$ver" tar.gz 1 "$1-$ver" "$1"
+}
+
+# ------------------------------------------------------------------------------
+# Load overlay version variables from ci-basic-overlay.sh and user-overlays/*.sh
+# ------------------------------------------------------------------------------
+
+function load_overlay_data {
+ if [ -n "${GITLAB_CI+}" ]; then
+ export CI_BRANCH="$CI_COMMIT_REF_NAME"
+ if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]]; then
+ export CI_PULL_REQUEST="${CI_BRANCH#pr-}"
+ else
+ export CI_PULL_REQUEST=""
+ fi
+ else
+ export CI_BRANCH=""
+ export CI_PULL_REQUEST=""
+ # Used when building 8.8.0 with the latest scripts
+ export TRAVIS_BRANCH=""
+ export TRAVIS_PULL_REQUEST=""
+ fi
+
+ for overlay in /build/user-overlays/*.sh; do
+ . "$overlay"
+ done
+ . /build/ci-basic-overlay.sh
+}
+
+# ------------------------------------------------------------------------------
# Finalize a module build
# - create name.finished
# - go back to base folder
@@ -392,6 +467,7 @@ function build_post {
touch "$FLAGFILES/$BUILD_PACKAGE_NAME.finished"
PATH=$BUILD_OLDPATH
LOGTARGET=other
+ installer_addon_end
fi
}
@@ -522,6 +598,101 @@ function files_to_nsis {
tr '/' '\\' < "/build/filelists/$1" | sed -r 's/^\.(.*)\\([^\\]+)$/SetOutPath $INSTDIR\\\1\nFile ${COQ_SRC_PATH}\\\1\\\2/' > "/build/filelists/$1.nsh"
}
+# ------------------------------------------------------------------------------
+# Create an nsis installer addon section
+#
+# parameters
+# $1 identifier of installer section and base name of file list files
+# $2 human readable name of section
+# $3 description of section
+# $4 flags (space separated list of keywords): off = default off
+#
+# $1 must be a valid NSIS identifier!
+# ------------------------------------------------------------------------------
+
+function installer_addon_section {
+ installersection=$1
+ list_files "addon_pre_$installersection"
+
+ echo 'LangString' "DESC_$1" '${LANG_ENGLISH}' "\"$3\"" >> "/build/filelists/addon_strings.nsh"
+
+ echo '!insertmacro MUI_DESCRIPTION_TEXT' '${'"Sec_$1"'}' '$('"DESC_$1"')' >> "/build/filelists/addon_descriptions.nsh"
+
+ local sectionoptions=
+ if [[ "$4" == *off* ]] ; then sectionoptions+=" /o" ; fi
+
+ echo "Section $sectionoptions \"$2\" Sec_$1" >> "/build/filelists/addon_sections.nsh"
+ echo 'SetOutPath "$INSTDIR\"' >> "/build/filelists/addon_sections.nsh"
+ echo '!include "..\..\..\filelists\addon_'"$1"'.nsh"' >> "/build/filelists/addon_sections.nsh"
+ echo 'SectionEnd' >> "/build/filelists/addon_sections.nsh"
+}
+
+# ------------------------------------------------------------------------------
+# Start an installer addon dependency group
+#
+# parameters
+# $1 identifier of the section which depends on other sections
+# The parameters must match the $1 parameter of a installer_addon_section call
+# ------------------------------------------------------------------------------
+
+dependencysections=
+
+function installer_addon_dependency_beg {
+ installer_addon_dependency "$1"
+ dependencysections="$1 $dependencysections"
+}
+
+# ------------------------------------------------------------------------------
+# End an installer addon dependency group
+# ------------------------------------------------------------------------------
+
+function installer_addon_dependency_end {
+ set -- $dependencysections
+ shift
+ dependencysections="$*"
+}
+
+# ------------------------------------------------------------------------------
+# Create an nsis installer addon dependency entry
+# This needs to be bracketed with installer_addon_dependencies_beg/end
+#
+# parameters
+# $1 identifier of the section on which other sections might depend
+# The parameters must match the $1 parameter of a installer_addon_section call
+# ------------------------------------------------------------------------------
+
+function installer_addon_dependency {
+ for section in $dependencysections ; do
+ echo '${CheckSectionDependency} ${Sec_'"$section"'} ${Sec_'"$1"'} '"'$section' '$1'" >> "/build/filelists/addon_dependencies.nsh"
+ done
+}
+
+# ------------------------------------------------------------------------------
+# Finish an installer section after an addon build
+#
+# This creates the file list files
+#
+# parameters: none
+# ------------------------------------------------------------------------------
+
+function installer_addon_end {
+ if [ -n "$installersection" ]; then
+ list_files "addon_post_$installersection"
+ diff_files "addon_$installersection" "addon_post_$installersection" "addon_pre_$installersection"
+ files_to_nsis "addon_$installersection"
+ fi
+}
+
+# ------------------------------------------------------------------------------
+# Set all timeouts in all .v files to 1000
+# Since timeouts can lead to CI failures, this is useful
+#
+# parameters: none
+# ------------------------------------------------------------------------------
+
+function coq_set_timeouts_1000 {
+ find . -type f -name '*.v' -print0 | xargs -0 sed -i 's/timeout\s\+[0-9]\+/timeout 1000/'
+}
###################### MODULE BUILD FUNCTIONS #####################
@@ -1203,7 +1374,7 @@ function copy_coq_license {
# FIXME: this is not the micromega license
# It only applies to code that was copied into one single file!
install -D README.md "$PREFIXCOQ/license_readme/coq/ReadMe.md"
- install -D CHANGES "$PREFIXCOQ/license_readme/coq/Changes.txt"
+ install -D CHANGES.md "$PREFIXCOQ/license_readme/coq/Changes.md"
install -D INSTALL "$PREFIXCOQ/license_readme/coq/Install.txt"
install -D doc/README.md "$PREFIXCOQ/license_readme/coq/ReadMeDoc.md" || true
fi
@@ -1287,6 +1458,8 @@ function make_coq {
build_post
fi
+
+ load_overlay_data
}
##### GNU Make for MinGW #####
@@ -1450,18 +1623,15 @@ function make_coq_installer {
fi
}
-###################### ADDONS #####################
+###################### ADDON COQ LIBRARIES / PLUGINS / TOOLS #####################
# The bignums library
# Provides BigN, BigZ, BigQ that used to be part of Coq standard library
function make_addon_bignums {
- bignums_SHA=$(git ls-remote "$bignums_CI_GITURL" "refs/heads/$bignums_CI_REF" | cut -f 1)
- if [[ "$bignums_SHA" == "" ]]; then
- # $bignums_CI_REF must have been a tag / commit and not a branch
- bignums_SHA="$bignums_CI_REF"
- fi
- if build_prep "$bignums_CI_ARCHIVEURL" "$bignums_SHA" zip 1 "bignums-$bignums_SHA"; then
+ installer_addon_dependency bignums
+ if build_prep_overlay bignums; then
+ installer_addon_section bignums "Bignums" "Coq library for fast arbitrary size numbers" ""
# To make command lines shorter :-(
echo 'COQ_SRC_SUBDIRS:=$(filter-out plugins/%,$(COQ_SRC_SUBDIRS)) plugins/syntax' >> Makefile.coq.local
log1 make all
@@ -1470,61 +1640,277 @@ function make_addon_bignums {
fi
}
+# Equations plugin
+# A function definition plugin
+
+function make_addon_equations {
+ installer_addon_dependency equations
+ if build_prep_overlay Equations; then
+ installer_addon_section equations "Equations" "Coq plugin for defining functions by equations" ""
+ # Note: PATH is automatically saved/restored by build_prep / build_post
+ PATH=$COQBIN:$PATH
+ logn coq_makefile ${COQBIN}coq_makefile -f _CoqProject -o Makefile
+ log1 make
+ log2 make install
+ build_post
+ fi
+}
+
+# mathcomp - ssreflect and mathematical components library
+
+function make_addon_mathcomp {
+ installer_addon_dependency mathcomp
+ if build_prep_overlay mathcomp; then
+ installer_addon_section mathcomp "Math-Components" "Coq library with mathematical components" ""
+ cd mathcomp
+ log1 make $MAKE_OPT
+ log2 make install
+ build_post
+ fi
+}
+
+# ssreflect part of mathcomp
+
+function make_addon_ssreflect {
+ # if mathcomp addon is requested, build this instead
+ if [[ "$COQ_ADDONS" == *mathcomp* ]]; then
+ make_addon_mathcomp
+ else
+ # Note: since either mathcomp or ssreflect is defined, it is fine to name both mathcomp
+ installer_addon_dependency ssreflect
+ if build_prep_overlay mathcomp; then
+ installer_addon_section ssreflect "SSReflect" "Coq support library for small scale reflection plugin" ""
+ cd mathcomp
+ logn make-makefile make Makefile.coq
+ logn make-ssreflect make $MAKE_OPT -f Makefile.coq ssreflect/all_ssreflect.vo
+ logn make-install make -f Makefile.coq install
+ build_post
+ fi
+ fi
+}
+
# Ltac-2 plugin
# A new (experimental) tactic language
function make_addon_ltac2 {
- ltac2_SHA=$(git ls-remote "$ltac2_CI_GITURL" "refs/heads/$ltac2_CI_REF" | cut -f 1)
- if [[ "$ltac2_SHA" == "" ]]; then
- # $ltac2_CI_REF must have been a tag / commit and not a branch
- ltac2_SHA="$ltac2_CI_REF"
- fi
- if build_prep "$ltac2_CI_ARCHIVEURL" "$ltac2_SHA" zip 1 "ltac2-$ltac2_SHA"; then
+ installer_addon_dependency ltac2
+ if build_prep_overlay ltac2; then
+ installer_addon_section ltac2 "Ltac-2" "Coq plugin with the Ltac-2 enhanced tactic language" ""
log1 make all
log2 make install
build_post
fi
}
-# Equations plugin
-# A function definition plugin
-
-function make_addon_equations {
- Equations_SHA=$(git ls-remote "$Equations_CI_GITURL" "refs/heads/$Equations_CI_REF" | cut -f 1)
- if [[ "$Equations_SHA" == "" ]]; then
- # $Equations_CI_REF must have been a tag / commit and not a branch
- Equations_SHA="$Equations_CI_REF"
+# UniCoq plugin
+# An alternative unification algorithm
+function make_addon_unicoq {
+ installer_addon_dependency unicoq
+ if build_prep_overlay unicoq; then
+ installer_addon_section unicoq "Unicoq" "Coq plugin for an enhanced unification algorithm" ""
+ log1 coq_makefile -f Make -o Makefile
+ log1 make
+ log2 make install
+ build_post
fi
- if build_prep "$Equations_CI_ARCHIVEURL" "$Equations_SHA" zip 1 "Equations-$Equations_SHA"; then
- # Note: PATH is autmatically saved/restored by build_prep / build_post
- PATH=$COQBIN:$PATH
- logn coq_makefile ${COQBIN}coq_makefile -f _CoqProject -o Makefile
+}
+
+# Mtac2 plugin
+# An alternative typed tactic language
+function make_addon_mtac2 {
+ installer_addon_dependency_beg mtac2
+ make_addon_unicoq
+ installer_addon_dependency_end
+ if build_prep_overlay mtac2; then
+ installer_addon_section mtac2 "Mtac-2" "Coq plugin for a typed tactic language for Coq." ""
+ log1 coq_makefile -f _CoqProject -o Makefile
log1 make
log2 make install
build_post
fi
}
-function make_addons {
- if [ -n "$GITLAB_CI" ]; then
- export CI_BRANCH="$CI_COMMIT_REF_NAME"
- if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]]; then
- export CI_PULL_REQUEST="${CI_BRANCH#pr-}"
- else
- export CI_PULL_REQUEST=""
+# Menhir parser generator
+
+function make_addon_menhir {
+ make_menhir
+ # If COQ and OCaml are installed to the same folder, there is nothing to do
+ installer_addon_dependency menhir
+ if [ "$PREFIXOCAML" != "$PREFIXCOQ" ] ; then
+ # Just install menhir files required for COQ to COQ target folder
+ if [ ! -f "$FLAGFILES/menhir-addon.finished" ] ; then
+ installer_addon_section menhir "Menhir" "Menhir parser generator windows executable and libraries" ""
+ LOGTARGET=menhir-addon
+ touch "$FLAGFILES/menhir-addon.started"
+ # Menhir executable
+ install_glob "$PREFIXOCAML/bin" 'menhir.exe' "$PREFIXCOQ/bin/"
+ # Menhir Standard library
+ install_glob "$PREFIXOCAML/share/menhir/" '*.mly' "$PREFIXCOQ/share/menhir/"
+ # Menhir PDF doc
+ install_glob "$PREFIXOCAML/share/doc/menhir/" '*.pdf' "$PREFIXCOQ/doc/menhir/"
+ touch "$FLAGFILES/menhir-addon.finished"
+ LOGTARGET=other
+ installer_addon_end
fi
- else
- export CI_BRANCH=""
- export CI_PULL_REQUEST=""
fi
- for overlay in /build/user-overlays/*.sh; do
- . "$overlay"
- done
- . /build/ci-basic-overlay.sh
+}
+
+# COQ library for Menhir
+
+function make_addon_menhirlib {
+ installer_addon_dependency menhirlib
+ if build_prep_overlay menhirlib; then
+ installer_addon_section menhirlib "Menhirlib" "Coq support library for using Menhir generated parsers in Coq" ""
+ # The supplied makefiles don't work in any way on cygwin
+ cd src
+ echo -R . MenhirLib > _CoqProject
+ ls -1 *.v >> _CoqProject
+ log1 coq_makefile -f _CoqProject -o Makefile.coq
+ log1 make -f Makefile.coq all
+ logn make-install make -f Makefile.coq install
+ build_post
+ fi
+}
+
+# CompCert
+
+function make_addon_compcert {
+ installer_addon_dependency_beg compcert
+ make_menhir
+ make_addon_menhirlib
+ installer_addon_dependency_end
+ if build_prep_overlay CompCert; then
+ installer_addon_section compcert "CompCert" "ATTENTION: THIS IS NOT OPEN SOURCE! CompCert verified C compiler and Clightgen (required for using VST for your own code)" "off"
+ logn configure ./configure -ignore-coq-version -clightgen -prefix "$PREFIXCOQ" -coqdevdir "$PREFIXCOQ/lib/coq/user-contrib/compcert" x86_32-cygwin
+ log1 make
+ log2 make install
+ logn install-license-1 install -D -T "LICENSE" "$PREFIXCOQ/lib/coq/user-contrib/compcert/LICENSE"
+ logn install-license-2 install -D -T "LICENSE" "$PREFIXCOQ/lib/compcert/LICENSE"
+ build_post
+ fi
+}
+
+# Princeton VST
+
+function install_addon_vst {
+ VSTDEST="$PREFIXCOQ/lib/coq/user-contrib/VST"
+
+ # Install VST .v, .vo, .c and .h files
+ install_rec compcert '*.v' "$VSTDEST/compcert/"
+ install_rec compcert '*.vo' "$VSTDEST/compcert/"
+ install_glob "msl" '*.v' "$VSTDEST/msl/"
+ install_glob "msl" '*.vo' "$VSTDEST/msl/"
+ install_glob "sepcomp" '*.v' "$VSTDEST/sepcomp/"
+ install_glob "sepcomp" '*.vo' "$VSTDEST/sepcomp/"
+ install_glob "floyd" '*.v' "$VSTDEST/floyd/"
+ install_glob "floyd" '*.vo' "$VSTDEST/floyd/"
+ install_glob "progs" '*.v' "$VSTDEST/progs/"
+ install_glob "progs" '*.c' "$VSTDEST/progs/"
+ install_glob "progs" '*.h' "$VSTDEST/progs/"
+ install_glob "veric" '*.v' "$VSTDEST/msl/"
+ install_glob "veric" '*.vo' "$VSTDEST/msl/"
+
+ # Install VST documentation files
+ install_glob "." 'LICENSE' "$VSTDEST"
+ install_glob "." '*.md' "$VSTDEST"
+ install_glob "compcert" '*' "$VSTDEST/compcert"
+ install_glob "doc" '*.pdf' "$VSTDEST/doc"
+
+ # Install VST _CoqProject files
+ install_glob "." '_CoqProject*' "$VSTDEST"
+ install_glob "." '_CoqProject-export' "$VSTDEST/progs"
+}
+
+function make_addon_vst {
+ installer_addon_dependency vst
+ if build_prep_overlay VST; then
+ installer_addon_section vst "VST" "ATTENTION: SOME INCLUDED COMPCERT PARTS ARE NOT OPEN SOURCE! Verified Software Toolchain for verifying C code" "off"
+ log1 coq_set_timeouts_1000
+ log1 make IGNORECOQVERSION=true $MAKE_OPT
+ log1 install_addon_vst
+ build_post
+ fi
+}
+
+# coquelicot Real analysis
+
+function make_addon_coquelicot {
+ installer_addon_dependency_beg coquelicot
+ make_addon_ssreflect
+ installer_addon_dependency_end
+ if build_prep_overlay Coquelicot; then
+ installer_addon_section coquelicot "Coquelicot" "Coq library for real analysis" ""
+ logn configure ./configure --libdir="$PREFIXCOQ/lib/coq/user-contrib/Coquelicot"
+ logn remake ./remake
+ logn remake-install ./remake install
+ build_post
+ fi
+}
+
+# AAC associative / commutative rewriting
+
+function make_addon_aactactics {
+ installer_addon_dependency aac
+ if build_prep_overlay aactactics; then
+ installer_addon_section aac "AAC" "Coq plugin for extensible associative and commutative rewriting" ""
+ log1 make
+ log2 make install
+ build_post
+ fi
+}
+
+# extlib
+
+function make_addon_extlib {
+ installer_addon_dependency extlib
+ if build_prep_overlay ext_lib; then
+ installer_addon_section extlib "Ext-Lib" "Coq library with many reusable general purpose components" ""
+ log1 make $MAKE_OPT
+ log2 make install
+ build_post
+ fi
+}
+
+# SimpleIO
+
+function make_addon_simple_io {
+ installer_addon_dependency simpleIO
+ if build_prep_overlay simple_io; then
+ installer_addon_section simpleIO "SimpleIO" "Coq plugin for reading and writing files directly from Coq code" ""
+ log1 make $MAKE_OPT
+ log2 make install
+ build_post
+ fi
+}
+
+# Quickchick Randomized Property-Based Testing Plugin for Coq
+
+function make_addon_quickchick {
+ installer_addon_dependency_beg quickchick
+ make_addon_ssreflect
+ make_addon_extlib
+ make_addon_simple_io
+ make_ocamlbuild
+ installer_addon_dependency_end
+ if build_prep_overlay quickchick; then
+ installer_addon_section quickchick "QuickChick" "Coq plugin for randomized testing and counter example search" ""
+ log1 make
+ log2 make install
+ build_post
+ fi
+}
+
+# Main function for building addons
+
+function make_addons {
+ # Note: ':' is the empty command, which does not produce any output
+ : > "/build/filelists/addon_dependencies.nsh"
for addon in $COQ_ADDONS; do
"make_addon_$addon"
done
+
+ sort -u -o "/build/filelists/addon_dependencies.nsh" "/build/filelists/addon_dependencies.nsh"
}
###################### TOP LEVEL BUILD #####################
diff --git a/dev/build/windows/patches_coq/coq_new.nsi b/dev/build/windows/patches_coq/coq_new.nsi
index 55fba6d5ab..9947965c28 100644
--- a/dev/build/windows/patches_coq/coq_new.nsi
+++ b/dev/build/windows/patches_coq/coq_new.nsi
@@ -38,43 +38,20 @@ Var INSTDIR_DBS ; INSTDIR with \\ instead of \
;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
+;Extra license pages
- ;Description
- LangString DESC_1 ${LANG_ENGLISH} "This package contains Coq and CoqIDE."
- LangString DESC_2 ${LANG_ENGLISH} "This package contains the following extra Coq packages: ${COQ_ADDONS}"
- ;LangString DESC_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."
+!macro MUI_PAGE_LICENSE_EXTRA Licensefile Header Subheader Bottom SelFunc
+ !define MUI_PAGE_HEADER_TEXT "${Header}"
+ !define MUI_PAGE_HEADER_SUBTEXT "${Subheader}"
+ !define MUI_LICENSEPAGE_TEXT_BOTTOM "${Bottom}"
+ !define MUI_PAGE_CUSTOMFUNCTION_PRE ${SelFunc}
+ !insertmacro MUI_PAGE_LICENSE "${Licensefile}"
+!macroend
;--------------------------------
; Check for white spaces
@@ -95,7 +72,6 @@ FunctionEnd
;--------------------------------
;Installer Sections
-
Section "Coq" Sec1
SetOutPath "$INSTDIR\"
@@ -105,7 +81,7 @@ Section "Coq" Sec1
;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" \
@@ -123,7 +99,7 @@ Section "Coq" Sec1
; Create start menu entries
; SetOutPath is required for the path in the .lnk files
- SetOutPath "$INSTDIR"
+ SetOutPath "$INSTDIR"
CreateDirectory "$SMPROGRAMS\Coq"
; The first shortcut set here is treated as main application by Windows 7/8.
; Use CoqIDE as main application
@@ -138,24 +114,23 @@ SectionEnd
;OCAML Section "Ocaml for native compute and plugin development" Sec2
;OCAML SetOutPath "$INSTDIR\"
;OCAML !include "..\..\..\filelists\ocaml.nsh"
-;OCAML
+;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
;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 packages" Sec2
- SetOutPath "$INSTDIR\"
- !include "..\..\..\filelists\coq_addons.nsh"
-SectionEnd
+
+SectionGroup "Coq addons" Sec2
+ !include "..\..\..\filelists\addon_sections.nsh"
+SectionGroupEnd
Section "Coq files for plugin developers" Sec3
SetOutPath "$INSTDIR\"
@@ -179,6 +154,130 @@ SectionEnd
;OCAML SectionEnd
;--------------------------------
+;Section dependencies
+
+; Parameters on the stack:
+; top-0 : section B on which section A dependencies
+; top-1 : section A, which depends on section B
+; top-2 : name of section B
+; top-3 : name of section A
+
+Function CheckSectionDependency
+ ; stack=nameB nameA secB secA rest
+ Exch $R3 ; stack=$R3 nameA secB secA rest; $R3=nameB
+ Exch ; stack=nameA $R3 secB secA rest
+ Exch $R2 ; stack=$R2 $R3 secB secA rest; $R2=nameA
+ Exch 2 ; stack=secB $R3 $R2 secA rest
+ Exch $R1 ; stack=$R1 $R3 $R2 secA rest; $R1=secB
+ Exch 3 ; stack=secA $R3 $R2 $R1 rest;
+ Exch $R0 ; stack=$R0 $R3 $R2 $R1 rest; $R0=secA
+ ; Take care of save order when popping the stack!
+ Push $R4
+ Push $R5
+
+ SectionGetFlags $R0 $R0
+ IntOp $R0 $R0 & ${SF_SELECTED}
+
+ SectionGetFlags $R1 $R4
+ IntOp $R5 $R4 & ${SF_SELECTED}
+
+ ${If} $R0 == ${SF_SELECTED}
+ ${AndIf} $R5 != ${SF_SELECTED}
+
+ IntOp $R5 $R4 | ${SF_SELECTED}
+ SectionSetFlags $R1 $R5
+ MessageBox MB_OK '"$R3" has been selected, because "$R2" depends on it'
+
+ ${EndIf}
+
+ Pop $R5
+ Pop $R4
+ Pop $R0
+ Pop $R3
+ Pop $R2
+ Pop $R1
+FunctionEnd
+
+!macro CheckSectionDependency secA secB nameA nameB
+ Push "${secA}"
+ Push "${secB}"
+ Push "${nameA}"
+ Push "${nameB}"
+ Call CheckSectionDependency
+!macroend
+
+!define CheckSectionDependency "!insertmacro CheckSectionDependency"
+
+Function .onSelChange
+ !include "..\..\..\filelists\addon_dependencies.nsh"
+FunctionEnd
+
+;--------------------------------
+;Modern UI Configuration
+
+; Note: this must be placed after the sections, because below we need to check at compile time
+; if sections exist (by !ifdef <section_index_var>) to decide if the license page must be included.
+; The section index variables are only defined after the section definitions.
+
+ !define MUI_ICON "${COQ_ICON}"
+
+ !insertmacro MUI_PAGE_WELCOME
+ !insertmacro MUI_PAGE_LICENSE "${COQ_SRC_PATH}/license_readme/coq/License.txt"
+ !insertmacro MUI_PAGE_COMPONENTS
+
+ !ifdef Sec_compcert
+ !define LicCompCert_Title "CompCert License Agreement"
+ !define LicCompCert_SubTitle "You selected the CompCert addon. CompCert is not open source. Please review the license terms before installing CompCert!"
+ !define LicCompCert_Bottom "If you accept the terms of the agreement, click I Agree to continue. Otherwise go back and unselect the CompCert addon."
+ !insertmacro MUI_PAGE_LICENSE_EXTRA "${COQ_SRC_PATH}/lib/coq/user-contrib/compcert/LICENSE" "${LicCompCert_Title}" "${LicCompCert_SubTitle}" "${LicCompCert_Bottom}" SelFuncCompCert
+
+ Function SelFuncCompCert
+ ${Unless} ${SectionIsSelected} ${Sec_compcert}
+ Abort
+ ${EndUnless}
+ FunctionEnd
+ !endif
+
+ !ifdef Sec_vst
+ !define LicVST_Title "Princeton VST License Agreement"
+ !define LicVST_SubTitle "You selected the VST addon. VST contains parts of CompCert which are not open source. Please review the license terms before installing VST!"
+ !define LicVST_Bottom "If you accept the terms of the agreement, click I Agree to continue. Otherwise go back and unselect the VST addon."
+ !insertmacro MUI_PAGE_LICENSE_EXTRA "${COQ_SRC_PATH}/lib/coq/user-contrib/VST/LICENSE" "${LicVST_Title}" "${LicVST_SubTitle}" "${LicVST_Bottom}" SelFuncVST
+
+ Function SelFuncVST
+ ${Unless} ${SectionIsSelected} ${Sec_vst}
+ Abort
+ ${EndUnless}
+ FunctionEnd
+ !endif
+
+ !define MUI_DIRECTORYPAGE_TEXT_TOP "Select where to install Coq. The path MUST NOT include spaces."
+ !insertmacro MUI_PAGE_DIRECTORY
+ !insertmacro MUI_PAGE_INSTFILES
+ !insertmacro MUI_PAGE_FINISH
+
+ !insertmacro MUI_UNPAGE_WELCOME
+ !insertmacro MUI_UNPAGE_CONFIRM
+ !insertmacro MUI_UNPAGE_INSTFILES
+ !insertmacro MUI_UNPAGE_FINISH
+
+;--------------------------------
+;Languages
+
+ !insertmacro MUI_LANGUAGE "English"
+
+;--------------------------------
+;Language Strings
+
+ ;Description
+ LangString DESC_1 ${LANG_ENGLISH} "This package contains Coq and CoqIDE."
+ LangString DESC_2 ${LANG_ENGLISH} "This package contains the following extra Coq packages: ${COQ_ADDONS}"
+ LangString DESC_3 ${LANG_ENGLISH} "This package contains the development files needed in order to build a plugin for Coq."
+ ; LangString DESC_4 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for the current user."
+ ; LangString DESC_5 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for all users."
+ !include "..\..\..\filelists\addon_strings.nsh"
+
+;--------------------------------
;Descriptions
!insertmacro MUI_FUNCTION_DESCRIPTION_BEGIN
@@ -187,8 +286,9 @@ SectionEnd
!insertmacro MUI_DESCRIPTION_TEXT ${Sec3} $(DESC_3)
;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec4} $(DESC_4)
;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec5} $(DESC_5)
+ !include "..\..\..\filelists\addon_descriptions.nsh"
!insertmacro MUI_FUNCTION_DESCRIPTION_END
-
+
;--------------------------------
;Uninstaller Section
@@ -214,7 +314,7 @@ Section "Uninstall"
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"
diff --git a/dev/build/windows/patches_coq/quickchick.patch b/dev/build/windows/patches_coq/quickchick.patch
new file mode 100755
index 0000000000..1afa6e7f95
--- /dev/null
+++ b/dev/build/windows/patches_coq/quickchick.patch
@@ -0,0 +1,26 @@
+diff/patch file created on Mon, Aug 27, 2018 9:21:52 AM with:
+difftar-folder.sh tarballs/quickchick-v1.0.2.tar.gz quickchick-v1.0.2 1
+TARFILE= tarballs/quickchick-v1.0.2.tar.gz
+FOLDER= quickchick-v1.0.2
+TARSTRIP= 1
+TARPREFIX= QuickChick-1.0.2/
+ORIGFOLDER= quickchick-v1.0.2.orig
+--- quickchick-v1.0.2.orig/Makefile 2018-08-22 18:21:39.000000000 +0200
++++ quickchick-v1.0.2/Makefile 2018-08-27 09:21:04.710461100 +0200
+@@ -2,7 +2,7 @@
+ .PHONY: plugin install install-plugin clean quickChickTool
+
+ QCTOOL_DIR=quickChickTool
+-QCTOOL_EXE=quickChickTool.byte
++QCTOOL_EXE=quickChickTool.native
+ QCTOOL_SRC=$(QCTOOL_DIR)/quickChickTool.ml \
+ $(QCTOOL_DIR)/quickChickToolTypes.ml \
+ $(QCTOOL_DIR)/quickChickToolLexer.mll \
+@@ -32,7 +32,7 @@
+ install: all
+ $(V)$(MAKE) -f Makefile.coq install > $(TEMPFILE)
+ # Manually copying the remaining files
+- $(V)cp $(QCTOOL_EXE) $(shell opam config var bin)/quickChick
++ $(V)cp $(QCTOOL_EXE) "$(COQBIN)/quickChick"
+ # $(V)cp src/quickChickLib.cmx $(COQLIB)/user-contrib/QuickChick
+ # $(V)cp src/quickChickLib.o $(COQLIB)/user-contrib/QuickChick
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 20:20:16 +0000