Github actions: docs for cross-project merges

[sv2518]

Following description is a collection of thoughts from the the discussion in PR #2068 and #2038.

In the action for building docs, the doc build runs in the most recently built trunk container, so the branches e.g. of loopy might be out of date. This is a problem for cross-project merges.
First idea to fix this was by firedrake-updating before building the docs, where firedrake-update is meant to update itself to the branch it's running on. But we are using the vanilla Docker container so Firedrake is installed into /home/firedrake/firedrake. It's possible that firedrake-update is using the Firedrake installed there (master) instead of the one we are testing.

What would be the best way to get this done properly?

[connorjward]

It's not pleasant but perhaps you could just modify the workflow file to run:

$ git -C /home/firedrake/firedrake/src/loopy checkout <test branch>

[wence-]

firedrake-update should DTRT thing though.

[connorjward]

But what is the right thing? We are installing a separate version of Firedrake when we run this action. Is it reasonable to expect firedrake-update to know about this? Perhaps we could get the action to checkout Firedrake into the venv instead of introducing a second one.

[wence-]

OIC, hmmm

[sv2518]

Okay so I have changed the action so it only works on one Firedrake in #2071, which should make it a bit more clear what is happening in it. Kudos to @connorjward for explaining.

The second part I'd quite like to introduce is a file which contains the branches of external packages, which the PR depends on being merged too, so e.g. loopy. In the docs build and in the Jenkins run we can then firedrake-update with a new option, something like --checkout-dependent-branches that picks up the branches from the file. We would obviously not want to merge that file.
I want that because a) I am lazy and don't always want to search for the line were I need to add those dependent branches and b) we could potentially avoid some of those "Drop before merge" commits by having an empty version of the file on master and specifying a merge strategy (Maybe in .attributes?), which always keeps the version that is on master when we merge a PR. I am not sure yet how the merge strategy will work, I will need to read a bit more about it. Otherwise the person who opens a cross-project PR would need to empty the file before it's merged.

[connorjward]

I like the idea of dropping the file automatically from the merge.

Also this would need to work for firedrake-install as well because that's the command Jenkins uses.