aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
authorMaxime Dénès2020-02-03 18:19:42 +0100
committerMaxime Dénès2020-07-06 11:22:43 +0200
commit0ea2d0ff4ed84e1cc544c958b8f6e98f6ba2e9b6 (patch)
treefbad060c3c2e29e81751dea414c898b5cb0fa22d /dev/ci
parentcf388fdb679adb88a7e8b3122f65377552d2fb94 (diff)
Primitive persistent arrays
Persistent arrays expose a functional interface but are implemented using an imperative data structure. The OCaml implementation is based on Jean-Christophe Filliâtre's. Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Diffstat (limited to 'dev/ci')
-rw-r--r--dev/ci/user-overlays/11604-persistent-arrays.sh18
1 files changed, 18 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/11604-persistent-arrays.sh b/dev/ci/user-overlays/11604-persistent-arrays.sh
new file mode 100644
index 0000000000..aec5c4fa3d
--- /dev/null
+++ b/dev/ci/user-overlays/11604-persistent-arrays.sh
@@ -0,0 +1,18 @@
+if [ "$CI_PULL_REQUEST" = "11604" ] || [ "$CI_BRANCH" = "persistent-arrays" ]; then
+
+ unicoq_CI_REF=persistent-arrays
+ unicoq_CI_GITURL=https://github.com/maximedenes/unicoq
+
+ elpi_CI_REF=persistent-arrays
+ elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi
+
+ #relation_algebra_CI_REF=persistent-arrays
+ #relation_algebra_CI_GITURL=https://github.com/maximedenes/relation-algebra
+
+ coqhammer_CI_REF=persistent-arrays
+ coqhammer_CI_GITURL=https://github.com/maximedenes/coqhammer
+
+ metacoq_CI_REF=persistent-arrays
+ metacoq_CI_GITURL=https://github.com/maximedenes/metacoq
+
+fi