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/ci-basic-overlay.sh38
-rwxr-xr-xdev/ci/ci-fiat-crypto-legacy.sh4
-rwxr-xr-xdev/ci/ci-fiat-crypto.sh6
-rwxr-xr-xdev/ci/ci-formal-topology.sh8
-rwxr-xr-xdev/ci/ci-plugin_tutorial.sh12
-rwxr-xr-xdev/ci/ci-verdi-raft.sh24
-rwxr-xr-xdev/ci/gitlab.bat7
-rwxr-xr-xdev/tools/merge-pr.sh20
10 files changed, 122 insertions, 58 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/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index e0f4f50fa9..8dee465cf4 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -150,11 +150,11 @@
: "${fiat_crypto_CI_ARCHIVEURL:=${fiat_crypto_CI_GITURL}/archive}"
########################################################################
-# formal-topology
+# fiat_crypto_legacy
########################################################################
-: "${formal_topology_CI_REF:=ci}"
-: "${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology}"
-: "${formal_topology_CI_ARCHIVEURL:=${formal_topology_CI_GITURL}/archive}"
+: "${fiat_crypto_legacy_CI_REF:=sp2019latest}"
+: "${fiat_crypto_legacy_CI_GITURL:=https://github.com/mit-plv/fiat-crypto}"
+: "${fiat_crypto_legacy_CI_ARCHIVEURL:=${fiat_crypto_legacy_CI_GITURL}/archive}"
########################################################################
# coq_dpdgraph
@@ -240,13 +240,6 @@
: "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}"
########################################################################
-# plugin_tutorial
-########################################################################
-: "${plugin_tutorial_CI_REF:=master}"
-: "${plugin_tutorial_CI_GITURL:=https://github.com/ybertot/plugin_tutorials}"
-: "${plugin_tutorial_CI_ARCHIVEURL:=${plugin_tutorial_CI_GITURL}/archive}"
-
-########################################################################
# menhirlib
########################################################################
: "${menhirlib_CI_REF:=master}"
@@ -273,3 +266,26 @@
: "${relation_algebra_CI_REF:=master}"
: "${relation_algebra_CI_GITURL:=https://github.com/damien-pous/relation-algebra}"
: "${relation_algebra_CI_ARCHIVEURL:=${relation_algebra_CI_GITURL}/archive}"
+
+########################################################################
+# StructTact + InfSeqExt + Cheerios + Verdi + Verdi Raft
+########################################################################
+: "${struct_tact_CI_REF:=master}"
+: "${struct_tact_CI_GITURL:=https://github.com/uwplse/StructTact}"
+: "${struct_tact_CI_ARCHIVEURL:=${struct_tact_CI_GITURL}/archive}"
+
+: "${inf_seq_ext_CI_REF:=master}"
+: "${inf_seq_ext_CI_GITURL:=https://github.com/DistributedComponents/InfSeqExt}"
+: "${inf_seq_ext_CI_ARCHIVEURL:=${inf_seq_ext_CI_GITURL}/archive}"
+
+: "${cheerios_CI_REF:=master}"
+: "${cheerios_CI_GITURL:=https://github.com/uwplse/cheerios}"
+: "${cheerios_CI_ARCHIVEURL:=${cheerios_CI_GITURL}/archive}"
+
+: "${verdi_CI_REF:=master}"
+: "${verdi_CI_GITURL:=https://github.com/uwplse/verdi}"
+: "${verdi_CI_ARCHIVEURL:=${verdi_CI_GITURL}/archive}"
+
+: "${verdi_raft_CI_REF:=master}"
+: "${verdi_raft_CI_GITURL:=https://github.com/uwplse/verdi-raft}"
+: "${verdi_raft_CI_ARCHIVEURL:=${verdi_raft_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh
index 6bf3138346..2af4b58201 100755
--- a/dev/ci/ci-fiat-crypto-legacy.sh
+++ b/dev/ci/ci-fiat-crypto-legacy.sh
@@ -4,11 +4,11 @@ ci_dir="$(dirname "$0")"
. "${ci_dir}/ci-common.sh"
FORCE_GIT=1
-git_download fiat_crypto
+git_download fiat_crypto_legacy
fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite old-pipeline-lite lite-display"
fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem old-pipeline-nobigmem nonautogenerated-specific nonautogenerated-specific-display"
-( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \
+( cd "${CI_BUILD_DIR}/fiat_crypto_legacy" && git submodule update --init --recursive && \
./etc/ci/remove_autogenerated.sh && \
make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} )
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index 7e8013be9b..bba17314f7 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -10,5 +10,9 @@ git_download fiat_crypto
# building the executables.
# c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241
+fiat_crypto_CI_TARGETS1="c-files printlite lite"
+fiat_crypto_CI_TARGETS2="print-nobigmem nobigmem"
+
( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \
- ulimit -s 32768 && make new-pipeline c-files )
+ ulimit -s 32768 && \
+ make ${fiat_crypto_CI_TARGETS1} && make -j 1 ${fiat_crypto_CI_TARGETS2} )
diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh
deleted file mode 100755
index 8be5a06ed2..0000000000
--- a/dev/ci/ci-formal-topology.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-. "${ci_dir}/ci-common.sh"
-
-git_download formal_topology
-
-( cd "${CI_BUILD_DIR}/formal_topology" && make )
diff --git a/dev/ci/ci-plugin_tutorial.sh b/dev/ci/ci-plugin_tutorial.sh
deleted file mode 100755
index 6c26a71a21..0000000000
--- a/dev/ci/ci-plugin_tutorial.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-. "${ci_dir}/ci-common.sh"
-
-git_download plugin_tutorial
-
-( cd "${CI_BUILD_DIR}/plugin_tutorial" && \
- pushd tuto0 && make && popd && \
- pushd tuto1 && make && popd && \
- pushd tuto2 && make && popd && \
- pushd tuto3 && make && popd )
diff --git a/dev/ci/ci-verdi-raft.sh b/dev/ci/ci-verdi-raft.sh
new file mode 100755
index 0000000000..3bcd52c464
--- /dev/null
+++ b/dev/ci/ci-verdi-raft.sh
@@ -0,0 +1,24 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download struct_tact
+
+( cd "${CI_BUILD_DIR}/struct_tact" && ./configure && make && make install )
+
+git_download inf_seq_ext
+
+( cd "${CI_BUILD_DIR}/inf_seq_ext" && ./configure && make && make install )
+
+git_download cheerios
+
+( cd "${CI_BUILD_DIR}/cheerios" && ./configure && make && make install )
+
+git_download verdi
+
+( cd "${CI_BUILD_DIR}/verdi" && ./configure && make && make install )
+
+git_download verdi_raft
+
+( cd "${CI_BUILD_DIR}/verdi_raft" && ./configure && make )
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= "
)
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index 5fd8a3b7d9..a27dacc5a7 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -198,8 +198,26 @@ if [ -z "$(git config user.signingkey)" ]; then
warning "gpg will guess a key out of your git config user.* data"
fi
+# Generate commit message
+
+info "Fetching review data"
+reviews=$(curl -s "$API/pulls/$PR/reviews")
+msg="Merge PR #$PR: $TITLE"
+
+has_state() {
+ [ "$(jq -rc 'map(select(.user.login == "'"$1"'") | .state) | any(. == "'"$2"'")' <<< "$reviews")" = true ]
+}
+
+for reviewer in $(jq -rc 'map(.user.login) | unique | join(" ")' <<< "$reviews" ); do
+ if has_state "$reviewer" APPROVED; then
+ msg=$(printf '%s\n' "$msg" | git interpret-trailers --trailer Reviewed-by="$reviewer")
+ elif has_state "$reviewer" COMMENTED; then
+ msg=$(printf '%s\n' "$msg" | git interpret-trailers --trailer Ack-by="$reviewer")
+ fi
+done
+
info "merging"
-git merge -v -S --no-ff FETCH_HEAD -m "Merge PR #$PR: $TITLE" -e
+git merge -v -S --no-ff FETCH_HEAD -m "$msg" -e
# TODO: improve this check
if ! git diff --quiet --diff-filter=A "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci/user-overlays; then
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 12:58:41 +0000