diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-03-20 18:02:29 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-20 18:03:16 +0100 |
commit | bc0fa22b91b55a110def7daec66713d2a7fb909e (patch) | |
tree | 4b7b1b1f917eae680c132694660a7ba117c79474 | |
parent | f21deb6c861b359f0d3bf8b170d277cfa0d80171 (diff) | |
parent | 45d8669d4f3cf009ee71c109fafd9d0fc9a9862c (diff) |
Merge PR #7014: New merging process
The last merge with the centralized process ;)
-rw-r--r-- | .github/CODEOWNERS | 118 | ||||
-rw-r--r-- | dev/doc/MERGING.md | 54 |
2 files changed, 172 insertions, 0 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS new file mode 100644 index 000000000..0f8b0a2cd --- /dev/null +++ b/.github/CODEOWNERS @@ -0,0 +1,118 @@ +# This file describes the maintainers for the main components. See +# `dev/doc/MERGING.md`. + +# component-path principal-maintainer secondary-maintainer + +# GitHub metadata, including this file +/.github/ @maximedenes @Zimmi48 + +# CI infrastructure +/dev/ci/*.sh @ejgallego @SkySkimmer +/.travis.yml @ejgallego @SkySkimmer +/.gitlab-ci.yml @SkySkimmer @ejgallego +/.appveyor.yml @maximedenes @SkySkimmer + +/default.nix @Zimmi48 @vbgl + +# Documentation +/README.md @Zimmi48 @maximedenes +/INSTALL* @Zimmi48 @maximedenes +/CONTRIBUTING.md @Zimmi48 @maximedenes +/dev/doc/ @Zimmi48 @maximedenes +/doc/ @silene @maximedenes +/man/ @silene @maximedenes + +/checker/ @barras @maximedenes + +/clib/ @ppedrot @ejgallego + + +/engine/ @ppedrot @aspiwack + +/grammar/ @ppedrot @maximedenes + +/ide/ @ppedrot @gares + +/interp/ @herbelin @ejgallego + +/intf/ @letouzey @ppedrot +/kernel/ @maximedenes @barras +/kernel/byterun/ @maximedenes @silene +/lib/ @ejgallego @ppedrot +/library/ @silene @gares + +/parsing/ @herbelin @mattam82 + +/plugins/btauto/ @ppedrot @herbelin + +/plugins/cc/ @herbelin # I don't know Pierre Corbineau's GitHub nickname +/plugins/derive/ @aspiwack @ppedrot +/plugins/extraction/ @letouzey @maximedenes +/plugins/firstorder/ @herbelin # I don't know Pierre Corbineau's GitHub nickname +/plugins/fourier/ @herbelin @gares +/plugins/funind/ @forestjulien @Matafou +/plugins/ltac/ @ppedrot +/plugins/micromega/ @fajb @bgregoir +/plugins/nsatz/ @thery @ppedrot +/plugins/omega/ @letouzey +/plugins/romega/ @letouzey +/plugins/setoid_ring/ @amahboubi @bgregoir +/plugins/ssrmatching/ @gares @maximedenes +/plugins/ssr/ @gares @maximedenes +/plugins/syntax/ @ppedrot @maximedenes + + +/plugins/quote/ @herbelin + +/plugins/rtauto/ @herbelin # Should be Pierre Corbineau too + +/pretyping/ @mattam82 @gares +/printing/ @herbelin @mattam82 + +/proofs/ @ppedrot @Zimmi48 + +/stm/ @gares @ejgallego + +/tactics/ @ppedrot @mattam82 + +/theories/Arith/ @letouzey @herbelin +/theories/Bool/ @letouzey @herbelin +/theories/Classes/ @mattam82 @herbelin +/theories/FSets/ @letouzey @herbelin +/theories/Init/ @letouzey @ppedrot +/theories/Lists/ @letouzey @ppedrot +/theories/Logic/ @herbelin @ppedrot +/theories/MSets/ @letouzey @herbelin +/theories/NArith/ @letouzey @herbelin +/theories/Numbers/ @letouzey @herbelin +/theories/PArith/ @letouzey @herbelin +/theories/Program/ @mattam82 @herbelin +/theories/QArith/ @letouzey @herbelin +/theories/Reals/ @silene @ppedrot +/theories/Relations/ @mattam82 @ppedrot +/theories/Setoids/ @mattam82 @ppedrot +/theories/Sets/ @letouzey @herbelin +/theories/Sorting/ @letouzey @herbelin +/theories/Strings/ @letouzey @herbelin +/theories/Structures/ @letouzey @herbelin +/theories/Unicode/ @letouzey @herbelin +/theories/Wellfounded/ @letouzey @mattam82 +/theories/ZArith/ @letouzey @herbelin + +/theories/Compat/ @JasonGross @Zimmi48 + +/theories/Vectors/ @herbelin + +/tools/coqdoc/ @silene @mattam82 +/tools/coq_makefile* @gares @silene +/tools/CoqMakefile* @gares @silene +/tools/coqdep* @ppedrot @maximedenes +/tools/coq_tex* @silene @gares +/tools/coqwc* @silene @gares + +/toplevel/ @ejgallego @gares +/vernac/ @mattam82 @maximedenes + +/Makefile* @letouzey @ejgallego +/configure* @letouzey @ejgallego +/META.coq @letouzey @ejgallego diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md new file mode 100644 index 000000000..df366a978 --- /dev/null +++ b/dev/doc/MERGING.md @@ -0,0 +1,54 @@ +# 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). + +## Code owners + +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 these two +maintainers for a review. If the pull request touches several parts, all the +corresponding maintainers will be asked for a review. + +Maintainers are never assigned as reviewer on their own PRs. + +## Reviewing + +When principal maintainers receive a review request, they are expected to: + +* Put their name in the assignee field, if they are in charge of the component + that is the main target of the patch (or if they are the only principal + maintainer asked to review the PR). +* Review the PR, approve it or request changes. +* If they are the assignee, check if all reviewers approved the PR. If not, + regularly ping the author (if changes should be implemented) or the reviewers + (if reviews are missing). The assignee ensures that any requests for more + discussion have been granted. When the discussion has converged and all + reviewers have approved the PR, the assignee is expected to follow the merging + process described below. + +In all cases, maintainers can delegate reviews to the other maintainer of the +same component, except if it would lead to a maintainer reviewing their own +patch. + +A maintainer is expected to be reasonably reactive, but no specific timeframe is +given for reviewing. + +## Merging + +Once all reviewers approved the PR, the assignee is expected to check that CI +completed without relevant failures, and that the PR comes with appropriate +documentation and test cases. If not, they should leave a comment on the PR and +put the approriate label. Otherwise, they are expected to merge the PR using the +[merge script](/dev/tools/merge-pr.sh). + +The command to be used is: +``` +$ dev/tools/merge-pr XXXX +``` +where `XXXX` is the number of the PR to be merged. This operation should be followed by a push. + +Maintainers MUST NOT merge their own patches. |