diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/README.md | 16 | ||||
| -rw-r--r-- | dev/ci/user-overlays/README.md | 8 |
2 files changed, 23 insertions, 1 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md index 7853866f62..4709247549 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -26,7 +26,8 @@ our CI. This means that: On the condition that: -- At the time of the submission, your development works with Coq master branch. +- At the time of the submission, your development works with Coq's + `master` branch. - Your development is publicly available in a git repository and we can easily send patches to you (e.g. through pull / merge requests). @@ -60,6 +61,19 @@ performance benchmark. Currently this is done by providing an OPAM package in https://github.com/coq/opam-coq-archive and opening an issue at https://github.com/coq/coq-bench/issues. +### Recommended branching policy. + +It is sometimes the case that you will need to maintain a branch of +your development for particular Coq versions. This is in fact very +likely if your development includes a Coq ML plugin. + +We thus recommend a branching convention that mirrors Coq's branching +policy. Then, you would have a `master` branch that follows Coq's +`master`, a `v8.8` branch that works with Coq's `v8.8` branch and so +on. + +This convention will be supported by tools in the future to make some +developer commands work more seamlessly. Information for developers -------------------------- diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index 68afe7ee4a..7fb73e447d 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -33,3 +33,11 @@ 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`. |