diff options
Diffstat (limited to 'dev/build/windows/MakeCoq_MinGW.bat')
| -rwxr-xr-x[-rw-r--r--] | dev/build/windows/MakeCoq_MinGW.bat | 225 |
1 files changed, 134 insertions, 91 deletions
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index 1e08cc5a..61cf6bc4 100644..100755 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -18,7 +18,7 @@ REM ========== DEFAULT VALUES FOR PARAMETERS ========== REM For a description of all parameters, see ReadMe.txt -SET BATCHFILE=%0 +SET BATCHFILE=%~0 SET BATCHDIR=%~dp0 REM see -arch in ReadMe.txt, but values are x86_64 or i686 (not 64 or 32) @@ -34,7 +34,7 @@ REM see -ocaml in ReadMe.txt SET INSTALLOCAML=N REM see -make in ReadMe.txt -SET INSTALLMAKE=Y +SET INSTALLMAKE=N REM see -destcyg in ReadMe.txt SET DESTCYG=C:\bin\cygwin_coq @@ -47,9 +47,11 @@ SET SETUP=setup-x86_64.exe REM see -proxy in ReadMe.txt IF DEFINED HTTP_PROXY ( - SET PROXY="%HTTP_PROXY:http://=%" + SET PROXY=%HTTP_PROXY:http://=% ) else ( - SET PROXY="" + REM One can't set a variable to empty in DOS, but you can set it to a space this way. + REM The quotes are just there to make the space visible and to protect from "remove trailing spaces". + SET "PROXY= " ) REM see -cygrepo in ReadMe.txt @@ -76,18 +78,21 @@ 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" ( +IF "%~0" == "-arch" ( + IF "%~1" == "32" ( SET ARCH=i686 SET SETUP=setup-x86.exe ) ELSE ( - IF "%1" == "64" ( + IF "%~1" == "64" ( SET ARCH=x86_64 SET SETUP=setup-x86_64.exe ) ELSE ( @@ -100,15 +105,15 @@ IF "%0" == "-arch" ( GOTO Parse ) -IF "%0" == "-mode" ( - IF "%1" == "mingwincygwin" ( - SET INSTALLMODE=%1 +IF "%~0" == "-mode" ( + IF "%~1" == "mingwincygwin" ( + SET INSTALLMODE=%~1 ) ELSE ( - IF "%1" == "absolute" ( - SET INSTALLMODE=%1 + IF "%~1" == "absolute" ( + SET INSTALLMODE=%~1 ) ELSE ( - IF "%1" == "relocatable" ( - SET INSTALLMODE=%1 + IF "%~1" == "relocatable" ( + SET INSTALLMODE=%~1 ) ELSE ( ECHO "Invalid -mode, valid are mingwincygwin, absolute and relocatable" GOTO :EOF @@ -120,122 +125,137 @@ IF "%0" == "-mode" ( GOTO Parse ) -IF "%0" == "-installer" ( - SET MAKEINSTALLER=%1 +IF "%~0" == "-installer" ( + SET MAKEINSTALLER=%~1 + CALL :CheckYN -installer %~1 || GOTO ErrorExit + SHIFT + SHIFT + GOTO Parse +) + +IF "%~0" == "-ocaml" ( + SET INSTALLOCAML=%~1 + CALL :CheckYN -installer %~1 || GOTO ErrorExit SHIFT SHIFT GOTO Parse ) -IF "%0" == "-ocaml" ( - SET INSTALLOCAML=%1 +IF "%~0" == "-make" ( + SET INSTALLMAKE=%~1 + CALL :CheckYN -installer %~1 || GOTO ErrorExit SHIFT SHIFT GOTO Parse ) -IF "%0" == "-make" ( - SET INSTALLMAKE=%1 +IF "%~0" == "-destcyg" ( + SET DESTCYG=%~1 SHIFT SHIFT GOTO Parse ) -IF "%0" == "-destcyg" ( - SET DESTCYG=%1 +IF "%~0" == "-destcoq" ( + SET DESTCOQ=%~1 SHIFT SHIFT GOTO Parse ) -IF "%0" == "-destcoq" ( - SET DESTCOQ=%1 +IF "%~0" == "-setup" ( + SET SETUP=%~1 SHIFT SHIFT GOTO Parse ) -IF "%0" == "-setup" ( - SET SETUP=%1 +IF "%~0" == "-proxy" ( + SET PROXY=%~1 SHIFT SHIFT GOTO Parse ) -IF "%0" == "-proxy" ( - SET PROXY="%1" +IF "%~0" == "-cygrepo" ( + SET CYGWIN_REPOSITORY=%~1 SHIFT SHIFT GOTO Parse ) -IF "%0" == "-cygrepo" ( - SET CYGWIN_REPOSITORY="%1" +IF "%~0" == "-cygcache" ( + SET CYGWIN_LOCAL_CACHE_WFMT=%~1 SHIFT SHIFT GOTO Parse ) -IF "%0" == "-cygcache" ( - SET CYGWIN_LOCAL_CACHE_WFMT="%1" +IF "%~0" == "-cyglocal" ( + SET CYGWIN_FROM_CACHE=%~1 + CALL :CheckYN -cyglocal %~1 || GOTO ErrorExit SHIFT SHIFT GOTO Parse ) -IF "%0" == "-cyglocal" ( - SET CYGWIN_FROM_CACHE=%1 +IF "%~0" == "-cygquiet" ( + SET CYGWIN_QUIET=%~1 + CALL :CheckYN -cygquiet %~1 || GOTO ErrorExit SHIFT SHIFT GOTO Parse ) -IF "%0" == "-cygquiet" ( - SET CYGWIN_QUIET=%1 +IF "%~0" == "-srccache" ( + SET SOURCE_LOCAL_CACHE_WFMT=%~1 SHIFT SHIFT GOTO Parse ) -IF "%0" == "-srccache" ( - SET SOURCE_LOCAL_CACHE_WFMT="%1" +IF "%~0" == "-coqver" ( + SET COQ_VERSION=%~1 SHIFT SHIFT GOTO Parse ) -IF "%0" == "-coqver" ( - SET COQ_VERSION=%1 +IF "%~0" == "-gtksrc" ( + SET GTK_FROM_SOURCES=%~1 + CALL :CheckYN -gtksrc %~1 || GOTO ErrorExit SHIFT SHIFT GOTO Parse ) -IF "%0" == "-gtksrc" ( - SET GTK_FROM_SOURCES=%1 +IF "%~0" == "-threads" ( + SET MAKE_THREADS=%~1 SHIFT SHIFT GOTO Parse ) -IF "%0" == "-threads" ( - SET MAKE_THREADS=%1 +IF "%~0" == "-addon" ( + SET "COQ_ADDONS=%COQ_ADDONS% %~1" SHIFT SHIFT GOTO Parse ) -IF NOT "%0" == "" ( + +IF NOT "%~0" == "" ( ECHO Install cygwin and download, compile and install OCaml and Coq for MinGW - ECHO !!! Illegal parameter %0 - ECHO Usage: + ECHO !!! Illegal parameter %~0 + ECHO Usage: ECHO MakeCoq_MinGW CALL :PrintPars - goto :EOF + 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 ) @@ -247,16 +267,14 @@ IF "%INSTALLMODE%" == "mingwincygwin" ( 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 "%COQREGTESTING%"=="Y" (GOTO DontAsk) + SET /p ANSWER="Is this correct? y/n " IF NOT "%ANSWER%"=="y" (GOTO :EOF) :DontAsk @@ -296,12 +314,13 @@ 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% +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= +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 @@ -315,17 +334,9 @@ 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 @@ -337,18 +348,31 @@ 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% ^ + --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 make,unzip ^ -P gdb,liblzma5 ^ - -P patch,automake1.14,automake1.15 ^ + -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 ^ @@ -358,15 +382,13 @@ IF "%RUNSETUP%"=="Y" ( -P gtk-update-icon-cache ^ -P libtool,automake ^ -P intltool ^ - > "%LOGFILE%" ^ - || GOTO :Error + %EXTRAPACKAGES% ^ + || GOTO ErrorExit - MKDIR %CYGWIN_INSTALLDIR_WFMT%\build - MKDIR %CYGWIN_INSTALLDIR_WFMT%\build\buildlogs - MOVE "%LOGFILE%" %CYGWIN_INSTALLDIR_WFMT%\build\buildlogs\cygwinsetup.log || GOTO :Error + MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build" + MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\buildlogs" ) - 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. @@ -377,18 +399,24 @@ IF NOT "%CYGWIN_QUIET%" == "Y" ( ECHO ========== CONFIGURE CYGWIN USER ACCOUNT ========== -copy %BATCHDIR%\configure_profile.sh %CYGWIN_INSTALLDIR_WFMT%\var\tmp || GOTO :Error -%BASH% --login %CYGWIN_INSTALLDIR_CFMT%\var\tmp\configure_profile.sh %PROXY% || GOTO :Error +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 +MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build" +MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\patches" -COPY %BATCHDIR%\makecoq_mingw.sh %CYGWIN_INSTALLDIR_WFMT%\build || GOTO :Error -COPY %BATCHDIR%\patches_coq\*.* %CYGWIN_INSTALLDIR_WFMT%\build\patches || GOTO :Error +COPY "%BATCHDIR%\makecoq_mingw.sh" "%CYGWIN_INSTALLDIR_WFMT%\build" || GOTO ErrorExit +COPY "%BATCHDIR%\patches_coq\*.*" "%CYGWIN_INSTALLDIR_WFMT%\build\patches" || GOTO ErrorExit -%BASH% --login %CYGWIN_INSTALLDIR_CFMT%\build\makecoq_mingw.sh || GOTO :Error +%BASH% --login "%CYGWIN_INSTALLDIR_CFMT%\build\makecoq_mingw.sh" || GOTO ErrorExit ECHO ========== FINISHED ========== @@ -411,12 +439,13 @@ ECHO ========== BATCH FUNCTIONS ========== 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 -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 -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( @@ -426,9 +455,9 @@ ECHO ========== BATCH FUNCTIONS ========== ECHO -ocaml = %INSTALLOCAML% ECHO -installer= %MAKEINSTALLER% ECHO -make = %INSTALLMAKE% - ECHO -destcyg = %DESTCYG% - ECHO -destcoq = %DESTCOQ% - ECHO -setup = %SETUP% + ECHO -destcyg = %DESTCYG% + ECHO -destcoq = %DESTCOQ% + ECHO -setup = %SETUP% ECHO -proxy = %PROXY% ECHO -cygrepo = %CYGWIN_REPOSITORY% ECHO -cygcache = %CYGWIN_LOCAL_CACHE_WFMT% @@ -438,8 +467,22 @@ ECHO ========== BATCH FUNCTIONS ========== 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 -:Error -ECHO Building Coq failed with error code %errorlevel% -EXIT /b %errorlevel% +:ErrorExit + ECHO ERROR MakeCoq_MinGW.bat failed + EXIT /b 1 |