diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/README-developers.md | 7 | ||||
| -rw-r--r-- | dev/ci/README-users.md | 42 |
2 files changed, 27 insertions, 22 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md index 9ed7180807..6a740b9033 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -43,9 +43,10 @@ See also [`test-suite/README.md`](../../test-suite/README.md) for information ab ### Breaking changes When your PR breaks an external project we test in our CI, you must -prepare a patch (or ask someone to prepare a patch) to fix the -project. There is experimental support for an improved workflow, see -[the next section](#experimental-automatic-overlay-creation-and-building), below +prepare a patch (or ask someone—possibly the project author—to +prepare a patch) to fix the project. There is experimental support for +an improved workflow, see [the next +section](#experimental-automatic-overlay-creation-and-building), below are the steps to manually prepare a patch: 1. Fork the external project, create a new branch, push a commit adapting diff --git a/dev/ci/README-users.md b/dev/ci/README-users.md index 06b617d4c1..6649820f22 100644 --- a/dev/ci/README-users.md +++ b/dev/ci/README-users.md @@ -1,36 +1,40 @@ Information for external library / Coq plugin authors ----------------------------------------------------- -You are encouraged to consider submitting your development for addition to +You are encouraged to consider submitting your project for addition to Coq's CI. This means that: -- Any time that a proposed change is breaking your development, Coq developers - will send you patches to adapt it or, at the very least, will work with you - to see how to adapt it. +- Any time that a proposed change is breaking your project, Coq + developers and contributors will send you patches to adapt it or + will explain how to adapt it and work with you to ensure that you + manage to do it. On the condition that: -- At the time of the submission, your development works with Coq's +- At the time of the submission, your project works with Coq's `master` branch. -- Your development is publicly available in a git repository and we can easily +- Your project is publicly available in a git repository and we can easily send patches to you (e.g. through pull / merge requests). - You react in a timely manner to discuss / integrate those patches. + When seeking your help for preparing such patches, we will accept + that it takes longer than when we are just requesting to integrate a + simple (and already fully prepared) patch. - You do not push, to the branches that we test, commits that haven't been first tested to compile with the corresponding branch(es) of Coq. - For that, we recommend setting a CI system for you development, see + For that, we recommend setting a CI system for you project, see [supported CI images for Coq](#supported-ci-images-for-coq) below. -- You maintain a reasonable build time for your development, or you provide +- You maintain a reasonable build time for your project, or you provide a "lite" target that we can use. In case you forget to comply with these last three conditions, we would reach -out to you and give you a 30-day grace period during which your development +out to you and give you a 30-day grace period during which your project would be moved into our "allow failure" category. At the end of the grace -period, in the absence of progress, the development would be removed from our +period, in the absence of progress, the project would be removed from our CI. ### Timely merging of overlays @@ -47,7 +51,7 @@ these kind of merges. ### OCaml and plugin-specific considerations -Developments that link against Coq's OCaml API [most of them are known +Projects that link against Coq's OCaml API [most of them are known as "plugins"] do have some special requirements: - Coq's OCaml API is not stable. We hope to improve this in the future @@ -65,7 +69,7 @@ as "plugins"] do have some special requirements: uses. In particular, warnings that are considered fatal by the Coq developers _must_ be also fatal for plugin CI code. -### Add your development by submitting a pull request +### Add your project by submitting a pull request Add a new `ci-mydev.sh` script to [`dev/ci`](.); set the corresponding variables in [`ci-basic-overlay.sh`](ci-basic-overlay.sh); add the @@ -75,7 +79,7 @@ Have a look at [#7656](https://github.com/coq/coq/pull/7656/files) for an example. **Do not hesitate to submit an incomplete pull request if you need help to finish it.** -You may also be interested in having your development tested in our +You may also be interested in having your project tested in our 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. @@ -83,13 +87,13 @@ 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. +your project for particular Coq versions. This is in fact very likely +if your project 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. +For such projects, we 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. |