CI: Test PR head

[nomeata]

by default, Github tests a hypothetical merged state, which can lead to PRs being red although they are perfectly fine. That’s annoying.

https://frontside.com/blog/2020-05-26-github-actions-pull_request/#how-does-pull_request-affect-actionscheckout

[rossberg]

Hm, I have to admit that I don't understand the difference. Will this still ensure that merging a green PR cannot break main?

[nomeata]

I'd you want that property as well, you should enable “strict merges” as well, which is good practice anyways.

(Even right now you don't have that property, I believe, as GitHub doesn't rerun all PR CIs when you update main…)

[rossberg]

Our workflows are configured to trigger when a commit is pushed to main. So I do believe we currently have this property, which seems relevant.

[nomeata]

Oh, are they? Are you sure? When you pushed 0aaed97 to main I didn't see builds for all PRs being triggered (else https://github.com/Wasm-DSL/spectec/actions would be much more noisy).

But if you say so I can keep an eye and see if that actually happens.

(I still prefer strict merges, it's simpler and easier to juggle multiple dependent PRs).

[rossberg]

See the workflow triggers here. I'm pretty sure I have observed this.

What are "strict merges"? I can't find anything under that title in the settings.

I should probably enable branch protection for main, but I did not bring my Yubikey with me.

[nomeata]

I don't think these triggers do what you say. They say “test main when main is pushed to” and “test any PR into main when the PR is changed”, to the best of my knowledge.

Strict merges means that before one press merge, one has to first merge main into the feature branch. It also makes the “merge main into this” button appear in the GitHub UI.

See https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/managing-protected-branches/about-protected-branches#require-status-checks-before-merging. It seems the option is only available of you also guard PRa on passing CI, which is useful too.

(No worries, as admin you can still allow yourself to push to main directly.)

[rossberg]

I don't think these triggers do what you say. They say “test main when main is pushed to” and “test any PR into main when the PR is changed”, to the best of my knowledge.

Actually, no. The semantics of plain on: push is to trigger "when a push is made to any branch in the workflow's repository". The branches: main then is a filter to only consider push events on main. See e.g. here.

[nomeata]

So, ea48704 was just made to main one hour ago. CI checked main, but nothing more:

But none of the PR’s CI was re-run.

I see how the docs are misleading, but this being github, one cannot expect common sensical expectations to just hold…

[rossberg]

That is odd. This is explained at length in the docs with various examples, so the docs wouldn't just be misleading, but plain lies. That seems unlikely, so I assume something else has gone wrong. I had issues with path filters before, but they look fine.

[nomeata]

https://stackoverflow.com/a/74971885/946226 says it’s not possible.

[rossberg]

Okay, I have no idea what's going on anymore. Perhaps the docs are very misleading.

In any case I'll make sure to activate branch protection once I get back. However, I still don't see where the UI lets me choose between "strict" and "loose", like the doc link you gave me claims.

As for this PR, I'm still a bit puzzled. What's a scenario where a PR is red spuriously, but you wouldn't have to fix anything to make it mergeable? (Provided main itself isn't broken.)

[nomeata]

In any case I'll make sure to activate branch protection once I get back. However, I still don't see where the UI lets me choose between "strict" and "loose", like the doc link you gave me claims.

I think it’s part of activating branch protection and selecting the CI jobs that need to parse.

As for this PR, I'm still a bit puzzled. What's a scenario where a PR is red spuriously, but you wouldn't have to fix anything to make it mergeable? (Provided main itself isn't broken.)

Ah: I prefer (but it’s just a preference) if a green check mark means „this code works“ (as a pure function of the branch state, not depending on what else happens in the repo). Whether it needs to be merged or not is then (if strict branch protection is on) signaled by „This branch is out of date“.

[rossberg]

I think it’s part of activating branch protection and selecting the CI jobs that need to parse.

That's where I looked and couldn't find it.

Ah: I prefer (but it’s just a preference) if a green check mark means „this code works“ (as a pure function of the branch state, not depending on what else happens in the repo). Whether it needs to be merged or not is then (if strict branch protection is on) signaled by „This branch is out of date“.

Okay, makes sense.

[nomeata]

This is the checkbox that’d be needed

[rossberg]

Yes, but I was expecting some reference to "strict" vs "loose". But rereading the table from the link that's just terminology they made up there. Took me a while to see that. Thanks for bearing with me.

[nomeata]

It just happened again: #28 was green and it said no merge conflicts, so I merged. But there were changes on main that happened since my PR was CIed, and main turned red.

If we require PRs to be up to date before merging, then this would not have happened.

[nomeata]

Did you actually check “Require branches to be up to date before merging” (I cannot see the settings)? I shouldn’t merge this PR before that is checked.