GitHub actions not running

Stream: general

[Damiano Testa]

It seems that GitHub actions are not running at the moment. Am I not seeing something or can someone else also confirm?

[Bryan Gin-ge Chen]

Hmm, I do see some running here https://github.com/leanprover-community/mathlib4/actions but only 1~2?

I don't see anything about actions at https://www.githubstatus.com/ yet

[Damiano Testa]

Yes, there is very minimal movement and it looks like most Build actions are delayed by over 20 mins.

[Damiano Testa]

Maybe it has been a temporary issue that is already fixed/almost fixed.

[Damiano Testa]

However, this bors batch https://mathlib-bors-ca18eefec4cb.herokuapp.com/batches/11251 does not seem to have started.

[Damiano Testa]

And the previous one, for #23974, I stopped after more than 30mins with no action.

[Bryan Gin-ge Chen]

Hmm, I wonder if we were also out of runners for bors temporarily? Let me tag a few more runners and then put #23974 back on the queue.

[Damiano Testa]

Something is doing something unusual. Here is the run for the current batch: https://github.com/leanprover-community/mathlib4/actions/runs/14907871549/job/41874502243

[Damiano Testa]

It is running, but Build took precedence over Lint, which is usually not the case.

[Damiano Testa]

This causes the status on the batch to not be reported, since Build takes a long time and Lint is not done.

[Damiano Testa]

So, maybe everything is still running ok, or almost ok, but it is hard to find out, since the reports do not get there quickly.

[Bryan Gin-ge Chen]

Aha, I believe that's consistent with there being a lack of runners for bors jobs. I think with the updated labels this should be OK now.

[Damiano Testa]

Ok, great! I am now seeing more movements with the actions, so this is probably resolved itself now.

[Bryan Gin-ge Chen]

To be more explicit, usually the Build and Lint jobs can run in parallel, but since we only had 2 runners that were labeled bors and they both happened to be busy, the bors jobs had to wait for a while. I relabeled all of the runners with bors again so this should be OK for now. (I think the runners were rebooted recently so maybe the labels changed then)

[Damiano Testa]

The build that I restarted got merged and the emoji bot accompanied all along: everything is looking good! :octopus:

[Kim Morrison]

Sorry, additionally three runners have been offline for a few days. I'll try to find time to restart them!

[Kim Morrison]

They're back.