Benoit, I've sent you an invite to the set.mm team, so you should be able to review and merge PRs now.
On Mon, Dec 20, 2021 at 8:35 AM Benoit <[email protected]> wrote: > I volunteer for being a maintainer (for all parts of all databases --- I'm > not sure differentiating by parts is useful at this stage: a maintainer > should abstain from approving something he does not understand, and I > certainly will). I think I have no GitHub permissions, so you may open them > when you have time. Thanks. > Benoît > > On Wednesday, December 15, 2021 at 11:19:07 AM UTC+1 Alexander van der > Vekens wrote: > >> In general, providing and handling PRs should be as simple as possible. I >> am not very experienced with Git, and I was happy that everything which was >> essential needed worked: As long as there were no merge conflicts, I just >> pushed my changes to my forked repository using GitHib Desktop, and a PR >> was created automatically by Github. If there were merge conflicts, I >> updated my forked repository by pulling the latest version of set.mm.git >> develop, resolving the merge conflicts, and pushed again. There should >> be not (much) more I have to do. >> >> About the reviews and maintainers: we must distinguish between reviewers >> and persons performing the merging: Since it seems that I have only >> restricted permissions (no write permissions?), I can only be a reviewer >> and could approve PRs. Two approvals should be sufficient for changes of >> the main part (except moving theorems from mathboxes only, see below), and >> no approval for changes in the own mathbox (the person performing the >> merging should have a quick look at it). Changing other mathboxes are >> sometimes required (e.g. if theorems are moved to the main part, or >> maintenace actions are performed, e.g. proof minimizations) - for this, >> maybe only one approval (not necessarily by the mathbox owner(s)) should be >> sufficient. >> >> I could volunteer for being a maintainer for set.mm, Parts >> 2,5,6,7,8,10,11,14,16. >> >> >> On Tuesday, December 14, 2021 at 10:43:13 PM UTC+1 vvs wrote: >> >>> Personally, I like seeing all the commits in my git log history. Using >>>> bisect I can generally piece together what happened when. I often use the >>>> PR history, but I'd hate to not have a local copy of the history to refer >>>> to. >>>> >>> >>> I'd say that it would be made simpler by a more simple history. And vice >>> versa: if there are lots of intertwined commits bisecting will be more >>> difficult. >>> >>> But it shows that it's more important to have simple PRs in a first >>> place rather then relying on squashing it afterwards. >>> >> -- > 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/64cb1a13-ad03-4552-a80c-d9ceb7e6e1c2n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/64cb1a13-ad03-4552-a80c-d9ceb7e6e1c2n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSso2dgpEaBiNjAbjQubJjYrzyxYN29%3D74D_EhMn3QB5wg%40mail.gmail.com.
