Coq: Change of maintainers for checker and kernel

Created on 25 Apr 2018  路  5Comments  路  Source: coq/coq

@barras is listed as the primary maintainer for the checker (and @maximedenes as the second one) and as the secondary maintainer for the kernel (and @maximedenes as the primary one) but he hasn't answered to #7032 (which basically amounts to a "No"). He has also never participated to the development since it moved to GitHub and his last commit predates the 8.5 release. So it means that we are currently without a primary maintainer for the checker and a secondary maintainer for the kernel.

Possible candidates: @mattam82 @ppedrot @SkySkimmer

https://github.com/coq/coq/blob/72d6d5e87759b62dcd9974c87bf59496d27e10b0/.github/CODEOWNERS#L55-L56
https://github.com/coq/coq/blob/72d6d5e87759b62dcd9974c87bf59496d27e10b0/.github/CODEOWNERS#L91-L92

meta

Most helpful comment

Separate maintainers for univ stuff | VM and native stuff | other kernel stuff sounds reasonable.
It kind of resembles our part: labels too.

All 5 comments

Pending on some IRL chat with @barras to know what his plans wrt to Coq are.

I already said that somewhere, but I believe that we need to involve as many persons as possible for the kernel and for the checker. Only one main owner does not reflect the complexity of the kernel internals, as devs typically have knowledge over a subset of the several components from the kernel (e.g. universes, inductive types, VM, conversion...).

If these subsets correspond to different files it is easy using GitHub CODEOWNER file to specify more than one maintainer for the kernel. For instance, we could put @SkySkimmer as a maintainer for kernel/univ.ml{,i}.
Otherwise, we can just expect people to comment / review PRs whenever they are competent even if they are not official maintainers. The maintainer's role is just to manage the reviewing / merging process. This requires the maintainer to be reactive but it doesn't mean that this person is the only one who must review.

Separate maintainers for univ stuff | VM and native stuff | other kernel stuff sounds reasonable.
It kind of resembles our part: labels too.

This has been mostly solved. @barras is still listed as a secondary maintainer of the kernel if he ever wants to come back but we don't depend on him.

Was this page helpful?
0 / 5 - 0 ratings