How to add overlays for PRs - math-comp/math-comp GitHub Wiki

⚠️ this page is outdated, it is about the Docker based CI which is mostly unused nowadays and replaced by the Nix based CI, to add an overlay in th Nix CI, it is often enough to add a line in .nix/config.nix like mathcomp-real-closed.override.version = "<github_login>:<branch>";

In case a PR breaks a "child project" tested in math-comp's CI, it is possible to slightly edit the .gitlab-ci.yml file within the PR to act as an overlay (borrowing the terminology used in the coq repository).

The different steps are summarized below on a hypothetical example:

1. assuming a math-comp PR #1234 breaks the ci-fourcolor-dev job defined as:

   ci-fourcolor-dev:
     extends: .ci-fourcolor
     variables:
       COQ_VERSION: "dev"

2. assuming a non-backward-compatible, downstream patch has been pushed to a separated branch fix-foo in a fork https://github.com/user/fourcolor.git
3. then one would only need to add one commit in the PR #1234, replacing the above four lines with:

   ci-fourcolor-dev:
     extends: .ci-fourcolor
     variables:
       COQ_VERSION: "dev"
     # lines below have been added
     except:
       - tags
       - merge_requests
       - schedules
       - /^pr-1234$/
       - /^github-branch$/
   
   ci-fourcolor-dev-1234:
     extends: .ci-fourcolor
     variables:
       COQ_VERSION: "dev"
       CONTRIB_URL: "https://github.com/user/fourcolor.git"
       CONTRIB_VERSION: "fix-foo"
     only:
       - /^pr-1234$/
       - /^github-branch$/

   where github-branch denotes the name of the GitHub source branch of the PR, assuming it is part of the upstream math-comp repo. If the PR is opened from a math-comp fork, the two - /^github-branch$/ lines should be skipped.
4. so the upcoming CI builds in pr-1234 (as well as in the github-branch, if specified) will use the relevant fourcolor branch, while after the merge in master, the regular branch of fourcolor will be used for all subsequent builds in master.
5. after math-comp master has been built and pushed to https://hub.docker.com/r/mathcomp/mathcomp-dev, the downstream PR containing the non-backward-compatible patch can be merged.
6. finally (for cleaning purposes), the commit that had changed the .gitlab-ci.yml file to configure the overlay can be reverted in master using git revert $COMMIT_HASH, as it is now a "no-op".

Note: as noticed in PR #451, we need to repeat the lines below from the .ci job in .gitlab-ci.yml in the overlay job that adds other except rules, otherwise the scheduled pipeline that deploys math-comp master to mathcomp/mathcomp-dev:coq-dev on Docker Hub every night would fail:

except:
  - tags
  - merge_requests
  - schedules