Improve build and deployment concurrency handling

[Stephan202]

Suggested commit message:

Improve build and deployment concurrency handling (#284)

Builds for the same branch are now serialized. Among other things this prevents
concurrent deployments.

While there, reduce the permission assigned to each of the two jobs.

[Stephan202]

The commit history shows my tests to reduce the scope of the permissions blocks. The initial attempts failed because I hadn't configured this branch as being allowed to deploy GitHub Pages.

[japborst]

Indeed, an oversight. Thanks for looking into this.
Left some comments.

[japborst]

Did you also consider removing this setting completely? What's the downside of deploying twice?

If I understand correctly, what's happening is:

• PR-1 merged => master is built & deployed
• PR-2 is merged => master is built & deployed

Where PR-2 is somehow faster and thus first PR-2 is deployed, after which PR-1 is deployed and thus leading to an outdated website. Additionally, the current setup is cancelling the build across multiple branches/PRs, which then requires one to manually re-run to fix the build.

Now, we're still grouping globally (group: pages), and this works because the if is on a single branch, but could still lead to issues across multiple branches I think.

Looking at the docs, an alternative would be moving this up again, but grouping differently. Arguably, if we merge the two PRs (from the above example), there's no need in building twice. Additionally, if you push 2 commits on a branch, we should be able to cancel them as - again - there's no use in building twice.

Suggested change

	concurrency:
	group: pages
	cancel-in-progress: true
	concurrency:
	group: ${{ github.ref }}
	cancel-in-progress: true

[Stephan202]

Additionally, if you push 2 commits on a branch, we should be able to cancel them as - again - there's no use in building twice.

This part I agree with (and also crossed my mind).

Arguably, if we merge the two PRs (from the above example), there's no need in building twice.

Strictly speaking true, but IMHO it's a nice feature that each merged commit has a "complete" build status, and that if a merge breaks the build, that the preceding commit still has a "build passed" check mark. (That said, generally @rickie and I don't merge a second PR until the first passed, so in practice there's limited difference.) (And perhaps we should require that PRs are up-to-date with the base branch before merging, but that's yet another discussion.)

[rickie]

Agree with this change, as this is undesirable:

Additionally, the current setup is cancelling the build across multiple branches/PRs, which then requires one to manually re-run to fix the build.

Based on the linked docs, I'd say that this would be even safer (and be prepared on possible future usages of concurrency as well): group: ${{ github.workflow }}-${{ github.ref }}.

[rickie]

I'd say that dropping cancel-in-progress would be fine as well.

Did you also consider removing this setting completely?

However, I'd say that it is nice if you do multiple commits that pending builds will get cancelled:

When a concurrent job or workflow is queued, if another job or workflow using the same concurrency group in the repository is in progress, the queued job or workflow will be pending. Any previously pending job or workflow in the concurrency group will be canceled.

[Stephan202]

Hmm, this was an old comment that I hadn't flushed yet, hence the funny ordering. Anyway, the question is whether we're okay with the PR as-is, or want to add cancel-in-progress: true again.

[rickie]

Suggested some possible tweaks / asked some questions :).

[Stephan202]

Rebased and resolved conflicts.

[Stephan202]

Updated the PR; sorry for the delay. @japborst @rickie WDYT?

[Stephan202]

Additionally, if you push 2 commits on a branch, we should be able to cancel them as - again - there's no use in building twice.

This part I agree with (and also crossed my mind).

Arguably, if we merge the two PRs (from the above example), there's no need in building twice.

Strictly speaking true, but IMHO it's a nice feature that each merged commit has a "complete" build status, and that if a merge breaks the build, that the preceding commit still has a "build passed" check mark. (That said, generally @rickie and I don't merge a second PR until the first passed, so in practice there's limited difference.) (And perhaps we should require that PRs are up-to-date with the base branch before merging, but that's yet another discussion.)

[Stephan202]

Alternatively we could do this, but as discussed it'd be nice not to cancel non-PR builds. I tried to specify cancel-in-progress: ${{ github.head_ref != null }}, but that doesn't seem to work.

[rickie]

Nice discussions! This looks good to me!

it's a nice feature that each merged commit has a "complete" build status

Completely agree.

[rickie]

Rebased. Anything else from your side @japborst 😄?

[japborst]

Went through the comments. Makes sense 👍 Thanks!