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/63a6f7f3-c0ac-4d32-817f-92fdaedea76cn%40googlegroups.com.
