From c4a3c98e32175831478e09ddebe6c301bbad6fe9 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop Date: Tue, 11 Dec 2018 13:01:12 +0100 Subject: Fix issue #9175 Windows: VST addon does not work if CompCert is also installed --- dev/build/windows/makecoq_mingw.sh | 18 +++++++++++++----- dev/build/windows/patches_coq/VST.patch | 15 +++++++++++++++ 2 files changed, 28 insertions(+), 5 deletions(-) create mode 100755 dev/build/windows/patches_coq/VST.patch (limited to 'dev/build') 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 -- cgit v1.2.3 From 017ef807492f4ad21ee0a02f0ca5cfc35fe41122 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop Date: Tue, 11 Dec 2018 13:54:52 +0100 Subject: Fix issue #9190 : Windows: overlay names changed in ci-basic-overlay.sh but have not been adjusted in make_coq_mingw.sh --- dev/build/windows/makecoq_mingw.sh | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'dev/build') diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 601a16de83..4da61303a4 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1779,7 +1779,7 @@ 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 @@ -1829,7 +1829,7 @@ function vst_patch_compcert_refs { 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 vst_patch_compcert_refs @@ -1859,7 +1859,7 @@ 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 log2 make install -- cgit v1.2.3 From ccd5cf3c0fa3248bcfc6c37b5693fc0e5ea6ac61 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop Date: Tue, 11 Dec 2018 14:01:46 +0100 Subject: Fix issue #9191 : Windows: parallel build is not enabled for some modules which support it --- dev/build/windows/makecoq_mingw.sh | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) (limited to 'dev/build') diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 4da61303a4..07a13b8204 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -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 @@ -1782,7 +1782,7 @@ function make_addon_compcert { 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" @@ -1861,7 +1861,7 @@ function make_addon_aactactics { installer_addon_dependency aac 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 @@ -1902,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 -- cgit v1.2.3