From 4e7d1a239fe325ca938db6144f77cdabd974ac17 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 19 Jul 2017 17:13:33 +0200
Subject: In regression test mode, run cygwin setup to install dependencies.

---
 dev/build/windows/MakeCoq_MinGW.bat | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'dev')

diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
index b2efe2ddd4..a420b5d8bb 100644
--- a/dev/build/windows/MakeCoq_MinGW.bat
+++ b/dev/build/windows/MakeCoq_MinGW.bat
@@ -344,6 +344,9 @@ IF EXIST "%CYGWIN_INSTALLDIR_WFMT%\etc\setup\installed.db" (
 IF NOT "%CYGWIN_QUIET%" == "Y" (
   SET RUNSETUP=Y
 )
+IF "%COQREGTESTING%" == "Y" (
+  SET RUNSETUP=Y
+)
 
 IF "%RUNSETUP%"=="Y" (
   %SETUP% ^
-- 
cgit v1.2.3


From 843df88cd5b30d7c5ff744735baaea2c5a03a1c5 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 19 Jul 2017 17:59:38 +0200
Subject: Print Coq build output.

---
 dev/build/windows/makecoq_mingw.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index e179239514..45a5a5a4f4 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1134,7 +1134,7 @@ function make_coq {
     if [[ $COQ_VERSION == 8.4* ]] ; then
       log1 make
     else
-      log1 make $MAKE_OPT
+      make $MAKE_OPT
     fi
     
     if [ "$INSTALLMODE" == "relocatable" ]; then
-- 
cgit v1.2.3


From 8ac880bee5611a0a408158ff021277c6157eccce Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 20 Jul 2017 15:01:47 +0200
Subject: Print more of the Coq build output.

---
 dev/build/windows/makecoq_mingw.sh | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'dev')

diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 45a5a5a4f4..9507fe79b4 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1119,11 +1119,11 @@ function make_coq {
   then
     if [ "$INSTALLMODE" == "relocatable" ]; then
       # HACK: for relocatable builds, first configure with ./, then build but before install reconfigure with the real target path
-      logn configure ./configure -debug -with-doc no -prefix ./ -libdir ./lib -mandir ./man
+      ./configure -debug -with-doc no -prefix ./ -libdir ./lib -mandir ./man
     elif [ "$INSTALLMODE" == "absolute" ]; then
-      logn configure ./configure -debug -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man"
+      ./configure -debug -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man"
     else
-      logn configure ./configure -debug -with-doc no -prefix "$PREFIXCOQ"
+      ./configure -debug -with-doc no -prefix "$PREFIXCOQ"
     fi
 
     # The windows resource compiler binary name is hard coded
@@ -1138,13 +1138,13 @@ function make_coq {
     fi
     
     if [ "$INSTALLMODE" == "relocatable" ]; then
-      logn reconfigure ./configure -debug -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man"
+      ./configure -debug -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man"
     fi
 
-    log2 make install
-    log1 copy_coq_dlls
+    make install
+    copy_coq_dlls
     if [ "$INSTALLOCAML" == "Y" ]; then
-      log1 copy_coq_objects
+      copy_coq_objects
     fi
     
     copq_coq_gtk
-- 
cgit v1.2.3


From ccf33e7aed7f6c8cdfa6ec6ebb6b5f094ed6989f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 21 Jul 2017 08:36:27 +0200
Subject: Adapt Windows build script to new CoqIDE data installation directory.

---
 dev/build/windows/makecoq_mingw.sh | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

(limited to 'dev')

diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 9507fe79b4..5352b1dce1 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1058,13 +1058,18 @@ function copq_coq_gtk {
     install_rec  "$PREFIX/share/themes/" '*'                          "$PREFIXCOQ/share/themes"
     
     # This below item look like a bug in make install
+    if [ -d "$PREFIXCOQ/share/coq/" ] ; then
+      COQSHARE="$PREFIXCOQ/share/coq/"
+    else
+      COQSHARE="$PREFIXCOQ/share/"
+    fi
     if [[ ! $COQ_VERSION == 8.4* ]] ; then
-      mv "$PREFIXCOQ/share/coq/"*.lang "$PREFIXCOQ/share/gtksourceview-2.0/language-specs"
-      mv "$PREFIXCOQ/share/coq/"*.xml  "$PREFIXCOQ/share/gtksourceview-2.0/styles"
+      mv "$COQSHARE"*.lang "$PREFIXCOQ/share/gtksourceview-2.0/language-specs"
+      mv "$COQSHARE"*.xml  "$PREFIXCOQ/share/gtksourceview-2.0/styles"
     fi
     mkdir -p "$PREFIXCOQ/ide"
-    mv "$PREFIXCOQ/share/coq/"*.png  "$PREFIXCOQ/ide"
-    rmdir "$PREFIXCOQ/share/coq"
+    mv "$COQSHARE"*.png  "$PREFIXCOQ/ide"
+    rmdir "$PREFIXCOQ/share/coq" || true
   fi
 }
 
-- 
cgit v1.2.3


From 802af9272442815012532818cffb6908ad5707e1 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 25 Jul 2017 11:26:33 +0200
Subject: Get sources of cygwin packages after building the installer.

---
 dev/build/windows/makecoq_mingw.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 5352b1dce1..fd5f47d0fa 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1272,7 +1272,7 @@ function get_cygwin_mingw_sources {
 function make_coq_installer {
   make_coq
   make_mingw_make
-  # get_cygwin_mingw_sources
+  get_cygwin_mingw_sources
 
   # Prepare the file lists for the installer. We created to file list dumps of the target folder during the build:
   # ocaml: ocaml + menhir + camlp5 + findlib
-- 
cgit v1.2.3


From df7f4445e73d7b47a3964fa477c533e6084eaa6f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 4 Sep 2017 16:11:14 +0200
Subject: Remove -debug option from Windows build script.

It is no longer accepted by Coq's ./configure.
---
 dev/build/windows/makecoq_mingw.sh | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'dev')

diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index fd5f47d0fa..f3e4cec0b9 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1124,11 +1124,11 @@ function make_coq {
   then
     if [ "$INSTALLMODE" == "relocatable" ]; then
       # HACK: for relocatable builds, first configure with ./, then build but before install reconfigure with the real target path
-      ./configure -debug -with-doc no -prefix ./ -libdir ./lib -mandir ./man
+      ./configure -with-doc no -prefix ./ -libdir ./lib -mandir ./man
     elif [ "$INSTALLMODE" == "absolute" ]; then
-      ./configure -debug -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man"
+      ./configure -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man"
     else
-      ./configure -debug -with-doc no -prefix "$PREFIXCOQ"
+      ./configure -with-doc no -prefix "$PREFIXCOQ"
     fi
 
     # The windows resource compiler binary name is hard coded
@@ -1143,7 +1143,7 @@ function make_coq {
     fi
     
     if [ "$INSTALLMODE" == "relocatable" ]; then
-      ./configure -debug -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man"
+      ./configure -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man"
     fi
 
     make install
-- 
cgit v1.2.3


From 2fee07f74a89dcdf526260934acd36ee71c9ccfa Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 19 Jul 2017 15:47:13 +0200
Subject: Make AppVeyor generate Windows package.

---
 dev/build/windows/appveyor.sh |  8 --------
 dev/ci/appveyor.bat           | 35 +++++++++++++++++++++++++++++++++++
 dev/ci/appveyor.sh            |  9 +++++++++
 3 files changed, 44 insertions(+), 8 deletions(-)
 delete mode 100644 dev/build/windows/appveyor.sh
 create mode 100644 dev/ci/appveyor.bat
 create mode 100644 dev/ci/appveyor.sh

(limited to 'dev')

diff --git a/dev/build/windows/appveyor.sh b/dev/build/windows/appveyor.sh
deleted file mode 100644
index 53f7a23466..0000000000
--- a/dev/build/windows/appveyor.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-#!/bin/bash
-set -e -x
-wget $opam_url
-tar -xf opam64.tar.xz
-bash opam64/install.sh
-opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp 4.02.3+mingw64c --switch 4.02.3+mingw64c
-eval $(opam config env)
-opam install -y ocamlfind camlp5
diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat
new file mode 100644
index 0000000000..ca6a5643c1
--- /dev/null
+++ b/dev/ci/appveyor.bat
@@ -0,0 +1,35 @@
+REM This script either runs the test suite with OPAM (if USEOPAM is true) or
+REM builds the Coq binary packages for windows (if USEOPAM is false).
+
+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
+)
+
+SET CYGCACHE=%CYGROOT%\var\cache\setup
+SET APPVEYOR_BUILD_FOLDER_MFMT=%APPVEYOR_BUILD_FOLDER:\=/%
+SET APPVEYOR_BUILD_FOLDER_CFMT=%APPVEYOR_BUILD_FOLDER_MFMT:C:/=/cygdrive/c/%
+SET DESTCOQ=C:\coq%ARCH%_inst
+SET COQREGTESTING=Y
+
+if %USEOPAM% == false (
+  call %APPVEYOR_BUILD_FOLDER%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
+    -arch=%ARCH% -installer=Y -coqver=%APPVEYOR_BUILD_FOLDER_CFMT% ^
+    -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
+    -setup %CYGROOT%\%SETUP%
+  copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis
+  7z a coq-opensource-archive-%ARCHLONG%.zip %CYGROOT%\build\tarballs\*
+)
+
+if %USEOPAM% == true (
+  %CYGROOT%\%SETUP% -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% ^
+    -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time
+  %CYGROOT%/bin/bash -l %APPVEYOR_BUILD_FOLDER%/dev/ci/appveyor.sh
+)
diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh
new file mode 100644
index 0000000000..524a55a423
--- /dev/null
+++ b/dev/ci/appveyor.sh
@@ -0,0 +1,9 @@
+#!/bin/bash
+set -e -x
+wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.1/opam64.tar.xz
+tar -xf opam64.tar.xz
+bash opam64/install.sh
+opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp 4.02.3+mingw64c --switch 4.02.3+mingw64c
+eval $(opam config env)
+opam install -y ocamlfind camlp5
+cd $APPVEYOR_BUILD_FOLDER && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= && make validate
-- 
cgit v1.2.3