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. 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).

This file must contain one or more invocation of the overlay function:

overlay <project> <giturl> <ref> <prnumber> [<prbranch>]

Each call creates an overlay for project using a given giturl and ref which is active for prnumber or prbranch (prbranch defaults to ref).

Example of an overlay for the project elpi that uses the branch noinstance from the fork of SkySkimmer and is active for pull request 13128

overlay elpi https://github.com/SkySkimmer/coq-elpi noinstance 13128

Such a file can be created automatically using the scripts create_overlays.sh. See also the list of projects for which one can write an overlay in the file ci-basic-overlay.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.