diff options
| author | Emilio Jesus Gallego Arias | 2018-10-17 14:26:32 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-17 14:41:38 +0200 |
| commit | b33794516f4dd10edcb06be49c0202a9e056c26e (patch) | |
| tree | 0fbf2eff7a667ff5c7f48d3a1c122041a8d26d94 /dev | |
| parent | f111af975860b5f48bb792d718e4eb211f6fa57f (diff) | |
[ci] [doc] Notes about branch names.
I'd like to add this convention as it is very convenient for the
development of dev tools. Example, I can do `setup-coq-devs ltac
equations` and then get a fully composed tree. Similarly for preparing
overlays.
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`. |