aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rwxr-xr-xdev/ci/ci-basic-overlay.sh5
-rwxr-xr-xdev/ci/ci-flocq.sh8
2 files changed, 10 insertions, 3 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 67555da0a2..0093b5fca2 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -139,7 +139,8 @@ project compcert "https://github.com/AbsInt/CompCert" "master"
########################################################################
# VST
########################################################################
-project vst "https://github.com/PrincetonUniversity/VST" "master"
+# todo: 2021 03 11: switch back to master once vst merges the compcert3.9 branch
+project vst "https://github.com/PrincetonUniversity/VST" "compcert3.9"
########################################################################
# cross-crypto
@@ -247,7 +248,7 @@ project reduction_effects "https://github.com/coq-community/reduction-effects" "
# menhirlib
########################################################################
# Note: menhirlib is now in subfolder coq-menhirlib of menhir
-project menhirlib "https://gitlab.inria.fr/fpottier/menhir" "20201122"
+project menhirlib "https://gitlab.inria.fr/fpottier/menhir" "20210310"
########################################################################
# aac_tactics
diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh
index cb6c3e6452..01723e5b5c 100755
--- a/dev/ci/ci-flocq.sh
+++ b/dev/ci/ci-flocq.sh
@@ -5,4 +5,10 @@ ci_dir="$(dirname "$0")"
git_download flocq
-( cd "${CI_BUILD_DIR}/flocq" && ( if [ ! -x ./configure ]; then autoconf && ./configure; fi ) && ./remake "-j${NJOBS}" && ./remake install )
+( cd "${CI_BUILD_DIR}/flocq"
+ ( if [ ! -x ./configure ]; then
+ autoconf
+ ./configure COQEXTRAFLAGS="-compat 8.13";
+ fi )
+ ./remake "-j${NJOBS}"
+ ./remake install )