diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /dev/build | |
parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) |
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'dev/build')
-rwxr-xr-x | dev/build/osx/make-macos-dmg.sh | 54 | ||||
-rwxr-xr-x | dev/build/windows/MakeCoq_MinGW.bat | 976 | ||||
-rw-r--r-- | dev/build/windows/configure_profile.sh | 24 | ||||
-rw-r--r-- | dev/build/windows/difftar-folder.sh | 22 | ||||
-rwxr-xr-x | dev/build/windows/makecoq_mingw.sh | 84 | ||||
-rwxr-xr-x | dev/build/windows/patches_coq/VST.patch | 15 | ||||
-rw-r--r-- | dev/build/windows/patches_coq/aactactis-86ac28259030649ef51460e4de2441c8a1017751.patch | 21 | ||||
-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 |