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/build') 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/build') 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/build') 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/build') 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/build') 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/build') 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 -------- 1 file changed, 8 deletions(-) delete mode 100644 dev/build/windows/appveyor.sh (limited to 'dev/build') 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 -- cgit v1.2.3