Split ci-ubuntu workflow into multiple jobs and add caching

[silas-hw]

ci-ubuntu can be split up into multiple jobs which run in parallel. This also potentially leads the way to further CI improvements. Currently, html generation and standard unit tests run in parallel.

GitHub Actions is a bit of a pain in that there's no way to have some way of setting up an initial workspace for each job to run in. This means that the init steps (set up env, install things, etc...) have to run on every job. To reduce redundant code I split this out into a composite workflow (see https://docs.github.com/en/actions/tutorials/create-actions/create-a-composite-action). This action will be given all the env variables set up by the calling workflow and can likewise set them with the usual write to GITHUB_ENV (see https://github.com/orgs/community/discussions/51280#discussioncomment-8726096).

I'm still not fully confident on this though.

Edit:

Data is now shared between jobs via upload- and download-artifact, as well as output variables if appropriate.

After this is merged, I plan on working more to resolve #2248, starting with more granularity over when jobs run.

[silas-hw]

Seems checkout needs to run first

[gallais]

That summary looks concerning: https://github.com/agda/agda-stdlib/actions/runs/28607124313?pr=3049
In case of cache miss, it looks like you'll rebuild Agda twice (in parallel but that's still wasteful).

I would recommend looking at the structure of the Idris2 CI pipeline:
https://github.com/idris-lang/Idris2/blob/main/.github/workflows/ci-idris2-and-libs.yml

You can see from the summary https://github.com/idris-lang/Idris2/actions/runs/28065704913?pr=3775
that we have a clear dependency graph & reuse artifacts produced in one stage in the later ones
(via actions/upload-artifact@v4).

So you could have a first stage checking whether we have agda in the cache. If not, build it and upload it.
Then have testing and upload the agdai files for the lib.
Then have in parallel golden testing & html generation.
Then deploy the html only if we are in the right branch and everything succeeded.

[silas-hw]

Seems a much better approach indeed. Initially dismissed upload-artificact since it seemed more tedious than needed, but given more thought it seems significantly more reasonable.

[silas-hw]

GITHUB_PATH is only for writing by the looks of it, fixing that now

[silas-hw]

Right now I don't like how sudo is before 'chmod' and that it's done on entire folders. Unsure if it should be changed, but chmod without sudo results in 'operation not permitted' due to how upload- and download- artifact handles permissions.

I imagine it would also be best to delete the artifacts after the workflow run?

Sorry for the large number of 'fix' commits. It's been a while since I've handled GitHub Actions.

[silas-hw]

So you could have a first stage checking whether we have agda in the cache. If not, build it and upload it. Then have testing and upload the agdai files for the lib. Then have in parallel golden testing & html generation. Then deploy the html only if we are in the right branch and everything succeeded.

@gallais It can't seem to find the agdai files. Am I doing something obviously wrong? I presume wildcards with upload-artifact work differently to how I think they do.

HTML is all in one job still, but I'll split out deploying it tomorrow.

[gallais]

I think they should all be in the _build/ directory.

Edit:

Sorry for the large number of 'fix' commits

No worries, we all do that. CI is hell

[silas-hw]

There's some versioning contstraints causing an error:

Error: [Cabal-7107]
Could not resolve dependencies:
[__0] trying: runtests-0.0 (user goal)
[__1] next goal: base (dependency of runtests)
[__1] rejecting: base-4.22.0.0/installed-fde1 (conflict: runtests => base>=4.12 && <4.22)
[__1] skipping: base-4.22.0.0 (has the same characteristics that caused the previous version to fail: excluded by constraint '>=4.12 && <4.22' from 'runtests')
[__1] rejecting: base; 4.21.2.0, 4.21.1.0, 4.21.0.0, 4.20.2.0, 4.20.1.0, 4.20.0.1, 4.20.0.0, 4.19.2.0, 4.19.1.0, 4.19.0.0, 4.18.3.0, 4.18.2.1, 4.18.2.0, 4.18.1.0, 4.18.0.0, 4.17.2.1, 4.17.2.0, 4.17.1.0, 4.17.0.0, 4.16.4.0, 4.16.3.0, 4.16.2.0, 4.16.1.0, 4.16.0.0, 4.15.1.0, 4.15.0.0, 4.14.3.0, 4.14.2.0, 4.14.1.0, 4.14.0.0, 4.13.0.0, 4.12.0.0, 4.11.1.0, 4.11.0.0, 4.10.1.0, 4.10.0.0, 4.9.1.0, 4.9.0.0, 4.8.2.0, 4.8.1.0, 4.8.0.0, 4.7.0.2, 4.7.0.1, 4.7.0.0, 4.6.0.1, 4.6.0.0, 4.5.1.0, 4.5.0.0, 4.4.1.0, 4.4.0.0, 4.3.1.0, 4.3.0.0, 4.2.0.2, 4.2.0.1, 4.2.0.0, 4.1.0.0, 4.0.0.0, 3.0.3.2, 3.0.3.1 (constraint from non-reinstallable package requires installed instance)
[__1] fail (backjumping, conflict set: base, runtests)
After searching the rest of the dependency tree exhaustively, these were the goals I've had most trouble fulfilling: base, runtests

I'm gonna make the potentially naive choice to relax the constraint to <=4.22. Do correct me if that is incorrect.

What's weird is that this hasn't been caught in other CI runs without the refactoring despite having the same GHC and Cabal versions. I imagine it might be to do with cacheing.

[silas-hw]

Golden testing A) puts build files in the tests directory and B) builds differently (transpile to haskell), so the download and upload agdai steps between test-stdlib and test-stdlib-golden weren't actually doing anything beneficial.

[silas-hw]

Each golden test invokes a build, which is what it's spending most of its time doing. Cacheing these should increase speed a lot, but itd be around 500MB, so I currently have it set to only cache on the master branch (e.g. once merged).

E.g. when running golden tests locally, data/lists goes from about 90s to 5s when running a second time.

EDIT:
I think I need to use a more unique cache key so merging does create a new cache. I believe a hit on actions/cache/save will just result in it being ignored. I think using restore-keys would be needed too.

[gallais]

It would be worth investigating why we have so much rechecking in the golden testing because
it does feel like we ought to be able to take advantage of the already computed .agdai files.

If the issue is that we are checking the same files over and over again because every invocation
is with slightly different, and incompatible, OPTIONS then the principled solution may be to
change Agda itself. In order to maximise sharing we may need to have _build have subdirectories
corresponding not only to the Agda versions but also the sets of options.

[silas-hw]

It would be worth investigating why we have so much rechecking in the golden testing because it does feel like we ought to be able to take advantage of the already computed .agdai files.

If the issue is that we are checking the same files over and over again because every invocation is with slightly different, and incompatible, OPTIONS then the principled solution may be to change Agda itself. In order to maximise sharing we may need to have _build have subdirectories corresponding not only to the Agda versions but also the sets of options.

If best, because it seems this may be a larger task, I can revert the caching steps and move it to a separate PR once this has been merged.