diff options
Diffstat (limited to 'dev/ci/user-overlays')
5 files changed, 70 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh b/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh new file mode 100644 index 0000000000..2df8affd14 --- /dev/null +++ b/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "9102" ] || [ "$CI_BRANCH" = "ltac+remove_aliases" ]; then + + elpi_CI_REF=ltac+remove_aliases + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + +fi diff --git a/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh b/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh new file mode 100644 index 0000000000..f2a113b118 --- /dev/null +++ b/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "9150" ] || [ "$CI_BRANCH" = "build+warn_50" ]; then + + mtac2_CI_REF=build+warn_50 + mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 + +fi diff --git a/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh b/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh new file mode 100644 index 0000000000..f532fdfc52 --- /dev/null +++ b/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "9172" ] || [ "$CI_BRANCH" = "proof_rework" ]; then + + ltac2_CI_REF=proof_rework + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + mtac2_CI_REF=proof_rework + mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 + +fi diff --git a/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh b/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh new file mode 100644 index 0000000000..efcdd2e97f --- /dev/null +++ b/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "9220" ] || [ "$CI_BRANCH" = "stm-shallow-logic" ]; then + + paramcoq_CI_REF=stm-shallow-logic + paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq + +fi diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md new file mode 100644 index 0000000000..7fb73e447d --- /dev/null +++ b/dev/ci/user-overlays/README.md @@ -0,0 +1,43 @@ +# Add overlays for your pull requests in this directory + +When your pull request breaks an external project we test in our CI and you +have prepared a branch with the fix, you can add an "overlay" to your pull +request to test it with the adapted version of the external project. + +An overlay is a file which defines where to look for the patched version so that +testing is possible. It redefines some variables from +[`ci-basic-overlay.sh`](../ci-basic-overlay.sh): +give the name of your branch / commit using a `_CI_REF` variable and the +location of your fork using a `_CI_GITURL` variable. +The `_CI_GITURL` variable should be the URL of the repository without a +trailing `.git`. +If the fork is not on the same platform (e.g. GitHub instead of GitLab), it is +necessary to redefine the `_CI_ARCHIVEURL` variable as well. + +Moreover, the file contains very simple logic to test the pull request number +or branch name and apply it only in this case. + +The name of your overlay file should start with a five-digit pull request +number, followed by a dash, anything (for instance your GitHub nickname +and the branch name), then a `.sh` extension (`[0-9]{5}-[a-zA-Z0-9-_]+.sh`). + +Example: `00669-maximedenes-ssr-merge.sh` containing + +``` +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then + mathcomp_CI_REF=ssr-merge + mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp +fi +``` + +(`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](../ci-common.sh)) + +### Branching conventions + +We suggest you use the convention of identical branch names for the +Coq branch and the CI project branch used in the overlay. For example, +if your Coq PR is coming from the branch `more_efficient_tc`, and that +breaks `ltac2`, we suggest you create a `ltac2` overlay with a branch +named `more_efficient_tc`. |