search

metamath / set.mm

Metamath source file for logic and set theory
Other
255 stars 89 forks source link

Use a merge queue to check for verification failures before merging pull requests #4228

Open BTernaryTau opened 2 months ago

BTernaryTau commented 2 months ago

It seems like it would be worth setting up a merge queue to rerun the verifier checks for a pull request immediately before merging it. This should prevent any more incidents like the one described in #4214 and #4215.

wlammen commented 2 months ago

This was really a rare event, so it is not a much missed feature. Nevertheless: Pull request merge queues are available in any public repository owned by an organization, ... If we qualify as an organization, then let's go ahead.

icecream17 commented 2 months ago

We do qualify as an org

Another documentation link: https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/configuring-pull-request-merges/managing-a-merge-queue

wlammen commented 2 months ago

What is at stake here: For a short period of time (around a quarter of an hour), the database was in an inconsistent state, i.e. discouraged file and .mm file did not match. Should someone fork or download the database in such a moment, he or she will see verification errors when pushing back contents, without knowing what is going on.

GinoGiotto commented 2 months ago

I think we should also take a look at the options:

To get more familiar with how they work, I opened a dummy organization and done some testing, you can do the same by opening your own organization (there is a free plan).

My first impression is that these options are probably fine, but maybe we can lower the "status check timeout" since set.mm CI usually does not exceed 4 minutes. In my tests I also noticed that the merge method seems forced to be the same for everyone, while currently I believe @jkingdon uses a different one, so this might need some discussion.

jkingdon commented 2 months ago

My first impression is that these options are probably fine, but maybe we can lower the "status check timeout" since set.mm CI usually does not exceed 4 minutes.

There's some variability in how long the checks take, but something like 10 minutes should give us enough padding, because something around 3 or 4 minutes is indeed the typical run time (which could be even shorter if someone takes on #4196 and it works out).

In my tests I also noticed that the merge method seems forced to be the same for everyone, while currently I believe @jkingdon uses a different one, so this might need some discussion.

What I have been doing is rebase-and-merge when the commits seem to be carefully organized, or squash-and-merge when the commits are just "fix typo" and other things which wouldn't be very interesting to keep separate in the long term. There are also cases where github will only do a squash-and-merge (I think it is when the branch contains a merge commit, but I'm not 100% sure on exactly when it happens), so I'll do the squash-and-merge then too.

But unless there is someone who is really attached to the fine grained commits, I'm fine with standardizing on squash-and-merge. My understanding is yours, that using a merge queue would involve picking a method.

benjub commented 2 months ago

What I have been doing is rebase-and-merge when the commits seem to be carefully organized, or squash-and-merge when the commits are just "fix typo" and other things which wouldn't be very interesting to keep separate in the long term. There are also cases where github will only do a squash-and-merge (I think it is when the branch contains a merge commit, but I'm not 100% sure on exactly when it happens), so I'll do the squash-and-merge then too.

But unless there is someone who is really attached to the fine grained commits, I'm fine with standardizing on squash-and-merge. My understanding is yours, that using a merge queue would involve picking a method.

I digress a bit from the initial proposal, but: I prefer squash-and-merge too, and I sometimes edit the merge message when there are things like "fix typo" too. I prefer it since it doesn't overwhelm the git history (the output of git log for instance). Also, knowing that everyone will squash-and-merge, you will not shy away from pushing new commits instead of doing force-pushes which make reviews harder.

jkingdon commented 2 months ago

I sometimes edit the merge message when there are things like "fix typo" too

Unless I'm misreading the documentation for merge queues, this wouldn't be possible when using merge queues.

In fact, browsing through https://github.com/Merge-queues/Test-merge-queues/commits/main/ I don't see the commit messages being kept at all. Is that really true? That seems bit hard to believe, so maybe there is some setting or something?

GinoGiotto commented 2 months ago

In fact, browsing through Merge-queues/Test-merge-queues@main (commits) I don't see the commit messages being kept at all. Is that really true? That seems bit hard to believe, so maybe there is some setting or something?

I merged this new PR using squash-and-merge (changed in the general settings), the commit message is preserved https://github.com/Merge-queues/Test-merge-queues/commits/main/.

However indeed, I don't see how to manually edit it. Normally, when pressing the dropdown arrow, a menu would appear, allowing the user to choose the merge option and then modify the commit message:

But when merge queues are active, none of that appears, only a button:

It seems other people have already noticed this: https://github.com/orgs/community/discussions/15925 https://github.com/orgs/community/discussions/111224.

BTernaryTau commented 2 months ago

That's unfortunate. I'm guessing that these sorts of conflicts come up rarely enough that using a merge queue isn't worth it until editing the merge commit message is possible?