aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/build
diff options
context:
space:
mode:
Diffstat (limited to 'dev/build')
-rwxr-xr-xdev/build/windows/MakeCoq_88git_installer.bat27
-rw-r--r--dev/build/windows/MakeCoq_MinGW.bat3
-rw-r--r--dev/build/windows/makecoq_mingw.sh12
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
}