diff options
Diffstat (limited to 'dev/ci/user-overlays')
8 files changed, 92 insertions, 2 deletions
diff --git a/dev/ci/user-overlays/06454-ejgallego-evar+strict_to_constr.sh b/dev/ci/user-overlays/06454-ejgallego-evar+strict_to_constr.sh new file mode 100644 index 0000000000..f4cb71cf19 --- /dev/null +++ b/dev/ci/user-overlays/06454-ejgallego-evar+strict_to_constr.sh @@ -0,0 +1,8 @@ +if [ "$CI_PULL_REQUEST" = "6454" ] || [ "$CI_BRANCH" = "evar+strict_to_constr" ]; then + + # ltac2_CI_BRANCH=econstr+more_fix + # ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + Equations_CI_BRANCH=evar+strict_to_constr + Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations +fi diff --git a/dev/ci/user-overlays/06859-ejgallego-stm+top.sh b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh new file mode 100644 index 0000000000..b22ab36302 --- /dev/null +++ b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh @@ -0,0 +1,9 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "6859" ] || [ "$CI_BRANCH" = "stm+top" ] || \ + [ "$CI_PULL_REQUEST" = "7543" ] || [ "$CI_BRANCH" = "ide+split" ] ; then + + pidetop_CI_BRANCH=stm+top + pidetop_CI_GITURL=https://bitbucket.org/ejgallego/pidetop.git + +fi diff --git a/dev/ci/user-overlays/07136-evar-map-econstr.sh b/dev/ci/user-overlays/07136-evar-map-econstr.sh new file mode 100644 index 0000000000..06aa62726d --- /dev/null +++ b/dev/ci/user-overlays/07136-evar-map-econstr.sh @@ -0,0 +1,7 @@ +if [ "$CI_PULL_REQUEST" = "7136" ] || [ "$CI_BRANCH" = "evar-map-econstr" ]; then + Equations_CI_BRANCH=8.9+alpha + Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git + + Elpi_CI_BRANCH=coq-7136 + Elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi.git +fi diff --git a/dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh b/dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh new file mode 100644 index 0000000000..7e554684e8 --- /dev/null +++ b/dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh @@ -0,0 +1,12 @@ +if [ "$CI_PULL_REQUEST" = "7152" ] || [ "$CI_BRANCH" = "api+vernac_expr_iso" ]; then + + # Equations_CI_BRANCH=ssr+correct_packing + # Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + # ltac2_CI_BRANCH=ssr+correct_packing + # ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + Elpi_CI_BRANCH=api+vernac_expr_iso + Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git + +fi diff --git a/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh b/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh new file mode 100644 index 0000000000..ea9cd8ee07 --- /dev/null +++ b/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh @@ -0,0 +1,21 @@ +if [ "$CI_PULL_REQUEST" = "7196" ] || [ "$CI_BRANCH" = "tactics+push_fix_naming_out" ] || [ "$CI_BRANCH" = "pr-7196" ]; then + + # Needed overlays: https://gitlab.com/coq/coq/pipelines/21244550 + # + # equations + # ltac2 + + # The below developments should instead use a backwards compatible fix. + # + # color + # iris-lambda-rust + # math-classes + # formal-topology + + ltac2_CI_BRANCH=tactics+push_fix_naming_out + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + Equations_CI_BRANCH=tactics+push_fix_naming_out + Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh new file mode 100644 index 0000000000..517088a247 --- /dev/null +++ b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "7213" ] || [ "$CI_BRANCH" = "fast-constr-match-no-context" ]; then + + ltac2_CI_BRANCH=fast-constr-match-no-context + ltac2_CI_GITURL=https://github.com/ppedrot/ltac2 + +fi diff --git a/dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh b/dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh new file mode 100644 index 0000000000..115f29f1ee --- /dev/null +++ b/dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh @@ -0,0 +1,14 @@ +if [ "$CI_PULL_REQUEST" = "7558" ] || [ "$CI_BRANCH" = "vernac+move_parser" ]; then + + _OVERLAY_BRANCH=vernac+move_parser + + Equations_CI_BRANCH="$_OVERLAY_BRANCH" + Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + ltac2_CI_BRANCH="$_OVERLAY_BRANCH" + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + mtac2_CI_BRANCH="$_OVERLAY_BRANCH" + mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 + +fi diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index a7474e3248..aec2dfe0a6 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -1,8 +1,21 @@ # Add overlays for your pull requests in this directory -An overlay is a file containing very simple logic to test whether we are currently building a specific pull request or git branch (useful so that overlays work on your own fork) and which changes some of the variables whose default can be found in [`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh). +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. -The name of your overlay file should be of the form `five_digit_PR_number-GitHub_handle-branch_name.sh`. +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`](/dev/ci/ci-basic-overlay.sh): +give the name of your branch using a `_CI_BRANCH` variable and the location of +your fork using a `_CI_GITURL` variable. + +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 |