diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/MERGING.md | 52 | ||||
| -rw-r--r-- | dev/doc/changes.md | 20 | ||||
| -rw-r--r-- | dev/doc/coq-src-description.txt | 6 | ||||
| -rw-r--r-- | dev/doc/debugging.md | 2 |
4 files changed, 69 insertions, 11 deletions
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index 71fc396088..84ff94c66a 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -1,6 +1,7 @@ # Merging changes in Coq -This document describes how patches (submitted as Pull Requests) should be +This document describes how patches (submitted as pull requests +on the `master` branch) should be merged into the main repository (https://github.com/coq/coq). ## Code owners @@ -65,14 +66,57 @@ 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. + +### What to do if the PR has overlays + +If the PR breaks compatibility of some developments in CI, then the author must +have prepared overlays for these developments (see [`dev/ci/README.md`](/dev/ci/README.md)) +and the PR must absolutely update the `CHANGES` file. + +There are two cases to consider: + +- If the patch is backward compatible (best scenario), then you should get + upstream maintainers to integrate it before merging the PR. +- If the patch is not backward compatible (which is often the case when + patching plugins after an update to the Coq API), then you can proceed to + merge the PR and then notify upstream they can merge the patch. This is a + less preferable scenario because it is probably going to create + spurious CI failures for unrelated PRs. + +### 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 tutorial to +creating your own GPG key: +<https://ekaia.org/blog/2009/05/10/creating-new-gpgkey/> + +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..2bad21bb20 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,3 +1,23 @@ +## Changes between Coq 8.8 and Coq 8.9 + +### ML API + +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. + ## Changes between Coq 8.7 and Coq 8.8 ### Bug tracker 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 |