Merge PR #9192: Issue #9175, #9190, #9191 (various minor Windows build issues)

Reviewed-by: Zimmi48

3 files changed, 45 insertions, 23 deletions

diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index b202635714..07a13b8204 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -691,7 +691,7 @@ function installer_addon_end {
 # ------------------------------------------------------------------------------
 
 function coq_set_timeouts_1000 {
-  find . -type f -name '*.v' -print0 | xargs -0 sed -i 's/timeout\s\+[0-9]\+/timeout 1000/'
+  find . -type f -name '*.v' -print0 | xargs -0 sed -i 's/timeout\s\+[0-9]\+/timeout 1000/g'
 }
 
 ###################### MODULE BUILD FUNCTIONS #####################
@@ -701,7 +701,7 @@ function coq_set_timeouts_1000 {
 function make_sed {
   if build_prep https://ftp.gnu.org/gnu/sed/  sed-4.2.2  tar.gz ; then
     logn configure ./configure
-    log1 make
+    log1 make $MAKE_OPT
     log2 make install
     log2 make clean
     build_post
@@ -1107,7 +1107,7 @@ function make_ocamlbuild {
   make_ocaml
   if build_prep https://github.com/ocaml/ocamlbuild/archive 0.12.0 tar.gz 1 ocamlbuild-0.12.0; then
     log2 make configure OCAML_NATIVE=true OCAMLBUILD_PREFIX=$PREFIXOCAML OCAMLBUILD_BINDIR=$PREFIXOCAML/bin OCAMLBUILD_LIBDIR=$PREFIXOCAML/lib
-    log1 make
+    log1 make $MAKE_OPT
     log2 make install
     build_post
   fi
@@ -1634,7 +1634,7 @@ function make_addon_bignums {
     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
+    log1 make $MAKE_OPT all
     log2 make install
     build_post
   fi
@@ -1650,7 +1650,7 @@ function make_addon_equations {
     # 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
+    log1 make $MAKE_OPT
     log2 make install
     build_post
   fi
@@ -1696,7 +1696,7 @@ 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 tactic language" ""
-    log1 make all
+    log1 make $MAKE_OPT all
     log2 make install
     build_post
   fi
@@ -1709,7 +1709,7 @@ function make_addon_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
+    log1 make $MAKE_OPT
     log2 make install
     build_post
   fi
@@ -1724,7 +1724,7 @@ function make_addon_mtac2 {
   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
+    log1 make $MAKE_OPT
     log2 make install
     build_post
   fi
@@ -1766,7 +1766,7 @@ function make_addon_menhirlib {
     echo -R . MenhirLib > _CoqProject
     ls -1 *.v >> _CoqProject
     log1 coq_makefile -f _CoqProject -o Makefile.coq
-    log1 make -f Makefile.coq all
+    log1 make -f Makefile.coq $MAKE_OPT all
     logn make-install make -f Makefile.coq install
     build_post
   fi
@@ -1779,10 +1779,10 @@ function make_addon_compcert {
   make_menhir
   make_addon_menhirlib
   installer_addon_dependency_end
-  if build_prep_overlay CompCert; then
+  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
+    log1 make $MAKE_OPT
     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"
@@ -1807,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"
@@ -1821,12 +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
+  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 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
@@ -1851,9 +1859,9 @@ function make_addon_coquelicot {
 
 function make_addon_aactactics {
   installer_addon_dependency aac
-  if build_prep_overlay aactactics; then
+  if build_prep_overlay aac_tactics; then
     installer_addon_section aac "AAC" "Coq plugin for extensible associative and commutative rewriting" ""
-    log1 make
+    log1 make $MAKE_OPT
     log2 make install
     build_post
   fi
@@ -1894,7 +1902,7 @@ function make_addon_quickchick {
   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
+    log1 make $MAKE_OPT
     log2 make install
     build_post
   fi
diff --git a/dev/build/windows/patches_coq/VST.patch b/dev/build/windows/patches_coq/VST.patch
new file mode 100755
index 0000000000..2c8c46373f
--- /dev/null
+++ b/dev/build/windows/patches_coq/VST.patch
@@ -0,0 +1,15 @@
+diff --git a/Makefile b/Makefile
+index 4a119042..fdfac13e 100755
+--- a/Makefile
++++ b/Makefile
+@@ -76,8 +76,8 @@ endif
+
+ COMPCERTDIRS=lib common $(ARCHDIRS) cfrontend flocq exportclight $(BACKEND)
+
+-COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT)/$(d) compcert.$(d))
+-EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT)/$(d) compcert.$(d))
++COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT)/$(d) VST.compcert.$(d))
++EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT)/$(d) VST.compcert.$(d))
+
+ # for SSReflect
+ ifdef MATHCOMP
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index 386a3de204..2a42a6b58e 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -49,10 +49,9 @@ IF "%WINDOWS%" == "enabled_all_addons" (
     -addon=compcert ^

     -addon=extlib ^

     -addon=quickchick ^

-    -addon=coquelicot

-  REM addons with build issues

-  REM -addon=vst ^

-  REM -addon=aactactics ^

+    -addon=coquelicot ^

+    -addon=vst ^

+    -addon=aactactics

 ) ELSE (

   SET "EXTRA_ADDONS= "

 )