diff options
| author | Emilio Jesus Gallego Arias | 2018-11-18 17:36:19 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-24 13:16:00 +0100 |
| commit | 991790c8135cf3073907fda3baadc9718419f173 (patch) | |
| tree | cc52eb7fd5910262a977c59a4fe67df405103371 | |
| parent | fe9dd5d75c54861a9a6b566c139225db356e9055 (diff) | |
[ci] [doc] Note about `create-overlays.sh`
| -rw-r--r-- | dev/ci/README-developers.md | 28 |
1 files changed, 26 insertions, 2 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md index f1b32ad318..8cb1a0edef 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -42,8 +42,11 @@ 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: +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 +are the steps to manually prepare a patch: 1. Fork the external project, create a new branch, push a commit adapting the project to your changes. @@ -65,6 +68,27 @@ patch (or ask someone to prepare a patch) to fix the project: Moreover your PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) file. +### Experimental automatic overlay creation and building + +If you break external projects that are hosted on GitHub, you can use +the `create-overlays.sh` script to automatically perform most of the +above step. In order to do so, call the script as: +``` +./dev/tools/create-overlays.sh ejgallego 9873 aac_tactics elpi ltac +``` +replacing `ejgallego` by your github id and `9873` by the actual PR +number. The script will: + +- checkout the contributions and prepare the branch/remote so you can + just commit the fixes and push, +- add the corresponding overlay file in `dev/ci/user-overlays` + +For problems related to ML-plugins, if you use `dune build` to build +Coq, it will actually be aware of the broken contributions and perform +a global build. This is very convenient when using `merlin` as you +will get a coherent view of all the broken plugins, which full +incremental cross-project rebuild. + Advanced GitLab CI information ------------------------------ |