Windows packaging build with Gitlab CI

We use a specific runner on Inria CloudStack. This allows us to have the
same build infrastructure setup for signed and unsigned binary packages.
The main Coq repository on Gitlab will produce unsigned binaries, using
a runner without secret. On my repository, a one-click operation will
sign the packages, making this part of the release process smoother.

.gitlab-ci.yml

@@ -134,6 +134,24 @@ before_script:
     OPAM_SWITCH: "edge"
     OPAM_VARIANT: "+flambda"
 
+.windows-template: &windows-template
+  stage: test
+  artifacts:
+    name: "%CI_JOB_NAME%"
+    paths:
+      - dev\nsis\*.exe
+      - coq-opensource-archive-windows-*.zip
+    expire_in: 1 week
+  dependencies: []
+  tags:
+    - windows
+  before_script: []
+  script:
+    - call dev/ci/gitlab.bat
+  only:
+    variables:
+      - $WINDOWS == "enabled"
+
 build:base:
   <<: *build-template
   variables:
@@ -160,6 +178,16 @@ build:edge+flambda:
     COQ_EXTRA_CONF: "-native-compiler no -coqide opt -flambda-opts "
     COQ_EXTRA_CONF_QUOTE: "-O3 -unbox-closures"
 
+windows64:
+  <<: *windows-template
+  variables:
+    ARCH: "64"
+
+windows32:
+  <<: *windows-template
+  variables:
+    ARCH: "32"
+
 warnings:base:
   <<: *warnings-template
 

dev/build/windows/makecoq_mingw.sh

@@ -970,6 +970,10 @@ function make_lablgtk {
     # These changes are included in dev/build/windows/patches_coq/lablgtk-2.18.3.patch
 
     log2 make world
+
+    # lablgtk does not escape FINDLIBDIR path, which can contain backslashes
+    sed -i "s|^FINDLIBDIR=.*|FINDLIBDIR=$PREFIXOCAML/libocaml/site-lib|" config.make
+
     log2 make install
     log2 make clean
     build_post

dev/ci/gitlab.bat

@@ -0,0 +1,50 @@
+@ECHO OFF
+
+REM This script builds and signs the Windows packages on Gitlab
+
+if %ARCH% == 32 (
+  SET ARCHLONG=i686
+  SET CYGROOT=C:\cygwin
+  SET SETUP=setup-x86.exe
+)
+
+if %ARCH% == 64 (
+  SET ARCHLONG=x86_64
+  SET CYGROOT=C:\cygwin64
+  SET SETUP=setup-x86_64.exe
+)
+
+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 DESTCOQ=C:\coq%ARCH%_inst
+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 -make=N ^
+  -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorExit
+
+copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit
+7z a coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit
+
+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
+  )
+)
+
+GOTO :EOF
+
+:ErrorExit
+  ECHO ERROR %0 failed
+  EXIT /b 1