diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/MERGING.md | 66 | ||||
| -rw-r--r-- | dev/doc/changes.md | 72 | ||||
| -rw-r--r-- | dev/doc/coq-src-description.txt | 6 | ||||
| -rw-r--r-- | dev/doc/debugging.md | 2 | ||||
| -rw-r--r-- | dev/doc/release-process.md | 100 |
5 files changed, 230 insertions, 16 deletions
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index 71fc396088..65457b63af 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -1,7 +1,8 @@ # Merging changes in Coq -This document describes how patches (submitted as Pull Requests) should be -merged into the main repository (https://github.com/coq/coq). +This document describes how patches, submitted as pull requests (PRs) on the +`master` branch, should be merged into the main repository +(https://github.com/coq/coq). ## Code owners @@ -9,8 +10,8 @@ The [CODEOWNERS](/.github/CODEOWNERS) file describes, for each part of the system, two owners. One is the principal maintainer of the component, the other is the secondary maintainer. -When a pull request is submitted, GitHub will automatically ask the principal -maintainer for a review. If the pull request touches several parts, all the +When a PR is submitted, GitHub will automatically ask the principal +maintainer for a review. If the PR touches several parts, all the corresponding principal maintainers will be asked for a review. Maintainers are never assigned as reviewer on their own PRs. @@ -42,10 +43,31 @@ A maintainer is expected to be reasonably reactive, but no specific timeframe is given for reviewing. (*) In case a component is touched in a trivial way (adding/removing one file in -a `Makefile`, etc), or by applying a systematic process (global renaming, -deprecationg propagation, etc) that has been reviewed globally, the assignee can +a `Makefile`, etc), or by applying a systematic refactoring process (global +renaming for instance) that has been reviewed globally, the assignee can say in a comment they think a review is not required and proceed with the merge. +### Breaking changes + +If the PR breaks compatibility of some external projects in CI, then fixes to +those external projects should have been prepared (cf. the relevant sub-section +in the [CI README](/dev/ci/README.md#Breaking-changes) and the PR can be tested +with these fixes thanks to ["overlays"](/dev/ci/user-overlays/README.md). + +Moreover the PR must absolutely update the [`CHANGES`](/CHANGES) file. + +If overlays are missing, ask the author to prepare them and label the PR with +the [needs: overlay](https://github.com/coq/coq/labels/needs%3A%20overlay) label. + +When fixes are ready, there are two cases to consider: + +- For patches that are backward compatible (best scenario), you should get the + external project maintainers to integrate them before merging the PR. +- For patches that are not backward compatible (which is often the case when + patching plugins after an update to the Coq API), you can proceed to merge + the PR and then notify the external project maintainers they can merge the + patch. + ## Merging Once all reviewers approved the PR, the assignee is expected to check that CI @@ -65,14 +87,40 @@ In some rare cases (e.g. the conflicts are in the CHANGES file), it is ok to fix the conflicts in the merge commit (following the same steps as below), and push to `master` directly. Don't use the GitHub interface to fix these conflicts. -The command to be used is: +To merge the PR proceed in the following way ``` -$ dev/tools/merge-pr XXXX +$ git checkout master +$ git pull +$ dev/tools/merge-pr.sh XXXX +$ git push upstream ``` -where `XXXX` is the number of the PR to be merged. This operation should be followed by a push. +where `XXXX` is the number of the PR to be merged and `upstream` is the name +of your remote pointing to `git@github.com:coq/coq.git`. +Note that you are only supposed to merge PRs into `master`. PRs should rarely +target the stable branch, but when it is the case they are the responsibility +of the release manager. + +This script conducts various checks before proceeding to merge. Don't bypass them +without a good reason to, and in that case, write a comment in the PR thread to +explain the reason. Maintainers MUST NOT merge their own patches. DON'T USE the GitHub interface for merging, since it will prevent the automated backport script from operating properly, generates bad commit messages, and a messy history when there are conflicts. + +### Merge script dependencies + +The merge script passes option `-S` to `git merge` to ensure merge commits +are signed. Consequently, it depends on the GnuPG command utility being +installed and a GPG key being available. Here is a short documentation on +how to use GPG, git & GitHub: https://help.github.com/articles/signing-commits-with-gpg/. + +The script depends on a few other utilities. If you are a Nix user, the +simplest way of getting them is to run `nix-shell` first. + +**Note for homebrew (MacOS) users:** it has been reported that installing GnuPG +is not out of the box. Installing explicitly "pinentry-mac" seems important for +typing of passphrase to work correctly (see also this +[Stack Overflow Q-and-A](https://stackoverflow.com/questions/39494631/gpg-failed-to-sign-the-data-fatal-failed-to-write-commit-object-git-2-10-0)). diff --git a/dev/doc/changes.md b/dev/doc/changes.md index ab78b0956f..4838dd734a 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,3 +1,70 @@ +## Changes between Coq 8.8 and Coq 8.9 + +### ML API + +Misctypes + +- Syntax for universe sorts and kinds has been moved from `Misctypes` + to `Glob_term`, as these are turned into kernel terms by + `Pretyping`. + +Proof engine + +- More functions have been changed to use `EConstr`, notably the + functions in `Evd`, and in particular `Evd.define`. + + Note that the core function `EConstr.to_constr` now _enforces_ by + default that the resulting term is ground, that is to say, free of + Evars. This is usually what you want, as open terms should be of + type `EConstr.t` to benefit from the invariants the `EConstr` API is + meant to guarantee. + + In case you'd like to violate this API invariant, you can use the + `abort_on_undefined_evars` flag to `EConstr.to_constr`, but note + that setting this flag to false is deprecated so it is only meant to + be used as to help port pre-EConstr code. + +- A few type alias have been deprecated, in all cases the message + should indicate what the canonical form is. An important change is + the move of `Globnames.global_reference` to `Names.GlobRef.t`. + +ML Libraries used by Coq + +- Introduction of a "Smart" module for collecting "smart*" functions, e.g. + Array.Smart.map. +- Uniformization of some names, e.g. Array.Smart.fold_left_map instead + of Array.smartfoldmap. + +Printer.ml API + +- The mechanism in Printer that allowed dynamically overriding pr_subgoals, + pr_subgoal and pr_goal was removed to simplify the code. It was + earlierly used by PCoq. + +Source code organization + +- We have eliminated / fused some redundant modules and relocated a + few interfaces files. The `intf` folder is gone, and now for example + `Constrexpr` is located in `interp/`, `Vernacexpr` in `vernac/` and + so on. Changes should be compatible, but in a few cases stricter + layering requirements may mean that functions have moved. In all + cases adapting is a matter of changing the module name. + +Vernacular commands + +- The implementation of vernacular commands has been refactored so it + is self-contained now, including the parsing and extension + mechanisms. This involves a couple of non-backward compatible + changes due to layering issues, where some functions have been moved + from `Pcoq` to `Pvernac` and from `Vernacexpr` to modules in + `tactics/`. In all cases adapting is a matter of changing the module + name. + +### Unit testing + + The test suite now allows writing unit tests against OCaml code in the Coq + code base. Those unit tests create a dependency on the OUnit test framework. + ## Changes between Coq 8.7 and Coq 8.8 ### Bug tracker @@ -74,6 +141,11 @@ Declaration of printers for arguments used only in vernac command happen. An alternative is to register the corresponding argument as a value, using "Geninterp.register_val0 wit None". +Types Alias deprecation and type relocation. + +- A few type alias have been deprecated, in all cases the message + should indicate what the canonical form is. + ### STM API The STM API has seen a general overhaul. The main change is the diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt index b3d49b7e56..764d482957 100644 --- a/dev/doc/coq-src-description.txt +++ b/dev/doc/coq-src-description.txt @@ -17,12 +17,6 @@ toplevel Special components ------------------ -intf : - - Contains mli-only interfaces, many of them providing a.s.t. - used for dialog bewteen coq components. Ex: Constrexpr.constr_expr - produced by parsing and transformed by interp. - grammar : Camlp5 syntax extensions. The file grammar/grammar.cma is used diff --git a/dev/doc/debugging.md b/dev/doc/debugging.md index fd3cbd1bc3..14a1cc693c 100644 --- a/dev/doc/debugging.md +++ b/dev/doc/debugging.md @@ -47,7 +47,7 @@ Debugging with ocamldebug from Emacs 7. some hints: - To debug a failure/error/anomaly, add a breakpoint in - Vernac.vernac_com at the with clause of the "try ... interp com + `Vernac.interp_vernac` (in `toplevel/vernac.ml`) at the with clause of the "try ... interp com with ..." block, then go "back" a few steps to find where the failure/error/anomaly has been raised - Alternatively, for an error or an anomaly, add breakpoints in the middle diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md new file mode 100644 index 0000000000..1821a181f1 --- /dev/null +++ b/dev/doc/release-process.md @@ -0,0 +1,100 @@ +# Release process # + +## As soon as the previous version branched off master ## + +- [ ] Create a new issue to track the release process where you can copy-paste + 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)). +- [ ] 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. +- [ ] Create the `X.X+beta1` milestone if it did not already exist. +- [ ] Decide the release calendar with the team (freeze date, beta date, final + release date) and put this information in the milestone (using the + description and due date fields). + +## About one month before the beta ## + +- [ ] Create the `X.X.0` milestone and set its due date. +- [ ] Send an announcement of the upcoming freeze on Coqdev and ask people to + remove from the beta milestone what they already know won't be ready on time + (possibly postponing to the `X.X.0` milestone for minor bug fixes, + infrastructure and documentation updates). +- [ ] Determine which issues should / must be fixed before the beta, add them + to the beta milestone, possibly with a + ["priority: blocker"](https://github.com/coq/coq/labels/priority%3A%20blocker) + label. Make sure that all these issues are assigned (and that the assignee + provides an ETA). +- [ ] Ping the development coordinator (**@mattam82**) to get him started on + the update to the Credits chapter of the reference manual. + See also [#7058](https://github.com/coq/coq/issues/7058). + The command to get the list of contributors for this version is + `git shortlog -s -n VX.X+alpha..master | cut -f2 | sort -k 2` + (the ordering is approximative as it will misplace people with middle names). + +## On the date of the feature freeze ## + +- [ ] Create the new version branch `vX.X` and + [protect it](https://github.com/coq/coq/settings/branches) + (activate the "Protect this branch", "Require pull request reviews before + merging" and "Restrict who can push to this branch" guards). +- [ ] Remove all remaining unmerged feature PRs from the beta milestone. +- [ ] Start a new project to track PR backporting. The proposed model is to + have a "X.X-only PRs" column for the rare PRs on the stable branch, a + "Request X.X inclusion" column for the PRs that were merged in `master` that + are to be considered for backporting, a "Waiting for CI" column to put the + PRs in the process of being backported, and "Shipped in ..." columns to put + what was backported. (The release manager is the person responsible for + merging PRs that target the version branch and backporting appropriate PRs + that are merged into `master`). + A message to **@coqbot** in the milestone description tells it to + automatically add merged PRs to the "Request X.X inclusion" column. +- [ ] Delay non-blocking issues to the appropriate milestone and ensure + blocking issues are solved. If required to solve some blocking issues, + it is possible to revert some feature PRs in the version branch only. + +## 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 + packages. +- [ ] Change the version name from alpha to beta1 (see + [#7009](https://github.com/coq/coq/pull/7009/files)). + We generally do not update the magic numbers at this point. +- [ ] Put the `VX.X+beta1` tag using `git tag -s`. + +### These steps are the same for all releases (beta, final, patch-level) ### + +- [ ] Send an e-mail on Coqdev announcing that the tag has been put so that + package managers can start preparing package updates. +- [ ] Draft a release on GitHub. +- [ ] Get **@maximedenes** to sign the Windows and MacOS packages and + upload them on GitHub. +- [ ] Prepare a page of news on the website with the link to the GitHub release + (see [coq/www#63](https://github.com/coq/www/pull/63)). +- [ ] Upload the new version of the reference manual to the website. + *TODO: setup some continuous deployment for this.* +- [ ] Merge the website update, publish the release + and send annoucement e-mails. +- [ ] Ping **@Zimmi48** to publish a new version on Zenodo. + *TODO: automate this.* +- [ ] Close the milestone + +## At the final release time ## + +- [ ] Change the version name to X.X.0 and the magic numbers (see + [#7271](https://github.com/coq/coq/pull/7271/files)). +- [ ] Put the `VX.X.0` tag. + +Repeat the generic process documented above for all releases. + +- [ ] Switch the default version of the reference manual on the website. + +## At the patch-level release time ## + +We generally do not update the magic numbers at this point (see +[`2881a18`](https://github.com/coq/coq/commit/2881a18)). |