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, golden testing, and standard unit tests run in parallel.

Furthermore, caching is added to the build files of the golden tests. Some rather non-scientific benchmarking showed running golden tests a second time shortened each test by often over a minute, backed up by Test.Golden calling a shell script that itself invokes cabal build for each test. Caching all of dist-newstyle consumes about 120MB, so should be done sparingly; currently, it will only be cached on the master branch and if dist-newstyle changes after running the golden tests (by checking the hashFiles of dist-newstyle before and after running the tests).

Workflow runs now take between 10 and 15 minutes, a significant improvement from the previous 30 to 50 minutes.

Most improvements now likely lie in optimising the tests themselves, but some micro optimisations could potentially be seen by parallelising golden tests using the matrix strategy (whilst complicating caching).

[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]

I'm currently not crazy confident on how caching on test-stdlib-golden is done (i.e. sha1sum and how the key is named)

[gallais]

This is already a win IMO even if you cannot figure out how to speed up
the golden testing. If that step is really not being sped up by running after
the library build then we should consider running it in parallel with test-stdlib
(and not bother with caching for now).

We could even run every golden-testing group separately (passing only=XXX
to make testsuite will only run the test cases whose name contain XXX as a
substring so for instance make testsuite only=data/ only runs the ones in the
data/ subdirectory!)

[silas-hw]

My instincts are telling me running golden tests in parallel will be faster than the speedup from reusingg agdai files, so I'm testing that out now.

It's almost certainly a good idea to shard/split the golden tests as well. Given they're pretty well structured into directories it shouldn't be too hard to split the groups evenly between a set number of runners instead of having them hard-coded (some bash wizardry should work). I might do that in a separate PR as to not bloat out this one too much (although I'm well aware it has already gotten quite big).

[silas-hw]

Well that shaved off ~10 minutes from the average CI run for this PR!

After forcing a cache save by editing the workflow and then reverting it to make sure it does in fact work I'm going to leave this and make new changes in fresh PRs.

[silas-hw]

Wow! That's a whole lot faster (14 minutes), and I believe it was only using 1-2 runners across it (test-stdlib and test-stdlib-golden started a few minutes after html-generate).

Golden testing itself only took 5 minutes!

The only thing I'm still not sure of is if the if for saving a new cache will work properly.

[silas-hw]

For some reason the hashes of dist-newstyle are always different. Probably something to do with hidden files.

[silas-hw]

I don't know enough about the files generated by cabal to know what's changing on each run and hence why the hash also changes.

A diff on two local runs only shows cache/config changing, but restricting to build/ doesn't fix the problem (it was a blind attempt anyway).

Even if this can't be fixed, only saving on master should at least be enough to prevent too much storage being used.

[JacquesCarette]

So is this now ready for a re-review?

[JacquesCarette]

As usual, my review of CI-related work should not count as a 'full' review. But nothing jumps out at me as being odd.