> 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? > 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. > 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. > Regarding the top date, I have said this before and I'll say it again: we > should just abandon it. It is a completely unnecessary merge hazard and I > don't know any other git-based project that checks in a date that changes on > every commit. (A version number might make more sense, but I don't think that > set.mm needs version numbers.) Git is perfectly capable of tracking the > commit date in a way that does not create rampant merge conflicts. I'm fine with removing the top date, let's do it. I think it's a vestige of the time before this was managed by git. --- David A. Wheeler -- 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/136549AD-F13E-495E-B503-857A98786D4D%40dwheeler.com.
