From da489b118e2b088d36f798020f6aaffbe4cf4324 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Mon, 23 Apr 2018 14:31:03 +0200
Subject: 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                     | 28 +++++++++++++++++++++
 dev/build/windows/makecoq_mingw.sh |  4 +++
 dev/ci/gitlab.bat                  | 50 ++++++++++++++++++++++++++++++++++++++
 3 files changed, 82 insertions(+)
 create mode 100644 dev/ci/gitlab.bat

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index ac4304da1..bd400f65b 100644
--- a/.gitlab-ci.yml
+++ b/.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
 
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index f4ec218b6..3608f7305 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/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
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
new file mode 100644
index 000000000..70278e6d0
--- /dev/null
+++ b/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
-- 
cgit v1.2.3


From 087e8c4c93c14de6038b79f4bbfd270124af2f11 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Fri, 11 May 2018 09:38:05 +0200
Subject: Remove packaging jobs from appveyor

They are now done on Gitlab CI. The test suite on Windows stays on
Appveyor.
---
 appveyor.yml | 12 ------------
 1 file changed, 12 deletions(-)

diff --git a/appveyor.yml b/appveyor.yml
index 44a93d15d..cd3b88d00 100644
--- a/appveyor.yml
+++ b/appveyor.yml
@@ -10,10 +10,6 @@ image:
 environment:
   CYGMIRROR: http://ftp.inf.tu-dresden.de/software/windows/cygwin32
   matrix:
-  - USEOPAM: false
-    ARCH: 32
-  - USEOPAM: false
-    ARCH: 64
   - USEOPAM: true
     ARCH: 64
 
@@ -21,11 +17,3 @@ build_script:
 - cmd: 'call %APPVEYOR_BUILD_FOLDER%\dev\ci\appveyor.bat'
 
 test: off
-
-artifacts:
-  - path: 'dev\nsis\*.exe'
-    name: installer
-
-  - path: 'coq-opensource-archive-*.zip'
-    name: opensource-archive
-
-- 
cgit v1.2.3