aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-20 18:02:29 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-20 18:03:16 +0100
commitbc0fa22b91b55a110def7daec66713d2a7fb909e (patch)
tree4b7b1b1f917eae680c132694660a7ba117c79474
parentf21deb6c861b359f0d3bf8b170d277cfa0d80171 (diff)
parent45d8669d4f3cf009ee71c109fafd9d0fc9a9862c (diff)
Merge PR #7014: New merging process
The last merge with the centralized process ;)
-rw-r--r--.github/CODEOWNERS118
-rw-r--r--dev/doc/MERGING.md54
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.