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
-rw-r--r--dev/ci/README-developers.md10
-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.bat9
-rwxr-xr-xdev/lint-repository.sh28
-rwxr-xr-xdev/tools/merge-pr.sh20
12 files changed, 139 insertions, 81 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/README-developers.md b/dev/ci/README-developers.md
index fa8962a06f..6663fbecf8 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -10,12 +10,14 @@ We are currently running tests on the following platforms:
- GitLab CI is the main CI platform. It tests the compilation of Coq,
of the documentation, and of CoqIDE on Linux with several versions
of OCaml and with warnings as errors; it runs the test-suite and
- tests the compilation of several external developments.
+ tests the compilation of several external developments. It also runs
+ a linter that checks whitespace discipline. A [pre-commit
+ hook](../tools/pre-commit) is automatically installed by
+ `./configure`. It should allow complying with this discipline
+ without pain.
- Travis CI is used to test the compilation of Coq and run the test-suite on
- macOS. It also runs a linter that checks whitespace discipline. A
- [pre-commit hook](../tools/pre-commit) is automatically installed by
- `./configure`. It should allow complying with this discipline without pain.
+ macOS.
- AppVeyor is used to test the compilation of Coq and run the test-suite on
Windows.
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..5f819f31f9 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -26,12 +26,12 @@ if %ARCH% == 64 (
SET CYGROOT=C:\ci\cygwin%ARCH%
SET DESTCOQ=C:\ci\coq%ARCH%
+SET CYGCACHE=C:\ci\cache\cgwin
CALL :MakeUniqueFolder %CYGROOT% CYGROOT
CALL :MakeUniqueFolder %DESTCOQ% DESTCOQ
powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/%SETUP%', '%SETUP%')"
-SET CYGCACHE=%CYGROOT%\var\cache\setup
SET CI_PROJECT_DIR_MFMT=%CI_PROJECT_DIR:\=/%
SET CI_PROJECT_DIR_CFMT=%CI_PROJECT_DIR_MFMT:C:/=/cygdrive/c/%
SET COQREGTESTING=Y
@@ -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/lint-repository.sh b/dev/lint-repository.sh
index cd09b6d305..f588c20d02 100755
--- a/dev/lint-repository.sh
+++ b/dev/lint-repository.sh
@@ -4,33 +4,25 @@
# lint-commits.sh seeks to prevent the worsening of already present
# problems, such as tab indentation in ml files. lint-repository.sh
-# seeks to prevent the (re-)introduction of solved problems, such as
-# newlines at the end of .v files.
+# also seeks to prevent the (re-)introduction of solved problems, such
+# as newlines at the end of .v files.
CODE=0
-if [ -n "${TRAVIS_PULL_REQUEST}" ] && [ "${TRAVIS_PULL_REQUEST}" != false ];
-then
- # skip PRs from before the linter existed
- if [ -z "$(git ls-tree --name-only "${TRAVIS_PULL_REQUEST_SHA}" dev/lint-commits.sh)" ];
- then
- 1>&2 echo "Linting skipped: pull request older than the linter."
- exit 0
- fi
-
- # Some problems are too widespread to fix in one commit, but we
- # can still check that they don't worsen.
- CUR_HEAD=${TRAVIS_COMMIT_RANGE%%...*}
- PR_HEAD=${TRAVIS_COMMIT_RANGE##*...}
- MERGE_BASE=$(git merge-base "$CUR_HEAD" "$PR_HEAD")
- dev/lint-commits.sh "$MERGE_BASE" "$PR_HEAD" || CODE=1
-fi
+# We assume that all merge commits are from the main branch
+# For Coq it is extremely rare for this assumption to be broken
+read -r base < <(git log -n 1 --merges --pretty='format:%H')
+head=$(git rev-parse HEAD)
+
+dev/lint-commits.sh "$base" "$head" || CODE=1
# Check that the files with 'whitespace' gitattribute end in a newline.
# xargs exit status is 123 if any file failed the test
+echo Checking end of file newlines
find . "(" -path ./.git -prune ")" -o -type f -print0 |
xargs -0 dev/tools/check-eof-newline.sh || CODE=1
+echo Checking overlays
dev/tools/check-overlays.sh || CODE=1
exit $CODE
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-05-02 00:45:15 +0000