diff options
Diffstat (limited to 'dev/doc/release-process.md')
| -rw-r--r-- | dev/doc/release-process.md | 30 |
1 files changed, 29 insertions, 1 deletions
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index 1821a181f1..b33a1cbd73 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -6,6 +6,35 @@ the present checklist. - [ ] Change the version name to the next major version and the magic numbers (see [#7008](https://github.com/coq/coq/pull/7008/files)). +- [ ] Update the compatibility infrastructure, which consists of doing + the following steps. Note that all but the final step can be + performed automatically by + [`dev/tools/update-compat.py`](/dev/tools/update-compat.py) so + long as you have already updated `coq_version` in + [`configure.ml`](/configure.ml). + + [ ] Add a file `theories/Compat/CoqXX.v` which contains just the header + from [`dev/header.ml`](/dev/header.ml) + + [ ] Add the line `Require Export Coq.Compat.CoqXX.` at the top of + `theories/Compat/CoqYY.v`, where Y.Y is the version prior to X.X. + + [ ] Delete the file `theories/Compat/CoqWW.v`, where W.W is three versions + prior to X.X. + + [ ] Update + [`doc/stdlib/index-list.html.template`](/doc/stdlib/index-list.html.template) + with the deleted/added files. + + [ ] Remove any notations in the standard library which have `compat "W.W"`. + + [ ] Update the type `compat_version` in [`lib/flags.ml`](/lib/flags.ml) by + bumping all the version numbers by one, and update the interpretations + of those flags in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml) and + [`vernac/g_vernac.mlg`](/vernac/g_vernac.mlg). + + [ ] Update the files + [`test-suite/success/CompatCurrentFlag.v`](/test-suite/success/CompatCurrentFlag.v), + [`test-suite/success/CompatPreviousFlag.v`](/test-suite/success/CompatPreviousFlag.v), + and + [`test-suite/success/CompatOldFlag.v`](/test-suite/success/CompatOldFlag.v) + by bumping all version numbers by 1. + + [ ] Decide what to do about all test-suite files which mention `-compat + W.W` or `Coq.Comapt.CoqWW` (which is no longer valid, since we only + keep compatibility against the two previous versions) - [ ] Put the corresponding alpha tag using `git tag -s`. The `VX.X+alpha` tag marks the first commit to be in `master` and not in the branch of the previous version. @@ -57,7 +86,6 @@ ## Before the beta release date ## - [ ] Ensure the Credits chapter has been updated. -- [ ] Ensure an empty `CompatXX.v` file has been created. - [ ] Ensure that an appropriate version of the plugins we will distribute with Coq has been tagged. - [ ] Have some people test the recently auto-generated Windows and MacOS |