summaryrefslogtreecommitdiff
path: root/dev/build
diff options
context:
space:
mode:
Diffstat (limited to 'dev/build')
-rwxr-xr-xdev/build/osx/make-macos-dmg.sh54
-rwxr-xr-xdev/build/windows/MakeCoq_MinGW.bat976
-rw-r--r--dev/build/windows/configure_profile.sh24
-rw-r--r--dev/build/windows/difftar-folder.sh22
-rwxr-xr-xdev/build/windows/makecoq_mingw.sh84
-rwxr-xr-xdev/build/windows/patches_coq/VST.patch15
-rw-r--r--dev/build/windows/patches_coq/aactactis-86ac28259030649ef51460e4de2441c8a1017751.patch21
-rwxr-xr-x[-rw-r--r--]dev/build/windows/patches_coq/quickchick.patch (renamed from dev/build/windows/patches_coq/quickchick-v1.0.2.patch)12
8 files changed, 635 insertions, 573 deletions
diff --git a/dev/build/osx/make-macos-dmg.sh b/dev/build/osx/make-macos-dmg.sh
index dc33838f..9b08f517 100755
--- a/dev/build/osx/make-macos-dmg.sh
+++ b/dev/build/osx/make-macos-dmg.sh
@@ -3,26 +3,68 @@
# Fail on first error
set -e
+# TODO use Docker instead of this
+brew update
+brew unlink python
+brew install opam gnu-time gtk+ expat gtksourceview gdk-pixbuf
+brew unlink python@2
+brew link python3
+pip3 install macpack
+opam init -a -y -j 2 --compiler=ocaml-base-compiler.4.07.1 default https://opam.ocaml.org
+opam switch ocaml-base-compiler.4.07.1
+eval $(opam config env)
+opam update
+opam config list
+opam list
+opam install -j 2 -y camlp5 ocamlfind.1.8.0 num lablgtk.2.18.6 conf-gtksourceview.2
+rm -rf ~/.opam/log/
+opam list
+
# Configuration setup
OUTDIR=$PWD/_install
DMGDIR=$PWD/_dmg
VERSION=$(sed -n -e '/^let coq_version/ s/^[^"]*"\([^"]*\)"$/\1/p' configure.ml)
APP=bin/CoqIDE_${VERSION}.app
+make clean
+./configure -native-compiler no -coqide opt -prefix "$OUTDIR"
+make -j "$NJOBS" byte
+make -j "$NJOBS" world
+make test-suite/misc/universes/all_stdlib.v
+make -j "$NJOBS" world
+make install
+make install-byte
+
# Create a .app file with CoqIDE, without signing it
-make PRIVATEBINARIES=$APP -j $NJOBS -l2 $APP
+make PRIVATEBINARIES="$APP" -j "$NJOBS" -l2 "$APP"
# Add Coq to the .app file
-make OLDROOT=$OUTDIR COQINSTALLPREFIX=$APP/Contents/Resources/ install-coq install-ide-toploop
+make OLDROOT="$OUTDIR" COQINSTALLPREFIX="$APP/Contents/Resources/" install-coq install-ide-toploop
+
+if [ -n "$MACOS_CERTIFICATE_IDENTITY" ] && [ -n "$MACOS_CERTIFICATE_PASSWORD" ] && [ -n "$MACOS_CERTIFICATE_BASE_PATH" ]
+then
+ readonly KEYCHAIN=macos-build.keychain
+ # This pile of hacks is required to avoid having to manually validate access to the key through UI
+ security create-keychain -p gitlab "${KEYCHAIN}"
+ security default-keychain -s "${KEYCHAIN}"
+ security unlock-keychain -p gitlab "${KEYCHAIN}"
+ security set-keychain-settings -t 3600 -u "${KEYCHAIN}"
+ security import "${MACOS_CERTIFICATE_BASE_PATH}/foundation.cer" -k ~/Library/Keychains/"${KEYCHAIN}" -T /usr/bin/codesign
+ security import "${MACOS_CERTIFICATE_BASE_PATH}/foundation.p12" -k ~/Library/Keychains/"${KEYCHAIN}" -P "${MACOS_CERTIFICATE_PASSWORD}" -T /usr/bin/codesign
+ security set-key-partition-list -S apple-tool:,apple: -s -k gitlab ~/Library/Keychains/"${KEYCHAIN}"
+ codesign -f -v -s "$MACOS_CERTIFICATE_IDENTITY" "$APP"
+ security default-keychain -s "login.keychain"
+ security delete-keychain "${KEYCHAIN}"
+fi
# Create the dmg bundle
-mkdir -p $DMGDIR
-ln -sf /Applications $DMGDIR/Applications
-cp -r $APP $DMGDIR
+mkdir -p "$DMGDIR"
+ln -sf /Applications "$DMGDIR/Applications"
+cp -r "$APP" "$DMGDIR"
mkdir -p _build
# Temporary countermeasure to hdiutil error 5341
# head -c9703424 /dev/urandom > $DMGDIR/.padding
-hdiutil create -imagekey zlib-level=9 -volname coq-$VERSION-installer-macos -srcfolder $DMGDIR -ov -format UDZO _build/coq-$VERSION-installer-macos.dmg
+hdiutil create -imagekey zlib-level=9 -volname "coq-$VERSION-installer-macos" -srcfolder "$DMGDIR" -ov -format UDZO "_build/coq-$VERSION-installer-macos.dmg"
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
index 61cf6bc4..8489bcfc 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://mirror.easyname.at/cygwin
+
+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/configure_profile.sh b/dev/build/windows/configure_profile.sh
index 16c972e8..7e606b55 100644
--- a/dev/build/windows/configure_profile.sh
+++ b/dev/build/windows/configure_profile.sh
@@ -14,30 +14,30 @@
rcfile=~/.bash_profile
donefile=~/.bash_profile.upated
+# to learn about `exec >> $file`, see https://www.tldp.org/LDP/abs/html/x17974.html
+exec >> $rcfile
+
if [ ! -f $donefile ] ; then
- echo >> $rcfile
-
- if [ "$1" != "" -a "$1" != " " ]; then
- echo export http_proxy="http://$1" >> $rcfile
- echo export https_proxy="http://$1" >> $rcfile
- echo export ftp_proxy="http://$1" >> $rcfile
+ if [ "$1" != "" ] && [ "$1" != " " ]; then
+ echo export http_proxy="http://$1"
+ echo export https_proxy="http://$1"
+ echo export ftp_proxy="http://$1"
fi
-
- mkdir -p $RESULT_INSTALLDIR_CFMT/bin
+
+ mkdir -p "$RESULT_INSTALLDIR_CFMT/bin"
# A tightly controlled path helps to avoid issues
# Note: the order is important: first have the cygwin binaries, then the mingw binaries in the path!
# Note: /bin is mounted at /usr/bin and /lib at /usr/lib and it is common to use /usr/bin in PATH
# See cat /proc/mounts
- echo "export PATH=/usr/local/bin:/usr/bin:$RESULT_INSTALLDIR_CFMT/bin:/usr/$TARGET_ARCH/sys-root/mingw/bin:/cygdrive/c/Windows/system32:/cygdrive/c/Windows" >> $rcfile
+ echo "export PATH=/usr/local/bin:/usr/bin:$RESULT_INSTALLDIR_CFMT/bin:/usr/$TARGET_ARCH/sys-root/mingw/bin:/cygdrive/c/Windows/system32:/cygdrive/c/Windows"
# find and xargs complain if the environment is larger than (I think) 8k.
# ORIGINAL_PATH (set by cygwin) can be a few k and exceed the limit
- echo unset ORIGINAL_PATH >> $rcfile
-
+ echo unset ORIGINAL_PATH
# Other installations of OCaml will mess up things
- echo unset OCAMLLIB >> $rcfile
+ echo unset OCAMLLIB
touch $donefile
fi
diff --git a/dev/build/windows/difftar-folder.sh b/dev/build/windows/difftar-folder.sh
index cbcf14ec..3bba451e 100644
--- a/dev/build/windows/difftar-folder.sh
+++ b/dev/build/windows/difftar-folder.sh
@@ -42,7 +42,7 @@ fi
if [ "$strip" -gt 0 ] ; then
# Get the path/name of the first file from teh tar and extract the first $strip path components
# This assumes that the first file in the tar file has at least $strip many path components
- prefix=$(tar -t -f $tarfile | head -1 | cut -d / -f -$strip)/
+ prefix=$(tar -t -f "$tarfile" | head -1 | cut -d / -f -$strip)/
else
prefix=
fi
@@ -60,13 +60,13 @@ mkdir -p "$empty"
# Print information (this is ignored by patch)
-echo diff/patch file created on $(date) with:
-echo difftar-folder.sh $@
-echo TARFILE= $tarfile
-echo FOLDER= $folder
-echo TARSTRIP= $strip
-echo TARPREFIX= $prefix
-echo ORIGFOLDER= $orig
+echo diff/patch file created on "$(date)" with:
+echo difftar-folder.sh "$@"
+echo TARFILE= "$tarfile"
+echo FOLDER= "$folder"
+echo TARSTRIP= "$strip"
+echo TARPREFIX= "$prefix"
+echo ORIGFOLDER= "$orig"
# Make sure tar uses english output (for Mod time differs)
export LC_ALL=C
@@ -76,14 +76,14 @@ tar --diff -a -f "$tarfile" --strip $strip --directory "$folder" | grep "Mod tim
# Substitute ': Mod time differs' with nothing
file=${file/: Mod time differs/}
# Check if file exists
- if [ -f "$folder/$file" ] ; then
+ if [ -f "$folder/$file" ] ; then
# Extract original file
tar -x -a -f "$tarfile" --strip $strip --directory "$orig" "$prefix$file"
# Compute diff
- diff -u "$orig/$file" "$folder/$file"
+ diff -u "$orig/$file" "$folder/$file"
fi
done
if [ -d "$new" ] ; then
- diff -u -r --unidirectional-new-file $empty $new
+ diff -u -r --unidirectional-new-file "$empty" "$new"
fi
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 86cc5f2d..070af6b4 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -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,12 @@ 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=
@@ -368,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"
@@ -409,7 +426,7 @@ function build_prep_overlay {
# $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"
+ build_prep "$url" "$ver" tar.gz 1 "$1-$ver" "$1"
}
# ------------------------------------------------------------------------------
@@ -666,6 +683,17 @@ function installer_addon_end {
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/g'
+}
+
###################### MODULE BUILD FUNCTIONS #####################
##### SED #####
@@ -1343,11 +1371,10 @@ function copy_coq_license {
install -D doc/LICENSE "$PREFIXCOQ/license_readme/coq/LicenseDoc.txt"
install -D LICENSE "$PREFIXCOQ/license_readme/coq/License.txt"
install -D plugins/micromega/LICENSE.sos "$PREFIXCOQ/license_readme/coq/LicenseMicromega.txt"
- install -D README "$PREFIXCOQ/license_readme/coq/ReadMe.txt" || true
- install -D README.md "$PREFIXCOQ/license_readme/coq/ReadMe.md" || true
- install -D README.win "$PREFIXCOQ/license_readme/coq/ReadMeWindows.txt" || true
- install -D README.doc "$PREFIXCOQ/license_readme/coq/ReadMeDoc.txt" || true
- install -D CHANGES "$PREFIXCOQ/license_readme/coq/Changes.txt"
+ # 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.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
@@ -1620,7 +1647,7 @@ 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 autmatically saved/restored by build_prep / build_post
+ # 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
@@ -1668,7 +1695,7 @@ function make_addon_ssreflect {
function make_addon_ltac2 {
installer_addon_dependency ltac2
if build_prep_overlay ltac2; then
- installer_addon_section ltac2 "Ltac-2" "Coq plugin with the Ltac-2 enhanced tactics language" ""
+ installer_addon_section ltac2 "Ltac-2" "Coq plugin with the Ltac-2 enhanced tactic language" ""
log1 make all
log2 make install
build_post
@@ -1680,6 +1707,7 @@ function make_addon_ltac2 {
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
@@ -1694,6 +1722,7 @@ function make_addon_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
@@ -1778,8 +1807,8 @@ function install_addon_vst {
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_glob "veric" '*.v' "$VSTDEST/veric/"
+ install_glob "veric" '*.vo' "$VSTDEST/veric/"
# Install VST documentation files
install_glob "." 'LICENSE' "$VSTDEST"
@@ -1792,11 +1821,20 @@ function install_addon_vst {
install_glob "." '_CoqProject-export' "$VSTDEST/progs"
}
+function vst_patch_compcert_refs {
+ find . -type f -name '*.v' -print0 | xargs -0 sed -E -i \
+ -e 's/(Require\s+(Import\s+|Export\s+)*)compcert\./\1VST.compcert./g' \
+ -e 's/From compcert Require/From VST.compcert Require/g'
+}
+
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 make IGNORECOQVERSION=true $MAKE_OPT
+ # log1 coq_set_timeouts_1000
+ log1 vst_patch_compcert_refs
+ # The usage of the shell variable ARCH in VST collides with the usage in this shellscript
+ logn make env -u ARCH make IGNORECOQVERSION=true $MAKE_OPT
log1 install_addon_vst
build_post
fi
diff --git a/dev/build/windows/patches_coq/VST.patch b/dev/build/windows/patches_coq/VST.patch
new file mode 100755
index 00000000..2c8c4637
--- /dev/null
+++ b/dev/build/windows/patches_coq/VST.patch
@@ -0,0 +1,15 @@
+diff --git a/Makefile b/Makefile
+index 4a119042..fdfac13e 100755
+--- a/Makefile
++++ b/Makefile
+@@ -76,8 +76,8 @@ endif
+
+ COMPCERTDIRS=lib common $(ARCHDIRS) cfrontend flocq exportclight $(BACKEND)
+
+-COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT)/$(d) compcert.$(d))
+-EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT)/$(d) compcert.$(d))
++COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT)/$(d) VST.compcert.$(d))
++EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT)/$(d) VST.compcert.$(d))
+
+ # for SSReflect
+ ifdef MATHCOMP
diff --git a/dev/build/windows/patches_coq/aactactis-86ac28259030649ef51460e4de2441c8a1017751.patch b/dev/build/windows/patches_coq/aactactis-86ac28259030649ef51460e4de2441c8a1017751.patch
deleted file mode 100644
index d9b134b2..00000000
--- a/dev/build/windows/patches_coq/aactactis-86ac28259030649ef51460e4de2441c8a1017751.patch
+++ /dev/null
@@ -1,21 +0,0 @@
---- aac-tactics-v8.8.orig\Tutorial.v 2018-05-30 16:09:06.000000000 +0200
-+++ aac-tactics-v8.8\Tutorial.v 2018-08-24 19:47:25.000000000 +0200
-@@ -9,16 +9,14 @@
- (** * Tutorial for using the [aac_tactics] library.
-
- Depending on your installation, either modify the following two
- lines, or add them to your .coqrc files, replacing "." with the
- path to the [aac_tactics] library. *)
-
--Add Rec LoadPath "." as AAC_tactics.
--Add ML Path ".".
--Require Import AAC.
--Require Instances.
-+Require Import AAC_tactics.AAC.
-+Require AAC_tactics.Instances.
- Require Arith ZArith.
-
- (** ** Introductory example
-
- Here is a first example with relative numbers ([Z]): one can
- rewrite an universally quantified hypothesis modulo the
diff --git a/dev/build/windows/patches_coq/quickchick-v1.0.2.patch b/dev/build/windows/patches_coq/quickchick.patch
index d03749ba..1afa6e7f 100644..100755
--- a/dev/build/windows/patches_coq/quickchick-v1.0.2.patch
+++ b/dev/build/windows/patches_coq/quickchick.patch
@@ -24,15 +24,3 @@ ORIGFOLDER= quickchick-v1.0.2.orig
+ $(V)cp $(QCTOOL_EXE) "$(COQBIN)/quickChick"
# $(V)cp src/quickChickLib.cmx $(COQLIB)/user-contrib/QuickChick
# $(V)cp src/quickChickLib.o $(COQLIB)/user-contrib/QuickChick
-
---- quickchick-v1.0.2.orig/src/Show.v 2018-08-22 18:21:39.000000000 +0200
-+++ quickchick-v1.0.2/src/Show.v 2018-08-27 09:21:35.893961900 +0200
-@@ -228,7 +228,7 @@
- match s with
- | EmptyString => (if b then ")" else "", b)
- | String a s =>
-- let (s', b) := aux s (orb b (nat_of_ascii a =? 32)) in
-+ let (s', b) := aux s (orb b (nat_of_ascii a =? 32)%nat) in
- (String a s', b)
- end in
- let (s', b) := aux s false in
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 10:21:41 +0000