aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rwxr-xr-xdev/ci/ci-basic-overlay.sh2
-rwxr-xr-xdev/ci/ci-iris.sh4
-rwxr-xr-xdev/ci/ci-quickchick.sh2
-rw-r--r--dev/ci/user-overlays/13852-Lysxia-no-collision-projection.sh1
-rwxr-xr-xdev/dune-dbg.in2
-rw-r--r--dev/top_printers.dbg1
6 files changed, 3 insertions, 9 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 4799755b15..67555da0a2 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -79,8 +79,6 @@ project iris "https://gitlab.mpi-sws.org/iris/iris" ""
project autosubst "https://github.com/coq-community/autosubst" "master"
-project iris_string_ident "https://gitlab.mpi-sws.org/iris/string-ident" "master"
-
project iris_examples "https://gitlab.mpi-sws.org/iris/examples" "master"
########################################################################
diff --git a/dev/ci/ci-iris.sh b/dev/ci/ci-iris.sh
index d29e6f1635..7a72462758 100755
--- a/dev/ci/ci-iris.sh
+++ b/dev/ci/ci-iris.sh
@@ -5,7 +5,6 @@ ci_dir="$(dirname "$0")"
# Setup iris_examples and separate dependencies first
git_download autosubst
-git_download iris_string_ident
git_download iris_examples
# Extract required version of Iris (avoiding "+" which does not work on MacOS :( *)
@@ -31,8 +30,5 @@ git_download stdpp
# Build autosubst
( cd "${CI_BUILD_DIR}/autosubst" && make && make install )
-# Build iris-string-ident
-( cd "${CI_BUILD_DIR}/iris_string_ident" && make && make install )
-
# Build Iris examples
( cd "${CI_BUILD_DIR}/iris_examples" && make && make install )
diff --git a/dev/ci/ci-quickchick.sh b/dev/ci/ci-quickchick.sh
index 2bc2a18849..62623f4c39 100755
--- a/dev/ci/ci-quickchick.sh
+++ b/dev/ci/ci-quickchick.sh
@@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")"
git_download quickchick
-( cd "${CI_BUILD_DIR}/quickchick" && make && make install)
+( cd "${CI_BUILD_DIR}/quickchick" && make && make install-plugin)
diff --git a/dev/ci/user-overlays/13852-Lysxia-no-collision-projection.sh b/dev/ci/user-overlays/13852-Lysxia-no-collision-projection.sh
new file mode 100644
index 0000000000..9b8d1a63d9
--- /dev/null
+++ b/dev/ci/user-overlays/13852-Lysxia-no-collision-projection.sh
@@ -0,0 +1 @@
+overlay compcert https://github.com/Lysxia/CompCert no-collision-projection 13852
diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in
index 47dfbad3a0..cc8574c6d6 100755
--- a/dev/dune-dbg.in
+++ b/dev/dune-dbg.in
@@ -26,4 +26,4 @@ esac
emacs="${INSIDE_EMACS:+-emacs}"
-ocamldebug $emacs $(ocamlfind query -recursive -i-format coq.top_printers) -I +threads -I dev $exe "$@"
+ocamldebug $emacs $(ocamlfind query -recursive -i-format coq-core.top_printers) -I +threads -I dev $exe "$@"
diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg
index fe95a59d9b..5d37c60bca 100644
--- a/dev/top_printers.dbg
+++ b/dev/top_printers.dbg
@@ -12,7 +12,6 @@ install_printer Top_printers.ppmind
install_printer Top_printers.ppind
install_printer Top_printers.ppsp
install_printer Top_printers.ppqualid
-install_printer Top_printers.ppclindex
install_printer Top_printers.ppscheme
install_printer Top_printers.ppwf_paths
install_printer Top_printers.ppevar