Fix issue #9175 Windows: VST addon does not work if CompCert is also installed

2 files changed, 28 insertions, 5 deletions

diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index b202635714..601a16de83 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 #####################
@@ -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
     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
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