diff options
Diffstat (limited to 'dev/build')
-rwxr-xr-x | dev/build/windows/MakeCoq_88git_installer.bat | 27 | ||||
-rw-r--r-- | dev/build/windows/MakeCoq_MinGW.bat | 3 | ||||
-rw-r--r-- | dev/build/windows/makecoq_mingw.sh | 12 |
3 files changed, 36 insertions, 6 deletions
diff --git a/dev/build/windows/MakeCoq_88git_installer.bat b/dev/build/windows/MakeCoq_88git_installer.bat new file mode 100755 index 000000000..b016fb389 --- /dev/null +++ b/dev/build/windows/MakeCoq_88git_installer.bat @@ -0,0 +1,27 @@ +@ECHO OFF
+
+REM ========== COPYRIGHT/COPYLEFT ==========
+
+REM (C) 2016 Intel Deutschland GmbH
+REM Author: Michael Soegtrop
+
+REM Released to the public by Intel under the
+REM GNU Lesser General Public License Version 2.1 or later
+REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
+
+REM ========== BUILD COQ ==========
+
+call MakeCoq_SetRootPath
+
+call MakeCoq_MinGW.bat ^
+ -arch=64 ^
+ -installer=Y ^
+ -coqver=git-v8.8 ^
+ -destcyg=%ROOTPATH%\cygwin_coq64_88_inst ^
+ -destcoq=%ROOTPATH%\coq64_88_inst ^
+ -addon=bignums
+
+IF %ERRORLEVEL% NEQ 0 (
+ ECHO MakeCoq_88git_installer.bat failed with error code %ERRORLEVEL%
+ EXIT /b %ERRORLEVEL%
+)
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index ccf22cc86..f960ff008 100644 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -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 @@ -267,7 +267,6 @@ IF "%INSTALLMODE%" == "mingwincygwin" ( IF "%MAKEINSTALLER%" == "Y" ( SET INSTALLMODE=relocatable SET INSTALLOCAML=Y - SET INSTALLMAKE=Y ) REM ========== CONFIRM PARAMETERS ========== diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index e5a7b04a1..18f1a2f16 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -142,18 +142,22 @@ LOGS=$(pwd)/buildlogs # The current log target (first part of the log file name) LOGTARGET=other +# Log command output - take log target name from command name (like log1 make => log target is "<module>-make") log1() { "$@" > "$LOGS/$LOGTARGET-$1.log" 2> "$LOGS/$LOGTARGET-$1.err" } +# Log command output - take log target name from command name and first argument (like log2 make install => log target is "<module>-make-install") log2() { "$@" > "$LOGS/$LOGTARGET-$1-$2.log" 2> "$LOGS/$LOGTARGET-$1-$2.err" } +# 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() { "$@" > "$LOGS/$LOGTARGET-$1-$3.log" 2> "$LOGS/$LOGTARGET-$1-$3.err" } +# Log command output - log target name is first argument (like logn untar tar xvaf ... => log target is "<module>-untar") logn() { LOGTARGETEX=$1 shift @@ -1291,7 +1295,6 @@ function get_cygwin_mingw_sources { 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: @@ -1344,12 +1347,13 @@ function make_coq_installer { } ###################### ADDONS ##################### + function make_addon_bignums { - if build_prep https://github.com/coq/bignums/archive/ V8.8+beta1 zip 1; then + if build_prep https://github.com/coq/bignums/archive/ V8.8+beta1 zip 1 bignums-8.8+beta1; then # To make command lines shorter :-( echo 'COQ_SRC_SUBDIRS:=$(filter-out plugins/%,$(COQ_SRC_SUBDIRS)) plugins/syntax' >> Makefile.coq.local - logn make make all - logn make-install make install + log1 make all + log2 make install build_post fi } |