aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci')
-rwxr-xr-xdev/ci/ci-basic-overlay.sh21
-rwxr-xr-xdev/ci/ci-fiat-crypto-legacy.sh14
-rwxr-xr-xdev/ci/ci-fiat-crypto.sh8
-rwxr-xr-xdev/ci/ci-mtac2.sh4
-rwxr-xr-xdev/ci/ci-reduction_effects.sh8
-rwxr-xr-xdev/ci/ci-unicoq.sh8
-rw-r--r--dev/ci/nix/default.nix1
-rw-r--r--dev/ci/nix/fiat_crypto_legacy.nix6
-rw-r--r--dev/ci/user-overlays/10204-rm-unsafe-type-of-coercion.sh6
-rw-r--r--dev/ci/user-overlays/11235-non-maximal-implicit.sh9
-rw-r--r--dev/ci/user-overlays/11417-ppedrot-rm-kind-of-type.sh6
-rw-r--r--dev/ci/user-overlays/11521-SkySkimmer-no-optname.sh15
-rw-r--r--dev/ci/user-overlays/11557-SkySkimmer-template-directify.sh12
13 files changed, 79 insertions, 39 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 9e9e3b4cfa..60c266699c 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -97,11 +97,8 @@
########################################################################
# Coquelicot
########################################################################
-# Modified until https://gitlab.inria.fr/coquelicot/coquelicot/merge_requests/2 is merged
-: "${coquelicot_CI_REF:=fix-rlist-import}"
-: "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/pedrot/coquelicot}"
-# : "${coquelicot_CI_REF:=master}"
-# : "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/coquelicot/coquelicot}"
+: "${coquelicot_CI_REF:=master}"
+: "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/coquelicot/coquelicot}"
: "${coquelicot_CI_ARCHIVEURL:=${coquelicot_CI_GITURL}/-/archive}"
########################################################################
@@ -168,13 +165,6 @@
: "${fiat_crypto_CI_ARCHIVEURL:=${fiat_crypto_CI_GITURL}/archive}"
########################################################################
-# fiat_crypto_legacy
-########################################################################
-: "${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
########################################################################
: "${coq_dpdgraph_CI_REF:=coq-master}"
@@ -259,6 +249,13 @@
: "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}"
########################################################################
+# reduction-effects
+########################################################################
+: "${reduction_effects_CI_REF:=master}"
+: "${reduction_effects_CI_GITURL:=https://github.com/coq-community/reduction-effects}"
+: "${reduction_effects_CI_ARCHIVEURL:=${reduction_effects_CI_GITURL}/archive}"
+
+########################################################################
# menhirlib
########################################################################
: "${menhirlib_CI_REF:=master}"
diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh
deleted file mode 100755
index 2af4b58201..0000000000
--- a/dev/ci/ci-fiat-crypto-legacy.sh
+++ /dev/null
@@ -1,14 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-. "${ci_dir}/ci-common.sh"
-
-FORCE_GIT=1
-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_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 000c418137..811fefda35 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -9,11 +9,15 @@ git_download fiat_crypto
# We need a larger stack size to not overflow ocamlopt+flambda when
# building the executables.
# c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241
+fiat_crypto_CI_STACKSIZE=32768
-fiat_crypto_CI_MAKE_ARGS="EXTERNAL_DEPENDENCIES=1"
+# fiat-crypto is not guaranteed to build with the latest version of
+# bedrock2, so we use the pinned version of bedrock2, but the external
+# version of other developments
+fiat_crypto_CI_MAKE_ARGS="EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1"
fiat_crypto_CI_TARGETS1="${fiat_crypto_CI_MAKE_ARGS} standalone-ocaml c-files rust-files printlite lite"
fiat_crypto_CI_TARGETS2="${fiat_crypto_CI_MAKE_ARGS} all"
( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \
- ulimit -s 32768 && \
+ ulimit -s ${fiat_crypto_CI_STACKSIZE} && \
make ${fiat_crypto_CI_TARGETS1} && make -j 1 ${fiat_crypto_CI_TARGETS2} )
diff --git a/dev/ci/ci-mtac2.sh b/dev/ci/ci-mtac2.sh
index 7075d4d7f6..e08dcf07ab 100755
--- a/dev/ci/ci-mtac2.sh
+++ b/dev/ci/ci-mtac2.sh
@@ -3,10 +3,6 @@
ci_dir="$(dirname "$0")"
. "${ci_dir}/ci-common.sh"
-git_download unicoq
-
-( cd "${CI_BUILD_DIR}/unicoq" && coq_makefile -f Make -o Makefile && make && make install )
-
git_download mtac2
( cd "${CI_BUILD_DIR}/mtac2" && coq_makefile -f _CoqProject -o Makefile && make )
diff --git a/dev/ci/ci-reduction_effects.sh b/dev/ci/ci-reduction_effects.sh
new file mode 100755
index 0000000000..6b6de3fa2f
--- /dev/null
+++ b/dev/ci/ci-reduction_effects.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download reduction_effects
+
+( cd "${CI_BUILD_DIR}/reduction_effects" && make && make test && make install)
diff --git a/dev/ci/ci-unicoq.sh b/dev/ci/ci-unicoq.sh
new file mode 100755
index 0000000000..36acb115e9
--- /dev/null
+++ b/dev/ci/ci-unicoq.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download unicoq
+
+( cd "${CI_BUILD_DIR}/unicoq" && coq_makefile -f Make -o Makefile && make && make install )
diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index f08a08531f..c8ea59f08a 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -91,7 +91,6 @@ let projects = {
cross_crypto = callPackage ./cross_crypto.nix {};
Elpi = callPackage ./Elpi.nix {};
fiat_crypto = callPackage ./fiat_crypto.nix {};
- fiat_crypto_legacy = callPackage ./fiat_crypto_legacy.nix {};
flocq = callPackage ./flocq.nix {};
formal-topology = callPackage ./formal-topology.nix {};
GeoCoq = callPackage ./GeoCoq.nix {};
diff --git a/dev/ci/nix/fiat_crypto_legacy.nix b/dev/ci/nix/fiat_crypto_legacy.nix
deleted file mode 100644
index 3248665579..0000000000
--- a/dev/ci/nix/fiat_crypto_legacy.nix
+++ /dev/null
@@ -1,6 +0,0 @@
-{}:
-
-{
- configure = "./etc/ci/remove_autogenerated.sh";
- make = "make print-old-pipeline-lite old-pipeline-lite lite-display";
-}
diff --git a/dev/ci/user-overlays/10204-rm-unsafe-type-of-coercion.sh b/dev/ci/user-overlays/10204-rm-unsafe-type-of-coercion.sh
new file mode 100644
index 0000000000..87dad61dbc
--- /dev/null
+++ b/dev/ci/user-overlays/10204-rm-unsafe-type-of-coercion.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10204" ] || [ "$CI_BRANCH" = "rm-unsafe-type-of-coercion" ]; then
+
+ paramcoq_CI_REF=fix-papp
+ paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq
+
+fi
diff --git a/dev/ci/user-overlays/11235-non-maximal-implicit.sh b/dev/ci/user-overlays/11235-non-maximal-implicit.sh
new file mode 100644
index 0000000000..fd63980036
--- /dev/null
+++ b/dev/ci/user-overlays/11235-non-maximal-implicit.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "11235" ] || [ "$CI_BRANCH" = "non-maximal-implicit" ]; then
+
+ quickchick_CI_REF=non_maximal_implicit
+ quickchick_CI_GITURL=https://github.com/SimonBoulier/QuickChick
+
+ elpi_CI_REF=non_maximal_implicit
+ elpi_CI_GITURL=https://github.com/SimonBoulier/coq-elpi
+
+fi
diff --git a/dev/ci/user-overlays/11417-ppedrot-rm-kind-of-type.sh b/dev/ci/user-overlays/11417-ppedrot-rm-kind-of-type.sh
new file mode 100644
index 0000000000..5fb29e1826
--- /dev/null
+++ b/dev/ci/user-overlays/11417-ppedrot-rm-kind-of-type.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "11417" ] || [ "$CI_BRANCH" = "rm-kind-of-type" ]; then
+
+ elpi_CI_REF=rm-kind-of-type
+ elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi
+
+fi
diff --git a/dev/ci/user-overlays/11521-SkySkimmer-no-optname.sh b/dev/ci/user-overlays/11521-SkySkimmer-no-optname.sh
new file mode 100644
index 0000000000..f2a431978d
--- /dev/null
+++ b/dev/ci/user-overlays/11521-SkySkimmer-no-optname.sh
@@ -0,0 +1,15 @@
+if [ "$CI_PULL_REQUEST" = "11521" ] || [ "$CI_BRANCH" = "no-optname" ]; then
+
+ coqhammer_CI_REF=no-optname
+ coqhammer_CI_GITURL=https://github.com/SkySkimmer/coqhammer
+
+ equations_CI_REF=no-optname
+ equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+ unicoq_CI_REF=no-optname
+ unicoq_CI_GITURL=https://github.com/SkySkimmer/unicoq
+
+ paramcoq_CI_REF=no-optname
+ paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq
+
+fi
diff --git a/dev/ci/user-overlays/11557-SkySkimmer-template-directify.sh b/dev/ci/user-overlays/11557-SkySkimmer-template-directify.sh
new file mode 100644
index 0000000000..913b39c30c
--- /dev/null
+++ b/dev/ci/user-overlays/11557-SkySkimmer-template-directify.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "11557" ] || [ "$CI_BRANCH" = "template-directify" ]; then
+
+ equations_CI_REF=template-directify
+ equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+ paramcoq_CI_REF=template-directify
+ paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq
+
+ elpi_CI_REF=template-directify
+ elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+fi
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 05:07:44 +0000