1 files changed, 61 insertions, 23 deletions

diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 86cc5f2d..070af6b4 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -159,19 +159,19 @@ if [ "${COQREGTESTING:-N}" == "Y" ] ; then
   # Log command output - take log target name from command name (like log1 make => log target is "<module>-make")
   log1() {
     { local -; set +x; } 2> /dev/null
-    "$@" >"$LOGS/$LOGTARGET-$1.log"  2>"$LOGS/$LOGTARGET-$1.err"
+    "$@" >"$LOGS/$LOGTARGET-$1_log.txt"  2>"$LOGS/$LOGTARGET-$1_err.txt"
   }
 
   # Log command output - take log target name from command name and first argument (like log2 make install => log target is "<module>-make-install")
   log2() {
     { local -; set +x; } 2> /dev/null
-    "$@" >"$LOGS/$LOGTARGET-$1-$2.log" 2>"$LOGS/$LOGTARGET-$1-$2.err"
+    "$@" >"$LOGS/$LOGTARGET-$1-$2_log.txt" 2>"$LOGS/$LOGTARGET-$1-$2_err.txt"
   }
 
   # Log command output - take log target name from command name and second argument (like log_1_3 ocaml setup.ml -configure => log target is "<module>-ocaml--configure")
   log_1_3() {
     { local -; set +x; } 2> /dev/null
-    "$@" >"$LOGS/$LOGTARGET-$1-$3.log" 2>"$LOGS/$LOGTARGET-$1-$3.err"
+    "$@" >"$LOGS/$LOGTARGET-$1-$3_log.txt" 2>"$LOGS/$LOGTARGET-$1-$3_err.txt"
   }
 
   # Log command output - log target name is first argument (like logn untar tar xvaf ... => log target is "<module>-untar")
@@ -179,26 +179,26 @@ if [ "${COQREGTESTING:-N}" == "Y" ] ; then
     { local -; set +x; } 2> /dev/null
     LOGTARGETEX=$1
     shift
-    "$@" >"$LOGS/$LOGTARGET-$LOGTARGETEX.log" 2>"$LOGS/$LOGTARGET-$LOGTARGETEX.err"
+    "$@" >"$LOGS/$LOGTARGET-${LOGTARGETEX}_log.txt" 2>"$LOGS/$LOGTARGET-${LOGTARGETEX}_err.txt"
   }
 else
   # If COQREGTESTING, log to log files and console
   # Log command output - take log target name from command name (like log1 make => log target is "<module>-make")
   log1() {
     { local -; set +x; } 2> /dev/null
-    "$@" > >(tee "$LOGS/$LOGTARGET-$1.log" | sed -e "s/^/$LOGTARGET-$1.log: /") 2> >(tee "$LOGS/$LOGTARGET-$1.err" | sed -e "s/^/$LOGTARGET-$1.err: /" 1>&2)
+    "$@" > >(tee "$LOGS/$LOGTARGET-$1_log.txt" | sed -e "s/^/$LOGTARGET-$1_log.txt: /") 2> >(tee "$LOGS/$LOGTARGET-$1_err.txt" | sed -e "s/^/$LOGTARGET-$1_err.txt: /" 1>&2)
   }
 
   # Log command output - take log target name from command name and first argument (like log2 make install => log target is "<module>-make-install")
   log2() {
     { local -; set +x; } 2> /dev/null
-    "$@" > >(tee "$LOGS/$LOGTARGET-$1-$2.log" | sed -e "s/^/$LOGTARGET-$1-$2.log: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$2.err" | sed -e "s/^/$LOGTARGET-$1-$2.err: /" 1>&2)
+    "$@" > >(tee "$LOGS/$LOGTARGET-$1-$2_log.txt" | sed -e "s/^/$LOGTARGET-$1-$2_log.txt: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$2_err.txt" | sed -e "s/^/$LOGTARGET-$1-$2_err.txt: /" 1>&2)
   }
 
   # Log command output - take log target name from command name and second argument (like log_1_3 ocaml setup.ml -configure => log target is "<module>-ocaml--configure")
   log_1_3() {
     { local -; set +x; } 2> /dev/null
-    "$@" > >(tee "$LOGS/$LOGTARGET-$1-$3.log" | sed -e "s/^/$LOGTARGET-$1-$3.log: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$3.err" | sed -e "s/^/$LOGTARGET-$1-$3.err: /" 1>&2)
+    "$@" > >(tee "$LOGS/$LOGTARGET-$1-$3_log.txt" | sed -e "s/^/$LOGTARGET-$1-$3_log.txt: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$3_err.txt" | sed -e "s/^/$LOGTARGET-$1-$3_err.txt: /" 1>&2)
   }
 
   # Log command output - log target name is first argument (like logn untar tar xvaf ... => log target is "<module>-untar")
@@ -206,7 +206,7 @@ else
     { local -; set +x; } 2> /dev/null
     LOGTARGETEX=$1
     shift
-    "$@" > >(tee "$LOGS/$LOGTARGET-$LOGTARGETEX.log" | sed -e "s/^/$LOGTARGET-$LOGTARGETEX.log: /") 2> >(tee "$LOGS/$LOGTARGET-$LOGTARGETEX.err" | sed -e "s/^/$LOGTARGET-$LOGTARGETEX.err: /" 1>&2)
+    "$@" > >(tee "$LOGS/$LOGTARGET-${LOGTARGETEX}_log.txt" | sed -e "s/^/$LOGTARGET-${LOGTARGETEX}_log.txt: /") 2> >(tee "$LOGS/$LOGTARGET-${LOGTARGETEX}_err.txt" | sed -e "s/^/$LOGTARGET-${LOGTARGETEX}_err.txt: /" 1>&2)
   }
 fi
 
@@ -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,12 @@ 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=
 
@@ -368,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"
 
@@ -409,7 +426,7 @@ function build_prep_overlay {
       # $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"
+  build_prep "$url" "$ver" tar.gz 1 "$1-$ver" "$1"
 }
 
 # ------------------------------------------------------------------------------
@@ -666,6 +683,17 @@ function installer_addon_end {
   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/g'
+}
+
 ###################### MODULE BUILD FUNCTIONS #####################
 
 ##### SED #####
@@ -1343,11 +1371,10 @@ function copy_coq_license {
     install -D doc/LICENSE                    "$PREFIXCOQ/license_readme/coq/LicenseDoc.txt"
     install -D LICENSE                        "$PREFIXCOQ/license_readme/coq/License.txt"
     install -D plugins/micromega/LICENSE.sos  "$PREFIXCOQ/license_readme/coq/LicenseMicromega.txt"
-    install -D README                         "$PREFIXCOQ/license_readme/coq/ReadMe.txt" || true
-    install -D README.md                      "$PREFIXCOQ/license_readme/coq/ReadMe.md" || true
-    install -D README.win                     "$PREFIXCOQ/license_readme/coq/ReadMeWindows.txt" || true
-    install -D README.doc                     "$PREFIXCOQ/license_readme/coq/ReadMeDoc.txt" || true
-    install -D CHANGES                        "$PREFIXCOQ/license_readme/coq/Changes.txt"
+    # FIXME: this is not the micromega license
+    # It only applies to code that was copied into one single file!
+    install -D README.md                      "$PREFIXCOQ/license_readme/coq/ReadMe.md"
+    install -D CHANGES.md                     "$PREFIXCOQ/license_readme/coq/Changes.md"
     install -D INSTALL                        "$PREFIXCOQ/license_readme/coq/Install.txt"
     install -D doc/README.md                  "$PREFIXCOQ/license_readme/coq/ReadMeDoc.md" || true
   fi
@@ -1620,7 +1647,7 @@ 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
+    # Note: PATH is automatically saved/restored by build_prep / build_post
     PATH=$COQBIN:$PATH
     logn coq_makefile ${COQBIN}coq_makefile -f _CoqProject -o Makefile
     log1 make
@@ -1668,7 +1695,7 @@ function make_addon_ssreflect {
 function make_addon_ltac2 {
   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" ""
+    installer_addon_section ltac2 "Ltac-2" "Coq plugin with the Ltac-2 enhanced tactic language" ""
     log1 make all
     log2 make install
     build_post
@@ -1680,6 +1707,7 @@ function make_addon_ltac2 {
 function make_addon_unicoq {
   installer_addon_dependency unicoq
   if build_prep_overlay unicoq; then
+    installer_addon_section unicoq "Unicoq" "Coq plugin for an enhanced unification algorithm" ""
     log1 coq_makefile -f Make -o Makefile
     log1 make
     log2 make install
@@ -1694,6 +1722,7 @@ function make_addon_mtac2 {
   make_addon_unicoq
   installer_addon_dependency_end
   if build_prep_overlay mtac2; then
+    installer_addon_section mtac2 "Mtac-2" "Coq plugin for a typed tactic language for Coq." ""
     log1 coq_makefile -f _CoqProject -o Makefile
     log1 make
     log2 make install
@@ -1778,8 +1807,8 @@ function install_addon_vst {
     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_glob "veric" '*.v' "$VSTDEST/veric/"
+    install_glob "veric" '*.vo' "$VSTDEST/veric/"
 
     # Install VST documentation files
     install_glob "." 'LICENSE' "$VSTDEST"
@@ -1792,11 +1821,20 @@ function install_addon_vst {
     install_glob "." '_CoqProject-export' "$VSTDEST/progs"
 }
 
+function vst_patch_compcert_refs {
+  find . -type f -name '*.v' -print0 | xargs -0 sed -E -i \
+    -e 's/(Require\s+(Import\s+|Export\s+)*)compcert\./\1VST.compcert./g' \
+    -e 's/From compcert Require/From VST.compcert Require/g'
+}
+
 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 make IGNORECOQVERSION=true $MAKE_OPT
+    # log1 coq_set_timeouts_1000
+    log1 vst_patch_compcert_refs
+    # The usage of the shell variable ARCH in VST collides with the usage in this shellscript
+    logn make env -u ARCH make IGNORECOQVERSION=true $MAKE_OPT
     log1 install_addon_vst
     build_post
   fi