diff options
Diffstat (limited to 'dev/build/windows')
| -rwxr-xr-x[-rw-r--r--] | dev/build/windows/MakeCoq_MinGW.bat | 8 | ||||
| -rw-r--r-- | dev/build/windows/makecoq_mingw.sh | 36 |
2 files changed, 42 insertions, 2 deletions
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index f960ff008..5af0fcff3 100644..100755 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -255,6 +255,7 @@ IF NOT "%~0" == "" ( 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 ) @@ -385,7 +386,6 @@ IF "%RUNSETUP%"=="Y" ( 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. @@ -396,6 +396,12 @@ IF NOT "%CYGWIN_QUIET%" == "Y" ( 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 diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 508dcf5fb..4fabf3161 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -118,6 +118,9 @@ mkdir -p "$PREFIX/bin" mkdir -p "$PREFIXCOQ/bin" mkdir -p "$PREFIXOCAML/bin" +# This is required for building addons and plugins +export COQBIN=$RESULT_INSTALLDIR_CFMT/bin/ + ###################### Copy Cygwin Setup Info ##################### # Copy Cygwin repo ini file and installed files db to tarballs folder. @@ -1211,6 +1214,9 @@ function make_coq { # 2.) clean of test suites fails with "cannot run complexity tests (no bogomips found)" # make clean + # Copy plugin version files somewhere, where the plugin builds can find them + cp -r dev/build/plugin-versions /build/ + build_post fi } @@ -1378,8 +1384,11 @@ function make_coq_installer { ###################### ADDONS ##################### +# The bignums library +# Provides BigN, BigZ, BigQ that used to be part of Coq standard library + function make_addon_bignums { - if build_prep https://github.com/coq/bignums/archive/ V8.8+beta1 zip 1 bignums-8.8+beta1; then + if build_prep $(/build/plugin-versions/bignums.sh "$COQ_VERSION"); then # To make command lines shorter :-( echo 'COQ_SRC_SUBDIRS:=$(filter-out plugins/%,$(COQ_SRC_SUBDIRS)) plugins/syntax' >> Makefile.coq.local log1 make all @@ -1388,6 +1397,31 @@ function make_addon_bignums { fi } +# Ltac-2 plugin +# A new (experimental) tactic language + +function make_addon_ltac2 { + if build_prep $(/build/plugin-versions/ltac2.sh "$COQ_VERSION"); then + log1 make all + log2 make install + build_post + fi +} + +# Equations plugin +# A function definition plugin + +function make_addon_equations { + if build_prep $(/build/plugin-versions/equations.sh "$COQ_VERSION"); 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 + log1 make + log2 make install + build_post + fi +} + function make_addons { for addon in $COQ_ADDONS; do "make_addon_$addon" |