diff options
Diffstat (limited to 'dev/ci/user-overlays')
25 files changed, 115 insertions, 111 deletions
diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh deleted file mode 100644 index 7716bcb59a..0000000000 --- a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then - mathcomp_CI_BRANCH=ssr-merge - mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git -fi diff --git a/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh b/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh deleted file mode 100644 index c2e3670380..0000000000 --- a/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6405" ] || [ "$CI_BRANCH" = "rm-local-polymorphic-flag" ]; then - Equations_CI_BRANCH=rm-local-polymorphic-flag - Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations -fi diff --git a/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh b/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh deleted file mode 100644 index 78789a6fc5..0000000000 --- a/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6483" ] || [ "$TRAVIS_BRANCH" = "check-poly-effects" ]; then - HoTT_CI_BRANCH=check-poly-effects - HoTT_CI_GITURL=https://github.com/ppedrot/HoTT.git -fi diff --git a/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh b/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh deleted file mode 100644 index 9677b35253..0000000000 --- a/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh +++ /dev/null @@ -1,8 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6493" ] || [ "$CI_BRANCH" = "API/remove-big-file" ]; then - Equations_CI_BRANCH=API-removal - Equations_CI_GITURL=https://github.com/gares/Coq-Equations.git - coq_dpdgraph_CI_BRANCH=API-removal - coq_dpdgraph_CI_GITURL=https://github.com/gares/coq-dpdgraph.git - ltac2_CI_BRANCH=API-removal - ltac2_CI_GITURL=https://github.com/gares/ltac2.git -fi diff --git a/dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh b/dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh deleted file mode 100644 index 4b681909d6..0000000000 --- a/dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh +++ /dev/null @@ -1,7 +0,0 @@ - if [ "$CI_PULL_REQUEST" = "6511" ] || [ "$CI_BRANCH" = "econstr+more_fix" ]; then - ltac2_CI_BRANCH=econstr+more_fix - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - Equations_CI_BRANCH=econstr+more_fix - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations -fi diff --git a/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh b/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh deleted file mode 100644 index 8a50fb1111..0000000000 --- a/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6535" ] || [ "$CI_BRANCH" = "fix-push-rel-to-named" ]; then - Equations_CI_BRANCH=fix-6535 - Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations -fi diff --git a/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh b/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh deleted file mode 100644 index 2451657d43..0000000000 --- a/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6676" ] || [ "$CI_BRANCH" = "proofview/goal-w-state" ]; then - ltac2_CI_BRANCH=fix-for/6676 - ltac2_CI_GITURL=https://github.com/gares/ltac2.git - Equations_CI_BRANCH=fix-for/6676 - Equations_CI_GITURL=https://github.com/gares/Coq-Equations.git -fi diff --git a/dev/ci/user-overlays/06686-ccnv-no-proj.sh b/dev/ci/user-overlays/06686-ccnv-no-proj.sh deleted file mode 100644 index 3a3ab44e03..0000000000 --- a/dev/ci/user-overlays/06686-ccnv-no-proj.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6686" ] || [ "$CI_BRANCH" = "ccnv-no-proj" ]; then - Equations_CI_BRANCH=ccnv-fixes - Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations -fi diff --git a/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh b/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh deleted file mode 100644 index d1d61fec2e..0000000000 --- a/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh +++ /dev/null @@ -1,13 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6745" ] || [ "$CI_BRANCH" = "located+vernac" ]; then - ltac2_CI_BRANCH=located+vernac - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - Equations_CI_BRANCH=located+vernac - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - fiat_parsers_CI_BRANCH=located+vernac - fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat - - Elpi_CI_BRANCH=located+vernac - Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git -fi diff --git a/dev/ci/user-overlays/06775-univ-cumul-weak.sh b/dev/ci/user-overlays/06775-univ-cumul-weak.sh deleted file mode 100644 index 8afcbf78a3..0000000000 --- a/dev/ci/user-overlays/06775-univ-cumul-weak.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6775" ] || [ "$CI_BRANCH" = "univ-cumul" ]; then - Elpi_CI_BRANCH=coq-master - Elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi.git -fi diff --git a/dev/ci/user-overlays/06831-ejgallego-located+vernac_2.sh b/dev/ci/user-overlays/06831-ejgallego-located+vernac_2.sh deleted file mode 100644 index df3e9cef28..0000000000 --- a/dev/ci/user-overlays/06831-ejgallego-located+vernac_2.sh +++ /dev/null @@ -1,14 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6831" ] || [ "$CI_BRANCH" = "located+vernac_2" ]; then - - ltac2_CI_BRANCH=located+vernac_2 - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - Equations_CI_BRANCH=located+vernac_2 - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - # fiat_parsers_CI_BRANCH=located+vernac - # fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat - - Elpi_CI_BRANCH=located+vernac_2 - Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git -fi diff --git a/dev/ci/user-overlays/06837-ejgallego-located+libnames.sh b/dev/ci/user-overlays/06837-ejgallego-located+libnames.sh deleted file mode 100644 index a785290e7c..0000000000 --- a/dev/ci/user-overlays/06837-ejgallego-located+libnames.sh +++ /dev/null @@ -1,15 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6837" ] || [ "$CI_BRANCH" = "located+libnames" ]; then - - ltac2_CI_BRANCH=located+libnames - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - Equations_CI_BRANCH=located+libnames - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - Elpi_CI_BRANCH=located+libnames - Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git - - coq_dpdgraph_CI_BRANCH=located+libnames - coq_dpdgraph_CI_GITURL=https://github.com/ejgallego/coq-dpdgraph.git - -fi diff --git a/dev/ci/user-overlays/06869-ejgallego-ssr+correct_packing.sh b/dev/ci/user-overlays/06869-ejgallego-ssr+correct_packing.sh deleted file mode 100644 index 5dedca0ca5..0000000000 --- a/dev/ci/user-overlays/06869-ejgallego-ssr+correct_packing.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6869" ] || [ "$CI_BRANCH" = "ssr+correct_packing" ]; 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=ssr+correct_packing - Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git - -fi diff --git a/dev/ci/user-overlays/06923-ppedrot-export-options.sh b/dev/ci/user-overlays/06923-ppedrot-export-options.sh deleted file mode 100644 index 333a9e84bd..0000000000 --- a/dev/ci/user-overlays/06923-ppedrot-export-options.sh +++ /dev/null @@ -1,7 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6923" ] || [ "$CI_BRANCH" = "export-options" ]; then - ltac2_CI_BRANCH=export-options - ltac2_CI_GITURL=https://github.com/ppedrot/ltac2 - - Equations_CI_BRANCH=export-options - Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations -fi diff --git a/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh b/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh new file mode 100644 index 0000000000..b05d02c5be --- /dev/null +++ b/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh @@ -0,0 +1,14 @@ +_OVERLAY_BRANCH=clean-transp-state + +if [ "$CI_PULL_REQUEST" = "7925" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then + + unicoq_CI_REF="$_OVERLAY_BRANCH" + unicoq_CI_GITURL=https://github.com/ppedrot/unicoq + + equations_CI_REF="$_OVERLAY_BRANCH" + equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + + mtac2_CI_REF="$_OVERLAY_BRANCH" + mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 + +fi diff --git a/dev/ci/user-overlays/08850-poly-local-univs.sh b/dev/ci/user-overlays/08850-poly-local-univs.sh new file mode 100644 index 0000000000..482792d7cd --- /dev/null +++ b/dev/ci/user-overlays/08850-poly-local-univs.sh @@ -0,0 +1,9 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "8850" ] || [ "$CI_BRANCH" = "poly-local-univs" ]; then + formal_topology_CI_REF=poly-local-univs + formal_topology_CI_GITURL=https://github.com/SkySkimmer/topology + + paramcoq_CI_REF=poly-local-univs + paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq +fi diff --git a/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh b/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh new file mode 100644 index 0000000000..17eb5fffae --- /dev/null +++ b/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "8889" ] || [ "$CI_BRANCH" = "program-hook-obligation-subst" ]; then + + Equations_CI_REF=program-hook-obligation-subst + Equations_CI_GITURL=https://github.com/mattam82/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh b/dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh new file mode 100644 index 0000000000..08112d3054 --- /dev/null +++ b/dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh @@ -0,0 +1,15 @@ +if [ "$CI_PULL_REQUEST" = "8902" ] || [ "$CI_BRANCH" = "ltac+use_atts_in_ast" ]; then + + aactactics_CI_REF=ltac+use_atts_in_ast + aactactics_CI_GITURL=https://github.com/ejgallego/aac-tactics + + coqhammer_CI_REF=ltac+use_atts_in_ast + coqhammer_CI_GITURL=https://github.com/ejgallego/coqhammer + + Equations_CI_REF=ltac+use_atts_in_ast + Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + mtac2_CI_REF=ltac+use_atts_in_ast + mtac2_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh b/dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh new file mode 100644 index 0000000000..1c5157ba12 --- /dev/null +++ b/dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "8914" ] || [ "$CI_BRANCH" = "lib+better_boot_coqproject" ]; then + + quickchick_CI_REF=lib+better_boot_coqproject + quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick + +fi diff --git a/dev/ci/user-overlays/08933-solve-remaining-evars-initial-arg.sh b/dev/ci/user-overlays/08933-solve-remaining-evars-initial-arg.sh new file mode 100644 index 0000000000..e74e53fa40 --- /dev/null +++ b/dev/ci/user-overlays/08933-solve-remaining-evars-initial-arg.sh @@ -0,0 +1,6 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "8933" ] || [ "$CI_BRANCH" = "solve-remaining-evars-initial-arg" ]; then + plugin_tutorial_CI_REF=solve-remaining-evars-initial-arg + plugin_tutorial_CI_GITURL=https://github.com/SkySkimmer/plugin_tutorials +fi diff --git a/dev/ci/user-overlays/08985-ejgallego-build+pack_gramlib.sh b/dev/ci/user-overlays/08985-ejgallego-build+pack_gramlib.sh new file mode 100644 index 0000000000..d7130cc67a --- /dev/null +++ b/dev/ci/user-overlays/08985-ejgallego-build+pack_gramlib.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "8985" ] || [ "$CI_BRANCH" = "build+pack_gramlib" ]; then + + elpi_CI_REF=use_coq_gramlib + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + +fi diff --git a/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh b/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh new file mode 100644 index 0000000000..c8bea0c868 --- /dev/null +++ b/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "8998" ] || [ "$CI_BRANCH" = "legacy_proof_eng_clean" ]; then + + equations_CI_REF=legacy_proof_eng_clean + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh b/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh new file mode 100644 index 0000000000..61ffa4a197 --- /dev/null +++ b/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "9003" ] || [ "$CI_BRANCH" = "vernac+move_extend_ast" ]; then + + ltac2_CI_REF=vernac+move_extend_ast + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + +fi diff --git a/dev/ci/user-overlays/09051-ppedrot-camlp5-safe-api-strikes-back.sh b/dev/ci/user-overlays/09051-ppedrot-camlp5-safe-api-strikes-back.sh new file mode 100644 index 0000000000..14e7c0d7f0 --- /dev/null +++ b/dev/ci/user-overlays/09051-ppedrot-camlp5-safe-api-strikes-back.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "9051" ] || [ "$CI_BRANCH" = "camlp5-safe-api-strikes-back" ]; then + + equations_CI_REF=camlp5-safe-api-strikes-back + equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + + ltac2_CI_REF=camlp5-safe-api-strikes-back + ltac2_CI_GITURL=https://github.com/ppedrot/ltac2 + +fi diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index 9f0377ceea..7fb73e447d 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -1,16 +1,43 @@ # 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`](../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_BRANCH=ssr-merge - mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git + 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`](/dev/ci/ci-common.sh)) +(`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`. |