aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci')
-rw-r--r--dev/ci/README-developers.md7
-rw-r--r--dev/ci/README-users.md42
-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/10832-herbelin-master+fix6082-7766-overriding-notation-format.sh9
-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
16 files changed, 115 insertions, 61 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index 9ed7180807..6a740b9033 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -43,9 +43,10 @@ See also [`test-suite/README.md`](../../test-suite/README.md) for information ab
### Breaking changes
When your PR breaks an external project we test in our CI, you must
-prepare a patch (or ask someone to prepare a patch) to fix the
-project. There is experimental support for an improved workflow, see
-[the next section](#experimental-automatic-overlay-creation-and-building), below
+prepare a patch (or ask someone—possibly the project author—to
+prepare a patch) to fix the project. There is experimental support for
+an improved workflow, see [the next
+section](#experimental-automatic-overlay-creation-and-building), below
are the steps to manually prepare a patch:
1. Fork the external project, create a new branch, push a commit adapting
diff --git a/dev/ci/README-users.md b/dev/ci/README-users.md
index 06b617d4c1..6649820f22 100644
--- a/dev/ci/README-users.md
+++ b/dev/ci/README-users.md
@@ -1,36 +1,40 @@
Information for external library / Coq plugin authors
-----------------------------------------------------
-You are encouraged to consider submitting your development for addition to
+You are encouraged to consider submitting your project for addition to
Coq's CI. This means that:
-- Any time that a proposed change is breaking your development, Coq developers
- will send you patches to adapt it or, at the very least, will work with you
- to see how to adapt it.
+- Any time that a proposed change is breaking your project, Coq
+ developers and contributors will send you patches to adapt it or
+ will explain how to adapt it and work with you to ensure that you
+ manage to do it.
On the condition that:
-- At the time of the submission, your development works with Coq's
+- At the time of the submission, your project works with Coq's
`master` branch.
-- Your development is publicly available in a git repository and we can easily
+- Your project is publicly available in a git repository and we can easily
send patches to you (e.g. through pull / merge requests).
- You react in a timely manner to discuss / integrate those patches.
+ When seeking your help for preparing such patches, we will accept
+ that it takes longer than when we are just requesting to integrate a
+ simple (and already fully prepared) patch.
- You do not push, to the branches that we test, commits that haven't been
first tested to compile with the corresponding branch(es) of Coq.
- For that, we recommend setting a CI system for you development, see
+ For that, we recommend setting a CI system for you project, see
[supported CI images for Coq](#supported-ci-images-for-coq) below.
-- You maintain a reasonable build time for your development, or you provide
+- You maintain a reasonable build time for your project, or you provide
a "lite" target that we can use.
In case you forget to comply with these last three conditions, we would reach
-out to you and give you a 30-day grace period during which your development
+out to you and give you a 30-day grace period during which your project
would be moved into our "allow failure" category. At the end of the grace
-period, in the absence of progress, the development would be removed from our
+period, in the absence of progress, the project would be removed from our
CI.
### Timely merging of overlays
@@ -47,7 +51,7 @@ these kind of merges.
### OCaml and plugin-specific considerations
-Developments that link against Coq's OCaml API [most of them are known
+Projects that link against Coq's OCaml API [most of them are known
as "plugins"] do have some special requirements:
- Coq's OCaml API is not stable. We hope to improve this in the future
@@ -65,7 +69,7 @@ as "plugins"] do have some special requirements:
uses. In particular, warnings that are considered fatal by the Coq
developers _must_ be also fatal for plugin CI code.
-### Add your development by submitting a pull request
+### Add your project by submitting a pull request
Add a new `ci-mydev.sh` script to [`dev/ci`](.); set the corresponding
variables in [`ci-basic-overlay.sh`](ci-basic-overlay.sh); add the
@@ -75,7 +79,7 @@ Have a look at [#7656](https://github.com/coq/coq/pull/7656/files) for an
example. **Do not hesitate to submit an incomplete pull request if you need
help to finish it.**
-You may also be interested in having your development tested in our
+You may also be interested in having your project tested in our
performance benchmark. Currently this is done by providing an OPAM package
in https://github.com/coq/opam-coq-archive and opening an issue at
https://github.com/coq/coq-bench/issues.
@@ -83,13 +87,13 @@ https://github.com/coq/coq-bench/issues.
### Recommended branching policy.
It is sometimes the case that you will need to maintain a branch of
-your development for particular Coq versions. This is in fact very
-likely if your development includes a Coq ML plugin.
+your project for particular Coq versions. This is in fact very likely
+if your project includes a Coq ML plugin.
-We thus recommend a branching convention that mirrors Coq's branching
-policy. Then, you would have a `master` branch that follows Coq's
-`master`, a `v8.8` branch that works with Coq's `v8.8` branch and so
-on.
+For such projects, we recommend a branching convention that mirrors
+Coq's branching policy. Then, you would have a `master` branch that
+follows Coq's `master`, a `v8.8` branch that works with Coq's `v8.8`
+branch and so on.
This convention will be supported by tools in the future to make some
developer commands work more seamlessly.
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/10832-herbelin-master+fix6082-7766-overriding-notation-format.sh b/dev/ci/user-overlays/10832-herbelin-master+fix6082-7766-overriding-notation-format.sh
new file mode 100644
index 0000000000..c17fe4fcba
--- /dev/null
+++ b/dev/ci/user-overlays/10832-herbelin-master+fix6082-7766-overriding-notation-format.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "10832" ] || [ "$CI_BRANCH" = "master+fix6082-7766-overriding-notation-format" ]; then
+
+ equations_CI_REF=master+fix-interpretation-notation-format-pr10832
+ equations_CI_GITURL=https://github.com/herbelin/Coq-Equations
+
+ quickchick_CI_REF=master+fix-interpretation-notation-format-pr10832
+ quickchick_CI_GITURL=https://github.com/herbelin/QuickChick
+
+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-05-01 17:29:45 +0000