On Tue, Dec 14, 2021 at 12:28 PM David A. Wheeler <[email protected]> wrote:
> > > On Dec 13, 2021, at 10:33 PM, Mario Carneiro <[email protected]> wrote: > > > > I think that a 5 day waiting period is too long, and indeed I don't > think there should be any time-based review barrier. For contributions to > main set.mm, I would propose that we have a simple system where at least > 2 people sign off on each PR: the author and at least one > maintainer/reviewer (not equal to the author). CI is quick so we can make > it a requirement for merging. > > I'm fine with omitting a waiting period! I suggested the "5 days" to > increase the likelihood of people agreeing to *a* merge criterion. > > But if "another maintainer approved" is generally acceptable as a merge > criterion, that's even better. > > So who does the merge? I guess any maintainer can trigger the merge once > the conditions are met? > Yes. Obviously it has to be someone with write permissions, but I think most of our contributors have such permission on set.mm already. > I think we should have designated maintainers for parts of set.mm. Any > changes to that section should be reviewed by at least one designated > maintainer. There aren't too many daily active contributors so possibly we > can just all be maintainers of everything to start, but some people have > their own pet sections and we should make an attempt to write down > everyone's area of expertise so that we know who to ping. > > Sounds good. I'll call those "area maintainers". Let's start with the > empty set. > > If anyone has a "pet section" or "pet database" > they want to review all changes to, please post here on the mailing list. > If there's general agreement, we'll add them to an "area maintainers" > list in the set.mm README. The rule would be, all changes to the area > (database or database section) > would require a review from one of those area maintainers before being > accepted. > Personally, I would put my area of expertise as overall set.mm cohesion and design, although there are also plenty of individual sections that I have contributed to. Of late I haven't had much time to devote to PR reviews though, so it will need more than just me if we want to keep the queue flowing. I think Jim Kingdon should take point on iset.mm maintenance, and others should speak up if they want to participate more in maintenance. > For mathbox-only changes, I would stick to the 1 reviewer rule but most > likely only a cursory examination is required. > > Fair enough. I imagine they'll mainly be looking for statements that might > interfere with others. > > If *every* pull request requires review & approval by someone else, we > could even enforce that via GitHub rule. > That might be a good thing. One of the main advantages of set.mm is how > rigorously verified it is > (every change is verified by multiple independent verifiers, etc.). Having > enforced review could help > us convince *others* that we take this database seriously. We don't need > to turn that on now, > but it might be worth thinking about. > It's a possibility, but I don't think we need to make the structures unnecessarily rigid. Most of our contributors are able to work well together without a heavy coordination framework and I'd like to keep it that way, at least until experience suggests that more structure will help more than hinder. Which is to say, I think we can function on the honor system for now. One thing that I think we should stick to is one commit per PR. We had a similar discussion for metamath-knife but for set.mm it's important to keep PR sizes down so that people can reasonably review them, and squash merges keep things organized. This is the mechanism we've been using in mathlib and it works well to avoid merge conflicts, especially when things scale to many concurrent PRs. Mario -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSsiZmtp3x%2BW6VOpUY_GSzANFWRCXrdx8aA5gNcT-UMzDQ%40mail.gmail.com.
