aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rwxr-xr-xdev/build/windows/makecoq_mingw.sh46
-rwxr-xr-xdev/build/windows/patches_coq/VST.patch15
-rwxr-xr-xdev/ci/gitlab.bat7
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= "
)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:44:40 +0000