Merge PR #6881: [windows] support -addon in build script

5 files changed, 65 insertions, 4 deletions

diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
index 665d54176..ccf22cc86 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   ^<Coq version to install^> 
   ECHO -gtksrc   ^<Y or N^> build GTK ^(90 min^) or use cygwin version
   ECHO -threads  ^<1..N^> Number of make threads
+  ECHO -addon    ^<name^>  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 7e80e33c6..93851aeb8 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 d8cde39f8..bea30b1a7 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
@@ -1280,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
@@ -1294,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
   
@@ -1314,12 +1327,30 @@ 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
 }
 
+###################### ADDONS #####################
+
+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
+  fi
+}
+
+function make_addons {
+  for addon in $COQ_ADDONS; do
+    make_addon_$addon
+  done
+}
+
 ###################### TOP LEVEL BUILD #####################
 
 make_sed
@@ -1337,6 +1368,10 @@ 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 2c2f0fa47..55fba6d5a 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)
diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat
index dec6f0d18..85a71baf7 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 -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