From f4736ec961706fc7cc6ace99089525a2c24e5138 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Feb 2018 18:32:21 +0100 Subject: build: win: support for addons --- dev/build/windows/MakeCoq_MinGW.bat | 13 +++++++++++++ dev/build/windows/ReadMe.txt | 5 +++++ dev/build/windows/makecoq_mingw.sh | 12 ++++++++++++ 3 files changed, 30 insertions(+) (limited to 'dev') diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index 665d541761..ccf22cc866 100644 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -78,6 +78,9 @@ SET GTK_FROM_SOURCES=N REM see -threads in ReadMe.txt SET MAKE_THREADS=8 +REM see -addon in ReadMe.txt +SET "COQ_ADDONS= " + REM ========== PARSE COMMAND LINE PARAMETERS ========== SHIFT @@ -233,6 +236,14 @@ IF "%~0" == "-threads" ( GOTO Parse ) +IF "%~0" == "-addon" ( + SET "COQ_ADDONS=%COQ_ADDONS% %~1" + SHIFT + SHIFT + GOTO Parse +) + + IF NOT "%~0" == "" ( ECHO Install cygwin and download, compile and install OCaml and Coq for MinGW ECHO !!! Illegal parameter %~0 @@ -426,6 +437,7 @@ ECHO ========== BATCH FUNCTIONS ========== ECHO -coqver ^ ECHO -gtksrc ^ build GTK ^(90 min^) or use cygwin version ECHO -threads ^<1..N^> Number of make threads + ECHO -addon ^ Enable building selected addon (can be repeated) ECHO( ECHO See ReadMe.txt for a detailed description of all parameters ECHO( @@ -447,6 +459,7 @@ ECHO ========== BATCH FUNCTIONS ========== ECHO -coqver = %COQ_VERSION% ECHO -gtksrc = %GTK_FROM_SOURCES% ECHO -threads = %MAKE_THREADS% + ECHO -addon = %COQ_ADDONS% GOTO :EOF :CheckYN diff --git a/dev/build/windows/ReadMe.txt b/dev/build/windows/ReadMe.txt index 7e80e33c6d..93851aeb8d 100644 --- a/dev/build/windows/ReadMe.txt +++ b/dev/build/windows/ReadMe.txt @@ -61,6 +61,7 @@ The Script MakeCoq_MinGW does: - either installs MinGW GTK via Cygwin or compiles it fom sources - download, compile and install OCaml, CamlP5, Menhir, lablgtk - download, compile and install Coq +- download, compile and install selected addons - create a Windows installer (NSIS based) The parameters are described below. Mostly paths and the HTTP proxy need to be @@ -335,6 +336,10 @@ Possible values: 1..N. Should not be more than 1.5x the number of cores. Should not be more than available RAM/2GB (e.g. 4 for 8GB) +===== -addon ===== + +Enable build and installation of selected Coq package (can be repeated for +selecting more packages) ==================== TODO ==================== diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index d8cde39f82..ff67416b1e 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1320,6 +1320,16 @@ function make_coq_installer { fi } +###################### ADDONS ##################### + + + +function make_addons { + for addon in $COQ_ADDONS; do + make_addon_$addon + done +} + ###################### TOP LEVEL BUILD ##################### make_sed @@ -1331,6 +1341,8 @@ list_files ocaml make_coq +make_addons + if [ "$INSTALLMAKE" == "Y" ] ; then make_mingw_make fi -- cgit v1.2.3 From 2dd05518ade9f19161eb0699db5e5ece34ca29d4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Feb 2018 10:53:04 +0100 Subject: build: win: addon bignums --- dev/build/windows/makecoq_mingw.sh | 8 +++++++- dev/ci/appveyor.bat | 1 + 2 files changed, 8 insertions(+), 1 deletion(-) (limited to 'dev') diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index ff67416b1e..17a94accd8 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1322,7 +1322,13 @@ function make_coq_installer { ###################### ADDONS ##################### - +function make_addon_bignums { + if build_prep https://github.com/coq/bignums/archive/ master zip 1 bignums-8.8.0; then + logn make make all + logn make-install make install + build_post + fi +} function make_addons { for addon in $COQ_ADDONS; do diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat index dec6f0d182..178121fd2b 100644 --- a/dev/ci/appveyor.bat +++ b/dev/ci/appveyor.bat @@ -23,6 +23,7 @@ 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% ^ + -addon=bignums ^ -setup %CYGROOT%\%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 -- cgit v1.2.3 From aadf6f68289f8ec1042c45b3e29610c2da786150 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 1 Mar 2018 17:38:06 +0100 Subject: build: win: detect 404 as HTML files --- dev/build/windows/makecoq_mingw.sh | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'dev') diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 17a94accd8..4c99648c3a 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -223,6 +223,12 @@ function get_expand_source_tar { cp "$SOURCE_LOCAL_CACHE_CFMT/$name.$3" $TARBALLS else wget $1/$2.$3 + if file -i $2.$3 | grep text/html; then + echo Download failed: $1/$2.$3 + echo The file wget downloaded is an html file: + cat $2.$3 + exit 1 + fi if [ ! "$2.$3" == "$name.$3" ] ; then mv $2.$3 $name.$3 fi -- cgit v1.2.3 From 7aa9b97896c7277c9979d3149fe126793863026e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 2 Mar 2018 01:50:57 -0800 Subject: installer: win: put addons in a separate package --- dev/build/windows/makecoq_mingw.sh | 22 +++++++++++++++++----- dev/build/windows/patches_coq/coq_new.nsi | 11 +++++++++-- 2 files changed, 26 insertions(+), 7 deletions(-) (limited to 'dev') diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 4c99648c3a..b0801190e1 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1286,7 +1286,8 @@ function make_coq_installer { # 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 - # ocal_coq: as above + coq + # ocaml_coq: as above + coq + # ocaml_coq_addons: as above + lib/user-contrib/* # Create coq file list as ocaml_coq / ocaml diff_files coq ocaml_coq ocaml @@ -1300,11 +1301,17 @@ function make_coq_installer { # Coq objects objects required for plugin development = coq objects except those for pre installed plugins diff_files coq_plugindev coq_objects coq_objects_plugins + # Addons (TODO: including objects that could go to the plugindev thing, but + # then one would have to make that package depend on this one, so not + # implemented yet) + diff_files coq_addons ocaml_coq_addons ocaml_coq + # Coq files, except objects needed only for plugin development diff_files coq_base coq coq_plugindev # Convert section files to NSIS format files_to_nsis coq_base + files_to_nsis coq_addons files_to_nsis coq_plugindev files_to_nsis ocaml @@ -1320,7 +1327,7 @@ function make_coq_installer { cp ../patches/ReplaceInFile.nsh dev/nsis VERSION=`grep '^VERSION=' config/Makefile | cut -d = -f 2 | tr -d '\r'` cd dev/nsis - logn nsis-installer "$NSIS" -DVERSION=$VERSION -DARCH=$ARCH -DCOQ_SRC_PATH="$PREFIXCOQ" -DCOQ_ICON=..\\..\\ide\\coq.ico coq_new.nsi + logn nsis-installer "$NSIS" -DVERSION=$VERSION -DARCH=$ARCH -DCOQ_SRC_PATH="$PREFIXCOQ" -DCOQ_ICON=..\\..\\ide\\coq.ico -DCOQ_ADDONS="$COQ_ADDONS" coq_new.nsi build_post fi @@ -1353,14 +1360,19 @@ list_files ocaml make_coq -make_addons - if [ "$INSTALLMAKE" == "Y" ] ; then - make_mingw_make + # I've to comment this out becase, with addons, if this make is in the + # PATH it hides the real one (the one that works, while this one does not) + #make_mingw_make + : fi list_files ocaml_coq +make_addons + +list_files ocaml_coq_addons + if [ "$MAKEINSTALLER" == "Y" ] ; then make_coq_installer fi diff --git a/dev/build/windows/patches_coq/coq_new.nsi b/dev/build/windows/patches_coq/coq_new.nsi index 2c2f0fa47c..55fba6d5ab 100644 --- a/dev/build/windows/patches_coq/coq_new.nsi +++ b/dev/build/windows/patches_coq/coq_new.nsi @@ -9,6 +9,7 @@ ; ARCH The target architecture, either x86_64 or i686 ; COQ_SRC_PATH path of Coq installation in Windows or MinGW format (either \\ or /, but with drive letter) ; COQ_ICON path of Coq icon file in Windows or MinGW format +; COQ_ADDONS list of addons that are shipped ; Enable compression after debugging. ; SetCompress off @@ -69,7 +70,8 @@ Var INSTDIR_DBS ; INSTDIR with \\ instead of \ ;Description LangString DESC_1 ${LANG_ENGLISH} "This package contains Coq and CoqIDE." - LangString DESC_2 ${LANG_ENGLISH} "This package contains an OCaml compiler for Coq native compute and plugin development." + LangString DESC_2 ${LANG_ENGLISH} "This package contains the following extra Coq packages: ${COQ_ADDONS}" + ;LangString DESC_2 ${LANG_ENGLISH} "This package contains an OCaml compiler for Coq native compute and plugin development." LangString DESC_3 ${LANG_ENGLISH} "This package contains the development files needed in order to build a plugin for Coq." LangString DESC_4 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for the current user." LangString DESC_5 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for all users." @@ -150,6 +152,11 @@ SectionEnd ;OCAML !insertmacro ReplaceInFile "$INSTDIR\etc\findlib.conf" "$COQ_SRC_PATH_DBS" "$INSTDIR_DBS" ;OCAML SectionEnd +Section "Coq packages" Sec2 + SetOutPath "$INSTDIR\" + !include "..\..\..\filelists\coq_addons.nsh" +SectionEnd + Section "Coq files for plugin developers" Sec3 SetOutPath "$INSTDIR\" !include "..\..\..\filelists\coq_plugindev.nsh" @@ -176,7 +183,7 @@ SectionEnd !insertmacro MUI_FUNCTION_DESCRIPTION_BEGIN !insertmacro MUI_DESCRIPTION_TEXT ${Sec1} $(DESC_1) - ;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec2} $(DESC_2) + !insertmacro MUI_DESCRIPTION_TEXT ${Sec2} $(DESC_2) !insertmacro MUI_DESCRIPTION_TEXT ${Sec3} $(DESC_3) ;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec4} $(DESC_4) ;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec5} $(DESC_5) -- cgit v1.2.3 From 951f80b0ce46976791d8b7fa7cf68aea11018da0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 2 Mar 2018 17:53:47 +0100 Subject: build: win: turn off build/installation of gnu Make --- dev/build/windows/makecoq_mingw.sh | 5 +---- dev/ci/appveyor.bat | 2 +- 2 files changed, 2 insertions(+), 5 deletions(-) (limited to 'dev') diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index b0801190e1..49eece5a44 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1361,10 +1361,7 @@ list_files ocaml make_coq if [ "$INSTALLMAKE" == "Y" ] ; then - # I've to comment this out becase, with addons, if this make is in the - # PATH it hides the real one (the one that works, while this one does not) - #make_mingw_make - : + make_mingw_make fi list_files ocaml_coq diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat index 178121fd2b..85a71baf7f 100644 --- a/dev/ci/appveyor.bat +++ b/dev/ci/appveyor.bat @@ -23,7 +23,7 @@ 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% ^ - -addon=bignums ^ + -addon=bignums -make=N ^ -setup %CYGROOT%\%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 -- cgit v1.2.3 From eb91eb5dd0487493b0b2e1a62ccabf4c8115ac98 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 6 Mar 2018 05:18:18 -0800 Subject: Hack to make bignum build on windows --- dev/build/windows/makecoq_mingw.sh | 2 ++ 1 file changed, 2 insertions(+) (limited to 'dev') diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 49eece5a44..bea30b1a72 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1337,6 +1337,8 @@ function make_coq_installer { function make_addon_bignums { if build_prep https://github.com/coq/bignums/archive/ master zip 1 bignums-8.8.0; then + # To make command lines shorter :-( + echo 'COQ_SRC_SUBDIRS:=$(filter-out plugins/%,$(COQ_SRC_SUBDIRS)) plugins/syntax' >> Makefile.coq.local logn make make all logn make-install make install build_post -- cgit v1.2.3