From 965c63f36c928c6e901f0f7f7a72a259f844f70c Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 26 Mar 2018 15:00:11 +0200 Subject: Adapt CONTRIBUTING to recent changes in Coq. - The testing and benchmarking labels are now distinct. - The release manager does not take care of merging anymore. - The reference manual is not written in LaTeX anymore. --- CONTRIBUTING.md | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 213b877351..1a3c993697 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -38,13 +38,11 @@ Whitespace discipline (do not indent using tabs, no trailing spaces, text files Here are a few tags Coq developers may add to your PR and what they mean. In general feedback and requests for you as the pull request author will be in the comments and tags are only used to organize pull requests. -- [needs: rebase](https://github.com/coq/coq/pulls?utf8=%E2%9C%93&q=is%3Aopen%20is%3Apr%20label%3A%22needs%3A%20rebase%22%20) indicates the PR should be rebased on top of the latest `master` branch. See the [GitHub documentation](https://help.github.com/articles/about-git-rebase/) for a brief introduction to using `git rebase`. +- [needs: rebase](https://github.com/coq/coq/pulls?utf8=%E2%9C%93&q=is%3Aopen%20is%3Apr%20label%3A%22needs%3A%20rebase%22) indicates the PR should be rebased on top of the latest `master` branch. See the [GitHub documentation](https://help.github.com/articles/about-git-rebase/) for a brief introduction to using `git rebase`. - [needs: fixing](https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+fixing%22) indicates the PR needs a fix, as discussed in the comments. -- [needs: testing](https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+testing%22) indicates the PR needs testing. This is often used when testing beyond what the test suite can handle is required. For example, performance benchmarking is currently performed with a different infrastructure. Unless some followup is specifically requested you aren't expected to do this additional testing. +- [needs: benchmarking](https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+benchmarking%22) and [needs: testing](https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+testing%22) indicate the PR needs testing beyond what the test suite can handle. For example, performance benchmarking is currently performed with a different infrastructure. Unless some followup is specifically requested you aren't expected to do this additional testing. -The release manager uses the following filter to know which PRs seem ready for merge. If you are waiting for a PR to be merged, make sure it appears in this list: - -- [Pull requests ready for merge](https://github.com/coq/coq/pulls?utf8=%E2%9C%93&q=is%3Apr%20is%3Aopen%20-label%3A%22needs%3A%20discussion%22%20-label%3A%22needs%3A%20testing%22%20-label%3A%22needs%3A%20fixing%22%20-label%3A%22needs%3A%20progress%22%20-label%3A%22needs%3A%20rebase%22%20-label%3A%22needs%3A%20review%22%20-label%3A%22needs%3A%20help%22%20-label%3A%22needs%3A%20independent%20fix%22%20-label%3A%22needs%3A%20feedback%22%20-label%3A%22help%20wanted%22%20-review%3Achanges_requested%20-status%3Apending%20base%3Amaster%20sort%3Aupdated-asc%20-label%3A%22needs%3A%20squashing%22%20) +To learn more about the merging process, you can read the [merging documentation for Coq maintainers](/dev/doc/MERGING.md). ## Documentation @@ -52,7 +50,7 @@ Currently the process for contributing to the documentation is the same as for c Our issue tracker includes a flag to mark bugs related to documentation. You can view a list of documentation-related bugs using a [GitHub issue search](https://github.com/coq/coq/issues?q=is%3Aopen+is%3Aissue+label%3A%22kind%3A+documentation%22). Many of these bugs can be fixed by contributing writing, without knowledge of Coq's OCaml source code. -The sources for the [Coq reference manual](https://coq.inria.fr/distrib/current/refman/) are at [`doc/refman`](/doc/refman). These are written in LaTeX and compiled to HTML with [HeVeA](http://hevea.inria.fr/). +The sources for the [Coq reference manual](https://coq.inria.fr/distrib/current/refman/) are at [`doc/sphinx`](/doc/sphinx). These are written in reStructuredText and compiled to HTML and PDF with [Sphinx](http://www.sphinx-doc.org/). You may also contribute to the informal documentation available in [Cocorico](https://github.com/coq/coq/wiki) (the Coq wiki), and the [Coq FAQ](https://github.com/coq/coq/wiki/The-Coq-FAQ). Both of these are editable by anyone with a GitHub account. -- cgit v1.2.3 From 19bbdb467360578c98d9787a9aebca4bf246a8e9 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 26 Mar 2018 15:46:33 +0200 Subject: Improve the MERGING doc. In particular, describes what to do with overlays. --- dev/doc/MERGING.md | 34 +++++++++++++++++++++++++++++++--- 1 file changed, 31 insertions(+), 3 deletions(-) diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index 71fc396088..70d8481887 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,41 @@ 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 ``` +$ git checkout master +$ git pull $ dev/tools/merge-pr 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. -- cgit v1.2.3 From 274da8930804b2187568423c3bfeed541f235001 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 26 Mar 2018 15:55:46 +0200 Subject: Some advice about merge script dependencies. Including: how to create a GPG key. --- dev/doc/MERGING.md | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index 70d8481887..402ed37bdc 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -104,3 +104,14 @@ There are two cases to consider: 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: + + +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. -- cgit v1.2.3 From 6dd06d92aad8ccd130b4d46b2ff79b71b148bb2b Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 5 Apr 2018 12:01:24 +0200 Subject: Add note for homebrew users. --- dev/doc/MERGING.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index 402ed37bdc..3a2df6a81f 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -115,3 +115,8 @@ creating your own GPG key: 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)). -- cgit v1.2.3