diff options
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/docker/bionic_coq/Dockerfile | 14 | ||||
| -rwxr-xr-x | dev/ci/gitlab.bat | 240 |
2 files changed, 126 insertions, 128 deletions
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 8d0f69626e..fcfa591ce1 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-09-24-V01" +# CACHEKEY: "bionic_coq-V2018-09-25-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -32,33 +32,31 @@ ENV NJOBS="2" \ OPAMYES="true" # Base opam is the set of base packages required by Coq -ENV COMPILER="4.02.3" +ENV COMPILER="4.05.0" # Common OPAM packages. # `num` does not have a version number as the right version to install varies # with the compiler version. -ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8" \ +ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8 odoc.1.2.0" \ CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. -ENV CAMLP5_VER="6.14" \ +ENV CAMLP5_VER="7.01" \ COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2" -# The separate `opam install ocamlfind` workarounds an OPAM repository bug in 4.02.3 +# base switch RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \ - opam install ocamlfind.1.8.0 && \ opam install $BASE_OPAM camlp5.$CAMLP5_VER $COQIDE_OPAM $CI_OPAM # base+32bit switch RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ - opam install ocamlfind.1.8.0 && \ opam install $BASE_OPAM camlp5.$CAMLP5_VER # EDGE switch ENV COMPILER_EDGE="4.07.0" \ CAMLP5_VER_EDGE="7.06" \ COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \ - BASE_OPAM_EDGE="odoc.1.2.0 dune-release.0.3.0" + BASE_OPAM_EDGE="dune-release.0.3.0" RUN opam switch create $COMPILER_EDGE && eval $(opam env) && \ opam install $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat index a848c49d75..09e9762261 100755 --- a/dev/ci/gitlab.bat +++ b/dev/ci/gitlab.bat @@ -1,120 +1,120 @@ -@ECHO OFF - -REM This script builds and signs the Windows packages on Gitlab - -ECHO "Start Time" -TIME /T - -REM List currently used cygwin and target folders for debugging / maintenance purposes - -ECHO "Currently used cygwin folders" -DIR C:\ci\cygwin* -ECHO "Currently used target folders" -DIR C:\ci\coq* -ECHO "Root folders" -DIR C:\ - -if %ARCH% == 32 ( - SET ARCHLONG=i686 - SET SETUP=setup-x86.exe -) - -if %ARCH% == 64 ( - SET ARCHLONG=x86_64 - SET SETUP=setup-x86_64.exe -) - -SET CYGROOT=C:\ci\cygwin%ARCH% -SET DESTCOQ=C:\ci\coq%ARCH% - -CALL :MakeUniqueFolder %CYGROOT% CYGROOT -CALL :MakeUniqueFolder %DESTCOQ% DESTCOQ - -powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/%SETUP%', '%SETUP%')" -SET CYGCACHE=%CYGROOT%\var\cache\setup -SET CI_PROJECT_DIR_MFMT=%CI_PROJECT_DIR:\=/% -SET CI_PROJECT_DIR_CFMT=%CI_PROJECT_DIR_MFMT:C:/=/cygdrive/c/% -SET COQREGTESTING=Y -SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\v7.1\Bin - -if exist %CYGROOT%\build\ rd /s /q %CYGROOT%\build -if exist %DESTCOQ%\ rd /s /q %DESTCOQ% - -call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^ - -arch=%ARCH% -installer=Y -coqver=%CI_PROJECT_DIR_CFMT% ^ - -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^ - -addon="bignums ltac2 equations" -make=N ^ - -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorCopyLogFilesAndExit - - -ECHO "Start Artifact Creation" -TIME /T - -mkdir artifacts - -CALL :CopyLogFiles - -copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" artifacts || GOTO ErrorExit -REM The open source archive is only required for release builds -IF DEFINED WIN_CERTIFICATE_PATH ( - 7z a artifacts\coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit -) ELSE ( - REM In non release builds, create a dummy file - ECHO "This is not a release build - open source archive not created / uploaded" > artifacts\coq-opensource-info.txt -) - -REM DO NOT echo the signing command below, as this would leak secrets in the logs -IF DEFINED WIN_CERTIFICATE_PATH ( - IF DEFINED WIN_CERTIFICATE_PASSWORD ( - ECHO Signing package - @signtool sign /f %WIN_CERTIFICATE_PATH% /p %WIN_CERTIFICATE_PASSWORD% dev\nsis\*.exe - signtool verify /pa dev\nsis\*.exe - ) -) - -ECHO "Finished Artifact Creation" -TIME /T - -CALL :CleanupFolders - -ECHO "Finished Cleanup" -TIME /T - -GOTO :EOF - -:CopyLogFiles - ECHO Copy log files for artifact upload - MKDIR artifacts\buildlogs - COPY %CYGROOT%\build\buildlogs\* artifacts\buildlogs - MKDIR artifacts\filelists - COPY %CYGROOT%\build\filelists\* artifacts\filelists - MKDIR artifacts\flagfiles - COPY %CYGROOT%\build\flagfiles\* artifacts\flagfiles - GOTO :EOF - -:CleanupFolders - ECHO "Cleaning %CYGROOT%" - RMDIR /S /Q "%CYGROOT%" - ECHO "Cleaning %DESTCOQ%" - RMDIR /S /Q "%DESTCOQ%" - GOTO :EOF - -:MakeUniqueFolder - REM Create a uniquely named folder - REM This script is safe because folder creation is atomic - either we create it or fail - REM %1 = base path or directory (_%RANDOM%_%RANDOM% is appended to this) - REM %2 = name of the variable which receives the unique folder name - SET "UNIQUENAME=%1_%RANDOM%_%RANDOM%" - MKDIR "%UNIQUENAME%" - IF ERRORLEVEL 1 GOTO :MakeUniqueFolder - SET "%2=%UNIQUENAME%" - GOTO :EOF - -:ErrorCopyLogFilesAndExit - CALL :CopyLogFiles - REM fall through - -:ErrorExit - CALL :CleanupFolders - ECHO ERROR %0 failed - EXIT /b 1 +@ECHO OFF
+
+REM This script builds and signs the Windows packages on Gitlab
+
+ECHO "Start Time"
+TIME /T
+
+REM List currently used cygwin and target folders for debugging / maintenance purposes
+
+ECHO "Currently used cygwin folders"
+DIR C:\ci\cygwin*
+ECHO "Currently used target folders"
+DIR C:\ci\coq*
+ECHO "Root folders"
+DIR C:\
+
+if %ARCH% == 32 (
+ SET ARCHLONG=i686
+ SET SETUP=setup-x86.exe
+)
+
+if %ARCH% == 64 (
+ SET ARCHLONG=x86_64
+ SET SETUP=setup-x86_64.exe
+)
+
+SET CYGROOT=C:\ci\cygwin%ARCH%
+SET DESTCOQ=C:\ci\coq%ARCH%
+
+CALL :MakeUniqueFolder %CYGROOT% CYGROOT
+CALL :MakeUniqueFolder %DESTCOQ% DESTCOQ
+
+powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/%SETUP%', '%SETUP%')"
+SET CYGCACHE=%CYGROOT%\var\cache\setup
+SET CI_PROJECT_DIR_MFMT=%CI_PROJECT_DIR:\=/%
+SET CI_PROJECT_DIR_CFMT=%CI_PROJECT_DIR_MFMT:C:/=/cygdrive/c/%
+SET COQREGTESTING=Y
+SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\v7.1\Bin
+
+if exist %CYGROOT%\build\ rd /s /q %CYGROOT%\build
+if exist %DESTCOQ%\ rd /s /q %DESTCOQ%
+
+call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
+ -arch=%ARCH% -installer=Y -coqver=%CI_PROJECT_DIR_CFMT% ^
+ -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
+ -addon="bignums ltac2 equations" -make=N ^
+ -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorCopyLogFilesAndExit
+
+
+ECHO "Start Artifact Creation"
+TIME /T
+
+mkdir artifacts
+
+CALL :CopyLogFiles
+
+copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" artifacts || GOTO ErrorExit
+REM The open source archive is only required for release builds
+IF DEFINED WIN_CERTIFICATE_PATH (
+ 7z a artifacts\coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit
+) ELSE (
+ REM In non release builds, create a dummy file
+ ECHO "This is not a release build - open source archive not created / uploaded" > artifacts\coq-opensource-info.txt
+)
+
+REM DO NOT echo the signing command below, as this would leak secrets in the logs
+IF DEFINED WIN_CERTIFICATE_PATH (
+ IF DEFINED WIN_CERTIFICATE_PASSWORD (
+ ECHO Signing package
+ @signtool sign /f %WIN_CERTIFICATE_PATH% /p %WIN_CERTIFICATE_PASSWORD% dev\nsis\*.exe
+ signtool verify /pa dev\nsis\*.exe
+ )
+)
+
+ECHO "Finished Artifact Creation"
+TIME /T
+
+CALL :CleanupFolders
+
+ECHO "Finished Cleanup"
+TIME /T
+
+GOTO :EOF
+
+:CopyLogFiles
+ ECHO Copy log files for artifact upload
+ MKDIR artifacts\buildlogs
+ COPY %CYGROOT%\build\buildlogs\* artifacts\buildlogs
+ MKDIR artifacts\filelists
+ COPY %CYGROOT%\build\filelists\* artifacts\filelists
+ MKDIR artifacts\flagfiles
+ COPY %CYGROOT%\build\flagfiles\* artifacts\flagfiles
+ GOTO :EOF
+
+:CleanupFolders
+ ECHO "Cleaning %CYGROOT%"
+ RMDIR /S /Q "%CYGROOT%"
+ ECHO "Cleaning %DESTCOQ%"
+ RMDIR /S /Q "%DESTCOQ%"
+ GOTO :EOF
+
+:MakeUniqueFolder
+ REM Create a uniquely named folder
+ REM This script is safe because folder creation is atomic - either we create it or fail
+ REM %1 = base path or directory (_%RANDOM%_%RANDOM% is appended to this)
+ REM %2 = name of the variable which receives the unique folder name
+ SET "UNIQUENAME=%1_%RANDOM%_%RANDOM%"
+ MKDIR "%UNIQUENAME%"
+ IF ERRORLEVEL 1 GOTO :MakeUniqueFolder
+ SET "%2=%UNIQUENAME%"
+ GOTO :EOF
+
+:ErrorCopyLogFilesAndExit
+ CALL :CopyLogFiles
+ REM fall through
+
+:ErrorExit
+ CALL :CleanupFolders
+ ECHO ERROR %0 failed
+ EXIT /b 1
|