aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci')
-rwxr-xr-xdev/ci/ci-basic-overlay.sh12
-rw-r--r--dev/ci/ci-common.sh34
-rwxr-xr-xdev/ci/ci-deriving.sh8
-rwxr-xr-xdev/ci/ci-fcsl_pcm.sh2
-rwxr-xr-xdev/ci/ci-flocq.sh8
-rwxr-xr-xdev/ci/ci-geocoq.sh2
-rwxr-xr-xdev/ci/ci-iris.sh4
-rwxr-xr-xdev/ci/ci-quickchick.sh4
-rw-r--r--dev/ci/docker/bionic_coq/Dockerfile4
-rw-r--r--dev/ci/user-overlays/13852-Lysxia-no-collision-projection.sh1
-rw-r--r--dev/ci/user-overlays/13912-pi8027-remove-bijint.sh1
-rw-r--r--dev/ci/user-overlays/13958-gares-recordops-api.sh6
-rw-r--r--dev/ci/user-overlays/14050-SkySkimmer-no-remote-counter-alt.sh1
-rw-r--r--dev/ci/user-overlays/14111-gares-update-elpi.sh2
14 files changed, 39 insertions, 50 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 8bcbd90f0b..0093b5fca2 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"
########################################################################
@@ -141,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
@@ -249,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
@@ -308,3 +307,8 @@ project sf "https://github.com/DeepSpec/sf" "master"
# Coqtail
########################################################################
project coqtail "https://github.com/whonore/Coqtail" "master"
+
+########################################################################
+# Deriving
+########################################################################
+project deriving "https://github.com/arthuraa/deriving" "master"
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 8d8f78e10c..6d1e6d788a 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -138,38 +138,8 @@ make()
if [ -z "${MAKEFLAGS+x}" ] && [ -n "${NJOBS}" ];
then
# Not submake and parallel make requested
- command make --output-sync -j "$NJOBS" "$@"
+ command make -j "$NJOBS" "$@"
else
- command make --output-sync "$@"
+ command make "$@"
fi
}
-
-# this installs just the ssreflect library of math-comp
-install_ssreflect()
-{
- echo 'Installing ssreflect'
-
- git_download mathcomp
-
- ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp/ssreflect" && \
- make && \
- make install )
-
-}
-
-# this installs just the ssreflect + algebra library of math-comp
-install_ssralg()
-{
- echo 'Installing ssralg'
-
- git_download mathcomp
-
- ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && \
- make -C ssreflect && \
- make -C ssreflect install && \
- make -C fingroup && \
- make -C fingroup install && \
- make -C algebra && \
- make -C algebra install )
-
-}
diff --git a/dev/ci/ci-deriving.sh b/dev/ci/ci-deriving.sh
new file mode 100755
index 0000000000..c34fc44f69
--- /dev/null
+++ b/dev/ci/ci-deriving.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download deriving
+
+( cd "${CI_BUILD_DIR}/deriving" && make && make tests && make install )
diff --git a/dev/ci/ci-fcsl_pcm.sh b/dev/ci/ci-fcsl_pcm.sh
index cb951630c8..e1248c6627 100755
--- a/dev/ci/ci-fcsl_pcm.sh
+++ b/dev/ci/ci-fcsl_pcm.sh
@@ -3,8 +3,6 @@
ci_dir="$(dirname "$0")"
. "${ci_dir}/ci-common.sh"
-install_ssreflect
-
git_download fcsl_pcm
( cd "${CI_BUILD_DIR}/fcsl_pcm" && make )
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 )
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
index e4fc983e68..0ad9ac0cbb 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -3,8 +3,6 @@
ci_dir="$(dirname "$0")"
. "${ci_dir}/ci-common.sh"
-install_ssralg
-
git_download geocoq
( cd "${CI_BUILD_DIR}/geocoq" && ./configure.sh && make )
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 08686d7ced..62623f4c39 100755
--- a/dev/ci/ci-quickchick.sh
+++ b/dev/ci/ci-quickchick.sh
@@ -3,8 +3,6 @@
ci_dir="$(dirname "$0")"
. "${ci_dir}/ci-common.sh"
-install_ssreflect
-
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/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 8f14625c63..00729cd168 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -24,7 +24,7 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
texlive-science tipa
# More dependencies of the sphinx doc, pytest for coqtail
-RUN pip3 install sphinx==2.3.1 sphinx_rtd_theme==0.4.3 \
+RUN pip3 install docutils==0.16 sphinx==2.3.1 sphinx_rtd_theme==0.4.3 \
antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.2 \
pytest==5.4.3
@@ -44,7 +44,7 @@ ENV COMPILER="4.05.0"
# Common OPAM packages
ENV BASE_OPAM="zarith.1.10 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.1" \
CI_OPAM="ocamlgraph.1.8.8" \
- BASE_ONLY_OPAM="elpi.1.13.0"
+ BASE_ONLY_OPAM="elpi.1.13.1"
# BASE switch; CI_OPAM contains Coq's CI dependencies.
ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.0"
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/ci/user-overlays/13912-pi8027-remove-bijint.sh b/dev/ci/user-overlays/13912-pi8027-remove-bijint.sh
new file mode 100644
index 0000000000..d860cfec01
--- /dev/null
+++ b/dev/ci/user-overlays/13912-pi8027-remove-bijint.sh
@@ -0,0 +1 @@
+overlay elpi https://github.com/pi8027/coq-elpi coq-overlay-13912 13912
diff --git a/dev/ci/user-overlays/13958-gares-recordops-api.sh b/dev/ci/user-overlays/13958-gares-recordops-api.sh
new file mode 100644
index 0000000000..0ec50a1dda
--- /dev/null
+++ b/dev/ci/user-overlays/13958-gares-recordops-api.sh
@@ -0,0 +1,6 @@
+overlay metacoq https://github.com/gares/metacoq recordops-api 13958
+overlay mtac2 https://github.com/gares/Mtac2 recordops-api 13958
+overlay elpi https://github.com/gares/coq-elpi recordops-api 13958
+overlay unicoq https://github.com/gares/unicoq recordops-api 13958
+overlay equations https://github.com/gares/Coq-Equations recordops-api 13958
+overlay hierarchy_builder https://github.com/gares/hierarchy-builder coq-master 13958
diff --git a/dev/ci/user-overlays/14050-SkySkimmer-no-remote-counter-alt.sh b/dev/ci/user-overlays/14050-SkySkimmer-no-remote-counter-alt.sh
new file mode 100644
index 0000000000..d1606711dc
--- /dev/null
+++ b/dev/ci/user-overlays/14050-SkySkimmer-no-remote-counter-alt.sh
@@ -0,0 +1 @@
+overlay metacoq https://github.com/SkySkimmer/metacoq no-remote-counter-alt 14050
diff --git a/dev/ci/user-overlays/14111-gares-update-elpi.sh b/dev/ci/user-overlays/14111-gares-update-elpi.sh
new file mode 100644
index 0000000000..8827127a38
--- /dev/null
+++ b/dev/ci/user-overlays/14111-gares-update-elpi.sh
@@ -0,0 +1,2 @@
+overlay elpi https://github.com/LPCIC/coq-elpi coq-master+1.9.5 14111
+overlay hierarchy_builder https://github.com/math-comp/hierarchy-builder coq-master+1.1.0 14111
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 01:52:23 +0000