Github actions

Stream: general

[Yaël Dillies]

I notice a very significant decrease of the speed at which actions are performed every day around 14h BST (CI takes 4-5h on each of my commits). What's happening?

[Bryan Gin-ge Chen]

Is that when the actions queue is longest? https://github.com/leanprover-community/mathlib/actions?query=is%3Aqueued

[Yaël Dillies]

I did not look at it much but it didn't seem like it :thinking: I will monitor more closely tomorrow.

[Yaël Dillies]

But even so we got faster build servers. So why do we have still comparable build speed? Is it because we only have 5 of them (vs 20 before, I think?)?

[Bryan Gin-ge Chen]

I think that's right.

[Yaël Dillies]

Hmm... that's unfortunate. We get faster builds when nobody is using the machines, but slower once we're all working. I suppose it's hard to redirect actions that would queue for too long on the faster machines to the Github servers?

[Bryan Gin-ge Chen]

Yes, I think that would be hard (though I would be happy to be proved wrong!)

[Bryan Gin-ge Chen]

One idea the maintainers have been bouncing around is the idea of splitting the test and lint jobs off into a new workflow and having one of them run on GitHub servers. This might also be a bit complicated, but it should be possible.

[Yaël Dillies]

Oh yeah, that sounds like a fair split of work. We mostly want the cache anyway.

[Yaël Dillies]

Actions have been timing out recently :fear: It seems like they are taking more than a day to go through.

[Scott Morrison]

We are working on getting more CI resources, but it's not going to be instant. Everyone is working too hard. :-)

[Scott Morrison]

We have a concrete funded plan ready to go, but it needs forms filled out and computers provisioned.

[Yaël Dillies]

Oh that's very nice to hear!