Fix issue #8321 "Add more useful addons to the Windows Installer"

Implemented by merging addon changes in V8.8.2 (keeping everything on master)

3 files changed, 598 insertions, 88 deletions

diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 74dd4d41c1..fcb3d8144e 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -2,7 +2,7 @@
 
 ###################### COPYRIGHT/COPYLEFT ######################
 
-# (C) 2016 Intel Deutschland GmbH
+# (C) 2016..2018 Intel Deutschland GmbH
 # Author: Michael Soegtrop
 #
 # Released to the public by Intel under the
@@ -238,9 +238,10 @@ fi
 # $1 file server name including protocol prefix
 # $2 file name (without extension)
 # $3 file extension
-# $4 number of path levels to strip from tar (usually 1)
-# $5 module name (if different from archive)
-# $6 expand folder name (if different from module name)
+# $4 [optional] number of path levels to strip from tar (usually 1)
+# $5 [optional] module name (if different from archive)
+# $6 [optional] expand folder name (if different from module name)
+# $7 [optional] module base name (used as 2nd choice for patches, defaults to $5)
 # ------------------------------------------------------------------------------
 
 function get_expand_source_tar {
@@ -263,6 +264,12 @@ function get_expand_source_tar {
     folder=$name
   fi
 
+  if [ "$#" -ge 7 ] ; then
+    basename=$7
+  else
+    basename=$name
+  fi
+
   # Set logging target
   logtargetold=$LOGTARGET
   LOGTARGET=$name
@@ -314,8 +321,11 @@ function get_expand_source_tar {
   fi
 
   # Patch if patch file exists
+  # First try specific patch file name then generic patch file name
   if [ -f "$PATCHES/$name.patch" ] ; then
     log1 patch -p1 -i "$PATCHES/$name.patch"
+  elif  [ -f "$PATCHES/$basename.patch" ] ; then
+    log1 patch -p1 -i "$PATCHES/$basename.patch"
   fi
 
   # Go back to base folder
@@ -340,6 +350,7 @@ function get_expand_source_tar {
 # $3 file extension
 # $4 [optional] number of path levels to strip from tar (usually 1)
 # $5 [optional] module name (if different from archive)
+# $6 [optional] module base name (used as 2nd choice for patches, defaults to $5)
 # ------------------------------------------------------------------------------
 
 function build_prep {
@@ -356,6 +367,15 @@ function build_prep {
     name=$2
   fi
 
+  if [ "$#" -ge 6 ] ; then
+    basename=$6
+  else
+    basename=$name
+  fi
+
+  # Set installer section to not set by default
+  installersection=
+
   # Check if build is already done
   if [ ! -f "$FLAGFILES/$name.finished" ] ; then
     BUILD_PACKAGE_NAME=$name
@@ -365,7 +385,7 @@ function build_prep {
 
     touch "$FLAGFILES/$name.started"
 
-    get_expand_source_tar "$1" "$2" "$3" "$strip" "$name"
+    get_expand_source_tar "$1" "$2" "$3" "$strip" "$name" "$name" "$basename"
 
     cd "$name"
 
@@ -381,6 +401,61 @@ function build_prep {
 }
 
 # ------------------------------------------------------------------------------
+# Like build_prep, but gets the data from an entry in ci-basic-overlay.sh
+# This assumes the following definitions exist in ci-basic-overlay.sh,
+# or in a file in the user-overlays folder:
+# $1_CI_REF
+# $1_CI_ARCHIVEURL
+# $1_CI_GITURL
+# ATTENTION: variables in ci-basic-overlay.sh are loaded by load_overlay_data.
+# load_overlay_data is is called at the end of make_coq (even if the build is skipped)
+#
+# Parameters
+# $1 base name of module in ci-basic-overlay.sh, e.g. mathcomp, bignums, ...
+# ------------------------------------------------------------------------------
+
+function build_prep_overlay {
+  urlvar=$1_CI_ARCHIVEURL
+  gitvar=$1_CI_GITURL
+  refvar=$1_CI_REF
+  url=${!urlvar}
+  git=${!gitvar}
+  ref=${!refvar}
+  ver=$(git ls-remote "$git" "refs/heads/$ref" | cut -f 1)
+  if [[ "$ver" == "" ]]; then
+      # $1_CI_REF must have been a tag or hash, not a branch
+      ver="$ref"
+  fi
+  build_prep "$url" "$ver" tar.gz 1 "$1-$ver" "$1"
+}
+
+# ------------------------------------------------------------------------------
+# Load overlay version variables from ci-basic-overlay.sh and user-overlays/*.sh
+# ------------------------------------------------------------------------------
+
+function load_overlay_data {
+  if [ -n "${GITLAB_CI+}" ]; then
+    export CI_BRANCH="$CI_COMMIT_REF_NAME"
+    if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]]; then
+      export CI_PULL_REQUEST="${CI_BRANCH#pr-}"
+    else
+      export CI_PULL_REQUEST=""
+    fi
+  else
+    export CI_BRANCH=""
+    export CI_PULL_REQUEST=""
+    # Used when building 8.8.0 with the latest scripts
+    export TRAVIS_BRANCH=""
+    export TRAVIS_PULL_REQUEST=""
+  fi
+
+  for overlay in /build/user-overlays/*.sh; do
+    . "$overlay"
+  done
+  . /build/ci-basic-overlay.sh
+}
+
+# ------------------------------------------------------------------------------
 # Finalize a module build
 # - create name.finished
 # - go back to base folder
@@ -392,6 +467,7 @@ function build_post {
     touch "$FLAGFILES/$BUILD_PACKAGE_NAME.finished"
     PATH=$BUILD_OLDPATH
     LOGTARGET=other
+    installer_addon_end
   fi
 }
 
@@ -522,6 +598,101 @@ function files_to_nsis {
   tr '/' '\\' < "/build/filelists/$1" | sed -r 's/^\.(.*)\\([^\\]+)$/SetOutPath $INSTDIR\\\1\nFile ${COQ_SRC_PATH}\\\1\\\2/' > "/build/filelists/$1.nsh"
 }
 
+# ------------------------------------------------------------------------------
+# Create an nsis installer addon section
+#
+# parameters
+# $1 identifier of installer section and base name of file list files
+# $2 human readable name of section
+# $3 description of section
+# $4 flags (space separated list of keywords): off = default off
+#
+# $1 must be a valid NSIS identifier!
+# ------------------------------------------------------------------------------
+
+function installer_addon_section {
+  installersection=$1
+  list_files "addon_pre_$installersection"
+
+  echo 'LangString' "DESC_$1" '${LANG_ENGLISH}' "\"$3\"" >> "/build/filelists/addon_strings.nsh"
+
+  echo '!insertmacro MUI_DESCRIPTION_TEXT' '${'"Sec_$1"'}' '$('"DESC_$1"')' >> "/build/filelists/addon_descriptions.nsh"
+
+  local sectionoptions=
+  if [[ "$4" == *off* ]] ; then sectionoptions+=" /o" ; fi
+
+  echo "Section $sectionoptions \"$2\" Sec_$1" >> "/build/filelists/addon_sections.nsh"
+  echo 'SetOutPath "$INSTDIR\"' >> "/build/filelists/addon_sections.nsh"
+  echo '!include "..\..\..\filelists\addon_'"$1"'.nsh"' >> "/build/filelists/addon_sections.nsh"
+  echo 'SectionEnd' >> "/build/filelists/addon_sections.nsh"
+}
+
+# ------------------------------------------------------------------------------
+# Start an installer addon dependency group
+#
+# parameters
+# $1 identifier of the section which depends on other sections
+# The parameters must match the $1 parameter of a installer_addon_section call
+# ------------------------------------------------------------------------------
+
+dependencysections=
+
+function installer_addon_dependency_beg {
+  installer_addon_dependency "$1"
+  dependencysections="$1 $dependencysections"
+}
+
+# ------------------------------------------------------------------------------
+# End an installer addon dependency group
+# ------------------------------------------------------------------------------
+
+function installer_addon_dependency_end {
+  set -- $dependencysections
+  shift
+  dependencysections="$*"
+}
+
+# ------------------------------------------------------------------------------
+# Create an nsis installer addon dependency entry
+# This needs to be bracketed with installer_addon_dependencies_beg/end
+#
+# parameters
+# $1 identifier of the section on which other sections might depend
+# The parameters must match the $1 parameter of a installer_addon_section call
+# ------------------------------------------------------------------------------
+
+function installer_addon_dependency {
+  for section in $dependencysections ; do
+    echo '${CheckSectionDependency} ${Sec_'"$section"'} ${Sec_'"$1"'} '"'$section' '$1'" >> "/build/filelists/addon_dependencies.nsh"
+  done
+}
+
+# ------------------------------------------------------------------------------
+# Finish an installer section after an addon build
+#
+# This creates the file list files
+#
+# parameters: none
+# ------------------------------------------------------------------------------
+
+function installer_addon_end {
+  if [ -n "$installersection" ]; then
+    list_files "addon_post_$installersection"
+    diff_files "addon_$installersection" "addon_post_$installersection" "addon_pre_$installersection"
+    files_to_nsis "addon_$installersection"
+  fi
+}
+
+# ------------------------------------------------------------------------------
+# Set all timeouts in all .v files to 1000
+# Since timeouts can lead to CI failures, this is useful
+#
+# parameters: none
+# ------------------------------------------------------------------------------
+
+function coq_set_timeouts_1000 {
+  find . -type f -name '*.v' -print0 | xargs -0 sed -i 's/timeout\s\+[0-9]\+/timeout 1000/'
+}
 
 ###################### MODULE BUILD FUNCTIONS #####################
 
@@ -1287,6 +1458,8 @@ function make_coq {
 
     build_post
   fi
+
+  load_overlay_data
 }
 
 ##### GNU Make for MinGW #####
@@ -1450,18 +1623,15 @@ function make_coq_installer {
   fi
 }
 
-###################### ADDONS #####################
+###################### ADDON COQ LIBRARIES / PLUGINS / TOOLS #####################
 
 # The bignums library
 # Provides BigN, BigZ, BigQ that used to be part of Coq standard library
 
 function make_addon_bignums {
-  bignums_SHA=$(git ls-remote "$bignums_CI_GITURL" "refs/heads/$bignums_CI_REF" | cut -f 1)
-  if [[ "$bignums_SHA" == "" ]]; then
-      # $bignums_CI_REF must have been a tag / commit and not a branch
-      bignums_SHA="$bignums_CI_REF"
-  fi
-  if build_prep "$bignums_CI_ARCHIVEURL" "$bignums_SHA" zip 1 "bignums-$bignums_SHA"; then
+  installer_addon_dependency bignums
+  if build_prep_overlay bignums; then
+    installer_addon_section bignums "Bignums" "Coq library for fast arbitrary size numbers" ""
     # To make command lines shorter :-(
     echo 'COQ_SRC_SUBDIRS:=$(filter-out plugins/%,$(COQ_SRC_SUBDIRS)) plugins/syntax' >> Makefile.coq.local
     log1 make all
@@ -1470,61 +1640,275 @@ function make_addon_bignums {
   fi
 }
 
+# Equations plugin
+# A function definition plugin
+
+function make_addon_equations {
+  installer_addon_dependency equations
+  if build_prep_overlay Equations; then
+    installer_addon_section equations "Equations" "Coq plugin for defining functions by equations" ""
+    # Note: PATH is autmatically saved/restored by build_prep / build_post
+    PATH=$COQBIN:$PATH
+    logn coq_makefile ${COQBIN}coq_makefile -f _CoqProject -o Makefile
+    log1 make
+    log2 make install
+    build_post
+  fi
+}
+
+# mathcomp - ssreflect and mathematical components library
+
+function make_addon_mathcomp {
+  installer_addon_dependency mathcomp
+  if build_prep_overlay mathcomp; then
+    installer_addon_section mathcomp "Math-Components" "Coq library with mathematical components" ""
+    cd mathcomp
+    log1 make $MAKE_OPT
+    log2 make install
+    build_post
+  fi
+}
+
+# ssreflect part of mathcomp
+
+function make_addon_ssreflect {
+  # if mathcomp addon is requested, build this instead
+  if [[ "$COQ_ADDONS" == *mathcomp* ]]; then
+    make_addon_mathcomp
+  else
+    # Note: since either mathcomp or ssreflect is defined, it is fine to name both mathcomp
+    installer_addon_dependency ssreflect
+    if build_prep_overlay mathcomp; then
+      installer_addon_section ssreflect "SSReflect" "Coq support library for small scale reflection plugin" ""
+      cd mathcomp
+      logn make-makefile  make Makefile.coq
+      logn make-ssreflect make $MAKE_OPT -f Makefile.coq ssreflect/all_ssreflect.vo
+      logn make-install   make -f Makefile.coq install
+      build_post
+    fi
+  fi
+}
+
 # Ltac-2 plugin
 # A new (experimental) tactic language
 
 function make_addon_ltac2 {
-  ltac2_SHA=$(git ls-remote "$ltac2_CI_GITURL" "refs/heads/$ltac2_CI_REF" | cut -f 1)
-  if [[ "$ltac2_SHA" == "" ]]; then
-      # $ltac2_CI_REF must have been a tag / commit and not a branch
-      ltac2_SHA="$ltac2_CI_REF"
-  fi
-  if build_prep "$ltac2_CI_ARCHIVEURL" "$ltac2_SHA" zip 1 "ltac2-$ltac2_SHA"; then
+  installer_addon_dependency ltac2
+  if build_prep_overlay ltac2; then
+    installer_addon_section ltac2 "Ltac-2" "Coq plugin with the Ltac-2 enhanced tactics language" ""
     log1 make all
     log2 make install
     build_post
   fi
 }
 
-# Equations plugin
-# A function definition plugin
-
-function make_addon_equations {
-  Equations_SHA=$(git ls-remote "$Equations_CI_GITURL" "refs/heads/$Equations_CI_REF" | cut -f 1)
-  if [[ "$Equations_SHA" == "" ]]; then
-      # $Equations_CI_REF must have been a tag / commit and not a branch
-      Equations_SHA="$Equations_CI_REF"
+# UniCoq plugin
+# An alternative unification algorithm
+function make_addon_unicoq {
+  installer_addon_dependency unicoq
+  if build_prep_overlay unicoq; then
+    log1 coq_makefile -f Make -o Makefile
+    log1 make
+    log2 make install
+    build_post
   fi
-  if build_prep "$Equations_CI_ARCHIVEURL" "$Equations_SHA" zip 1 "Equations-$Equations_SHA"; then
-    # Note: PATH is autmatically saved/restored by build_prep / build_post
-    PATH=$COQBIN:$PATH
-    logn coq_makefile ${COQBIN}coq_makefile -f _CoqProject -o Makefile
+}
+
+# Mtac2 plugin
+# An alternative typed tactic language
+function make_addon_mtac2 {
+  installer_addon_dependency_beg mtac2
+  make_addon_unicoq
+  installer_addon_dependency_end
+  if build_prep_overlay mtac2; then
+    log1 coq_makefile -f _CoqProject -o Makefile
     log1 make
     log2 make install
     build_post
   fi
 }
 
-function make_addons {
-  if [ -n "$GITLAB_CI" ]; then
-    export CI_BRANCH="$CI_COMMIT_REF_NAME"
-    if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]]; then
-      export CI_PULL_REQUEST="${CI_BRANCH#pr-}"
-    else
-      export CI_PULL_REQUEST=""
+# Menhir parser generator
+
+function make_addon_menhir {
+  make_menhir
+  # If COQ and OCaml are installed to the same folder, there is nothing to do
+  installer_addon_dependency menhir
+  if [ "$PREFIXOCAML" != "$PREFIXCOQ" ] ; then
+    # Just install menhir files required for COQ to COQ target folder
+    if [ ! -f "$FLAGFILES/menhir-addon.finished" ] ; then
+      installer_addon_section menhir "Menhir" "Menhir parser generator windows executable and libraries" ""
+      LOGTARGET=menhir-addon
+      touch "$FLAGFILES/menhir-addon.started"
+      # Menhir executable
+      install_glob "$PREFIXOCAML/bin" 'menhir.exe' "$PREFIXCOQ/bin/"
+      # Menhir Standard library
+      install_glob "$PREFIXOCAML/share/menhir/" '*.mly' "$PREFIXCOQ/share/menhir/"
+      # Menhir PDF doc
+      install_glob "$PREFIXOCAML/share/doc/menhir/" '*.pdf' "$PREFIXCOQ/doc/menhir/"
+      touch "$FLAGFILES/menhir-addon.finished"
+      LOGTARGET=other
+      installer_addon_end
     fi
-  else
-    export CI_BRANCH=""
-    export CI_PULL_REQUEST=""
   fi
-  for overlay in /build/user-overlays/*.sh; do
-    . "$overlay"
-  done
-  . /build/ci-basic-overlay.sh
+}
+
+# COQ library for Menhir
+
+function make_addon_menhirlib {
+  installer_addon_dependency menhirlib
+  if build_prep_overlay menhirlib; then
+    installer_addon_section menhirlib "Menhirlib" "Coq support library for using Menhir generated parsers in Coq" ""
+    # The supplied makefiles don't work in any way on cygwin
+    cd src
+    echo -R . MenhirLib > _CoqProject
+    ls -1 *.v >> _CoqProject
+    log1 coq_makefile -f _CoqProject -o Makefile.coq
+    log1 make -f Makefile.coq all
+    logn make-install make -f Makefile.coq install
+    build_post
+  fi
+}
+
+# CompCert
+
+function make_addon_compcert {
+  installer_addon_dependency_beg compcert
+  make_menhir
+  make_addon_menhirlib
+  installer_addon_dependency_end
+  if build_prep_overlay CompCert; then
+    installer_addon_section compcert "CompCert" "ATTENTION: THIS IS NOT OPEN SOURCE! CompCert verified C compiler and Clightgen (required for using VST for your own code)" "off"
+    logn configure ./configure -ignore-coq-version -clightgen -prefix "$PREFIXCOQ" -coqdevdir "$PREFIXCOQ/lib/coq/user-contrib/compcert" x86_32-cygwin
+    log1 make
+    log2 make install
+    logn install-license-1 install -D -T  "LICENSE" "$PREFIXCOQ/lib/coq/user-contrib/compcert/LICENSE"
+    logn install-license-2 install -D -T  "LICENSE" "$PREFIXCOQ/lib/compcert/LICENSE"
+    build_post
+  fi
+}
+
+# Princeton VST
+
+function install_addon_vst {
+    VSTDEST="$PREFIXCOQ/lib/coq/user-contrib/VST"
+
+    # Install VST .v, .vo, .c and .h files
+    install_rec compcert '*.v' "$VSTDEST/compcert/"
+    install_rec compcert '*.vo' "$VSTDEST/compcert/"
+    install_glob "msl" '*.v' "$VSTDEST/msl/"
+    install_glob "msl" '*.vo' "$VSTDEST/msl/"
+    install_glob "sepcomp" '*.v' "$VSTDEST/sepcomp/"
+    install_glob "sepcomp" '*.vo' "$VSTDEST/sepcomp/"
+    install_glob "floyd" '*.v' "$VSTDEST/floyd/"
+    install_glob "floyd" '*.vo' "$VSTDEST/floyd/"
+    install_glob "progs" '*.v' "$VSTDEST/progs/"
+    install_glob "progs" '*.c' "$VSTDEST/progs/"
+    install_glob "progs" '*.h' "$VSTDEST/progs/"
+    install_glob "veric" '*.v' "$VSTDEST/msl/"
+    install_glob "veric" '*.vo' "$VSTDEST/msl/"
+
+    # Install VST documentation files
+    install_glob "." 'LICENSE' "$VSTDEST"
+    install_glob "." '*.md' "$VSTDEST"
+    install_glob "compcert" '*' "$VSTDEST/compcert"
+    install_glob "doc" '*.pdf' "$VSTDEST/doc"
+
+    # Install VST _CoqProject files
+    install_glob "." '_CoqProject*' "$VSTDEST"
+    install_glob "." '_CoqProject-export' "$VSTDEST/progs"
+}
+
+function make_addon_vst {
+  installer_addon_dependency vst
+  if build_prep_overlay VST; then
+    installer_addon_section vst "VST" "ATTENTION: SOME INCLUDED COMPCERT PARTS ARE NOT OPEN SOURCE! Verified Software Toolchain for verifying C code" "off"
+    log1 coq_set_timeouts_1000
+    log1 make IGNORECOQVERSION=true $MAKE_OPT
+    log1 install_addon_vst
+    build_post
+  fi
+}
+
+# coquelicot Real analysis
+
+function make_addon_coquelicot {
+  installer_addon_dependency_beg coquelicot
+  make_addon_ssreflect
+  installer_addon_dependency_end
+  if build_prep_overlay Coquelicot; then
+    installer_addon_section coquelicot "Coquelicot" "Coq library for real analysis" ""
+    logn configure ./configure --libdir="$PREFIXCOQ/lib/coq/user-contrib/Coquelicot"
+    logn remake ./remake
+    logn remake-install ./remake install
+    build_post
+  fi
+}
+
+# AAC associative / commutative rewriting
+
+function make_addon_aactactics {
+  installer_addon_dependency aac
+  if build_prep_overlay aactactis; then
+    installer_addon_section aac "AAC" "Coq plugin for extensible associative and commutative rewriting" ""
+    log1 make
+    log2 make install
+    build_post
+  fi
+}
+
+# extlib
+
+function make_addon_extlib {
+  installer_addon_dependency extlib
+  if build_prep_overlay ext_lib; then
+    installer_addon_section extlib "Ext-Lib" "Coq library with many reusable general purpose components" ""
+    log1 make $MAKE_OPT
+    log2 make install
+    build_post
+  fi
+}
+
+# SimpleIO
+
+function make_addon_simple_io {
+  installer_addon_dependency simpleIO
+  if build_prep_overlay simple_io; then
+    installer_addon_section simpleIO "SimpleIO" "Coq plugin for reading and writing files directly from Coq code" ""
+    log1 make $MAKE_OPT
+    log2 make install
+    build_post
+  fi
+}
+
+# Quickchick Randomized Property-Based Testing Plugin for Coq
+
+function make_addon_quickchick {
+  installer_addon_dependency_beg quickchick
+  make_addon_ssreflect
+  make_addon_extlib
+  make_addon_simple_io
+  make_ocamlbuild
+  installer_addon_dependency_end
+  if build_prep_overlay quickchick; then
+    installer_addon_section quickchick "QuickChick" "Coq plugin for randomized testing and counter example search" ""
+    log1 make
+    log2 make install
+    build_post
+  fi
+}
+
+# Main function for building addons
+
+function make_addons {
+  # Note: ':' is the empty command, which does not produce any output
+  : > "/build/filelists/addon_dependencies.nsh"
 
   for addon in $COQ_ADDONS; do
     "make_addon_$addon"
   done
+
+  sort -u -o "/build/filelists/addon_dependencies.nsh" "/build/filelists/addon_dependencies.nsh"
 }
 
 ###################### TOP LEVEL BUILD #####################
diff --git a/dev/build/windows/patches_coq/coq_new.nsi b/dev/build/windows/patches_coq/coq_new.nsi
index 55fba6d5ab..9947965c28 100644
--- a/dev/build/windows/patches_coq/coq_new.nsi
+++ b/dev/build/windows/patches_coq/coq_new.nsi
@@ -38,43 +38,20 @@ Var INSTDIR_DBS       ; INSTDIR with \\ instead of \
 
   ;Folder selection page
   InstallDir "C:\${MY_PRODUCT}"
-  
+
   ;Remember install folder
   InstallDirRegKey HKCU "Software\${MY_PRODUCT}" ""
 
 ;--------------------------------
-;Modern UI Configuration
-  
-  !define MUI_ICON "${COQ_ICON}"
-
-  !insertmacro MUI_PAGE_WELCOME
-  !insertmacro MUI_PAGE_LICENSE "${COQ_SRC_PATH}/license_readme/coq/License.txt"
-  !insertmacro MUI_PAGE_COMPONENTS
-  !define MUI_DIRECTORYPAGE_TEXT_TOP "Select where to install Coq.  The path MUST NOT include spaces."
-  !insertmacro MUI_PAGE_DIRECTORY
-  !insertmacro MUI_PAGE_INSTFILES
-  !insertmacro MUI_PAGE_FINISH
-  
-  !insertmacro MUI_UNPAGE_WELCOME
-  !insertmacro MUI_UNPAGE_CONFIRM
-  !insertmacro MUI_UNPAGE_INSTFILES
-  !insertmacro MUI_UNPAGE_FINISH  
-
-;--------------------------------
-;Languages
- 
-  !insertmacro MUI_LANGUAGE "English"
-  
-;--------------------------------
-;Language Strings
+;Extra license pages
 
-  ;Description
-  LangString DESC_1 ${LANG_ENGLISH} "This package contains Coq and CoqIDE."
-  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."
+!macro MUI_PAGE_LICENSE_EXTRA Licensefile Header Subheader Bottom SelFunc
+  !define MUI_PAGE_HEADER_TEXT "${Header}"
+  !define MUI_PAGE_HEADER_SUBTEXT "${Subheader}"
+  !define MUI_LICENSEPAGE_TEXT_BOTTOM "${Bottom}"
+  !define MUI_PAGE_CUSTOMFUNCTION_PRE ${SelFunc}
+  !insertmacro MUI_PAGE_LICENSE "${Licensefile}"
+!macroend
 
 ;--------------------------------
 ; Check for white spaces
@@ -95,7 +72,6 @@ FunctionEnd
 ;--------------------------------
 ;Installer Sections
 
-
 Section "Coq" Sec1
 
   SetOutPath "$INSTDIR\"
@@ -105,7 +81,7 @@ Section "Coq" Sec1
 
   ;Store install folder
   WriteRegStr HKCU "Software\${MY_PRODUCT}" "" $INSTDIR
-  
+
   ;Create uninstaller
   WriteUninstaller "$INSTDIR\Uninstall.exe"
   WriteRegStr HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
@@ -123,7 +99,7 @@ Section "Coq" Sec1
 
   ; Create start menu entries
   ; SetOutPath is required for the path in the .lnk files
-  SetOutPath "$INSTDIR" 
+  SetOutPath "$INSTDIR"
   CreateDirectory "$SMPROGRAMS\Coq"
   ; The first shortcut set here is treated as main application by Windows 7/8.
   ; Use CoqIDE as main application
@@ -138,24 +114,23 @@ SectionEnd
 ;OCAML Section "Ocaml for native compute and plugin development" Sec2
 ;OCAML   SetOutPath "$INSTDIR\"
 ;OCAML   !include "..\..\..\filelists\ocaml.nsh"
-;OCAML 
+;OCAML
 ;OCAML   ; Create a few slash / backslash variants of the source and install path
 ;OCAML   ; Note: NSIS has variables, written as $VAR and defines, written as ${VAR}
 ;OCAML   !insertmacro StrRep $COQ_SRC_PATH_BS  ${COQ_SRC_PATH} "/" "\"
 ;OCAML   !insertmacro StrRep $COQ_SRC_PATH_DBS ${COQ_SRC_PATH} "/" "\\"
 ;OCAML   !insertmacro StrRep $INSTDIR_DBS      $INSTDIR        "\" "\\"
-;OCAML 
+;OCAML
 ;OCAML   ; Replace absolute paths in some OCaml config files
 ;OCAML   ; These are not all, see ReadMe.txt
 ;OCAML   !insertmacro ReplaceInFile "$INSTDIR\libocaml\ld.conf" "/"  "\"
 ;OCAML   !insertmacro ReplaceInFile "$INSTDIR\libocaml\ld.conf" "$COQ_SRC_PATH_BS"  "$INSTDIR"
 ;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
+
+SectionGroup "Coq addons" Sec2
+  !include "..\..\..\filelists\addon_sections.nsh"
+SectionGroupEnd
 
 Section "Coq files for plugin developers" Sec3
   SetOutPath "$INSTDIR\"
@@ -179,6 +154,130 @@ SectionEnd
 ;OCAML SectionEnd
 
 ;--------------------------------
+;Section dependencies
+
+; Parameters on the stack:
+; top-0 : section B on which section A dependencies
+; top-1 : section A, which depends on section B
+; top-2 : name of section B
+; top-3 : name of section A
+
+Function CheckSectionDependency
+            ; stack=nameB nameA secB secA rest
+  Exch $R3  ; stack=$R3   nameA secB secA rest; $R3=nameB
+  Exch      ; stack=nameA $R3   secB secA rest
+  Exch $R2  ; stack=$R2   $R3   secB secA rest; $R2=nameA
+  Exch 2    ; stack=secB  $R3   $R2  secA rest
+  Exch $R1  ; stack=$R1   $R3   $R2  secA rest; $R1=secB
+  Exch 3    ; stack=secA  $R3   $R2  $R1  rest;
+  Exch $R0  ; stack=$R0   $R3   $R2  $R1  rest; $R0=secA
+            ; Take care of save order when popping the stack!
+  Push $R4
+  Push $R5
+
+  SectionGetFlags $R0 $R0
+  IntOp $R0 $R0 & ${SF_SELECTED}
+
+  SectionGetFlags $R1 $R4
+  IntOp $R5 $R4 & ${SF_SELECTED}
+
+  ${If} $R0 == ${SF_SELECTED}
+  ${AndIf} $R5 != ${SF_SELECTED}
+
+  IntOp $R5 $R4 | ${SF_SELECTED}
+  SectionSetFlags $R1 $R5
+  MessageBox MB_OK '"$R3" has been selected, because "$R2" depends on it'
+
+  ${EndIf}
+
+  Pop $R5
+  Pop $R4
+  Pop $R0
+  Pop $R3
+  Pop $R2
+  Pop $R1
+FunctionEnd
+
+!macro CheckSectionDependency secA secB nameA nameB
+  Push "${secA}"
+  Push "${secB}"
+  Push "${nameA}"
+  Push "${nameB}"
+  Call CheckSectionDependency
+!macroend
+
+!define CheckSectionDependency "!insertmacro CheckSectionDependency"
+
+Function .onSelChange
+  !include "..\..\..\filelists\addon_dependencies.nsh"
+FunctionEnd
+
+;--------------------------------
+;Modern UI Configuration
+
+; Note: this must be placed after the sections, because below we need to check at compile time
+; if sections exist (by !ifdef <section_index_var>) to decide if the license page must be included.
+; The section index variables are only defined after the section definitions.
+
+  !define MUI_ICON "${COQ_ICON}"
+
+  !insertmacro MUI_PAGE_WELCOME
+  !insertmacro MUI_PAGE_LICENSE "${COQ_SRC_PATH}/license_readme/coq/License.txt"
+  !insertmacro MUI_PAGE_COMPONENTS
+
+  !ifdef Sec_compcert
+    !define LicCompCert_Title "CompCert License Agreement"
+    !define LicCompCert_SubTitle "You selected the CompCert addon. CompCert is not open source. Please review the license terms before installing CompCert!"
+    !define LicCompCert_Bottom "If you accept the terms of the agreement, click I Agree to continue. Otherwise go back and unselect the CompCert addon."
+    !insertmacro MUI_PAGE_LICENSE_EXTRA "${COQ_SRC_PATH}/lib/coq/user-contrib/compcert/LICENSE" "${LicCompCert_Title}" "${LicCompCert_SubTitle}" "${LicCompCert_Bottom}" SelFuncCompCert
+
+    Function SelFuncCompCert
+      ${Unless} ${SectionIsSelected} ${Sec_compcert}
+        Abort
+      ${EndUnless}
+    FunctionEnd
+  !endif
+
+  !ifdef Sec_vst
+    !define LicVST_Title "Princeton VST License Agreement"
+    !define LicVST_SubTitle "You selected the VST addon. VST contains parts of CompCert which are not open source. Please review the license terms before installing VST!"
+    !define LicVST_Bottom "If you accept the terms of the agreement, click I Agree to continue. Otherwise go back and unselect the VST addon."
+    !insertmacro MUI_PAGE_LICENSE_EXTRA "${COQ_SRC_PATH}/lib/coq/user-contrib/VST/LICENSE" "${LicVST_Title}" "${LicVST_SubTitle}" "${LicVST_Bottom}" SelFuncVST
+
+    Function SelFuncVST
+      ${Unless} ${SectionIsSelected} ${Sec_vst}
+        Abort
+      ${EndUnless}
+    FunctionEnd
+  !endif
+
+  !define MUI_DIRECTORYPAGE_TEXT_TOP "Select where to install Coq.  The path MUST NOT include spaces."
+  !insertmacro MUI_PAGE_DIRECTORY
+  !insertmacro MUI_PAGE_INSTFILES
+  !insertmacro MUI_PAGE_FINISH
+
+  !insertmacro MUI_UNPAGE_WELCOME
+  !insertmacro MUI_UNPAGE_CONFIRM
+  !insertmacro MUI_UNPAGE_INSTFILES
+  !insertmacro MUI_UNPAGE_FINISH
+
+;--------------------------------
+;Languages
+
+  !insertmacro MUI_LANGUAGE "English"
+
+;--------------------------------
+;Language Strings
+
+  ;Description
+  LangString DESC_1 ${LANG_ENGLISH} "This package contains Coq and CoqIDE."
+  LangString DESC_2 ${LANG_ENGLISH} "This package contains the following extra Coq packages: ${COQ_ADDONS}"
+  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."
+  !include "..\..\..\filelists\addon_strings.nsh"
+
+;--------------------------------
 ;Descriptions
 
 !insertmacro MUI_FUNCTION_DESCRIPTION_BEGIN
@@ -187,8 +286,9 @@ SectionEnd
   !insertmacro MUI_DESCRIPTION_TEXT ${Sec3} $(DESC_3)
   ;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec4} $(DESC_4)
   ;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec5} $(DESC_5)
+  !include "..\..\..\filelists\addon_descriptions.nsh"
 !insertmacro MUI_FUNCTION_DESCRIPTION_END
- 
+
 ;--------------------------------
 ;Uninstaller Section
 
@@ -214,7 +314,7 @@ Section "Uninstall"
   Delete "$SMPROGRAMS\Coq\The Coq HomePage.url"
   Delete "$SMPROGRAMS\Coq\The Coq Standard Library.url"
   Delete "$INSTDIR\Uninstall.exe"
-  
+
   ; Registry keys
   DeleteRegKey HKCU "Software\${MY_PRODUCT}"
   DeleteRegKey HKLM "SOFTWARE\Coq"
diff --git a/dev/build/windows/patches_coq/quickchick.patch b/dev/build/windows/patches_coq/quickchick.patch
new file mode 100755
index 0000000000..1afa6e7f95
--- /dev/null
+++ b/dev/build/windows/patches_coq/quickchick.patch
@@ -0,0 +1,26 @@
+diff/patch file created on Mon, Aug 27, 2018  9:21:52 AM with:
+difftar-folder.sh tarballs/quickchick-v1.0.2.tar.gz quickchick-v1.0.2 1
+TARFILE= tarballs/quickchick-v1.0.2.tar.gz
+FOLDER= quickchick-v1.0.2
+TARSTRIP= 1
+TARPREFIX= QuickChick-1.0.2/
+ORIGFOLDER= quickchick-v1.0.2.orig
+--- quickchick-v1.0.2.orig/Makefile	2018-08-22 18:21:39.000000000 +0200
++++ quickchick-v1.0.2/Makefile	2018-08-27 09:21:04.710461100 +0200
+@@ -2,7 +2,7 @@
+ .PHONY: plugin install install-plugin clean quickChickTool
+ 
+ QCTOOL_DIR=quickChickTool
+-QCTOOL_EXE=quickChickTool.byte
++QCTOOL_EXE=quickChickTool.native
+ QCTOOL_SRC=$(QCTOOL_DIR)/quickChickTool.ml \
+ 		   $(QCTOOL_DIR)/quickChickToolTypes.ml \
+ 		   $(QCTOOL_DIR)/quickChickToolLexer.mll \
+@@ -32,7 +32,7 @@
+ install: all
+ 	$(V)$(MAKE) -f Makefile.coq install > $(TEMPFILE)
+ # Manually copying the remaining files
+-	$(V)cp $(QCTOOL_EXE) $(shell opam config var bin)/quickChick
++	$(V)cp $(QCTOOL_EXE) "$(COQBIN)/quickChick"
+ #	 $(V)cp src/quickChickLib.cmx $(COQLIB)/user-contrib/QuickChick
+ #	 $(V)cp src/quickChickLib.o $(COQLIB)/user-contrib/QuickChick