slow linting step CI?

Stream: mathlib4

[David Loeffler]

For my recent PR #32646, the bors staging CI run took a really remarkably long time to finish, getting hung up on the "lint style" step. Since the PR adds a new linter, I was worried I'd done something wrong, but it looks like the slowness is something else: here's the relevant part of the CI log:

Get:29 http://azure.archive.ubuntu.com/ubuntu noble/universe amd64 lmodern all 2.005-1 [9542 kB]
Get:30 http://azure.archive.ubuntu.com/ubuntu noble/universe amd64 mupdf-tools amd64 1.23.10+ds1-1build3 [49.3 MB]
Get:31 http://azure.archive.ubuntu.com/ubuntu noble/main amd64 t1utils amd64 1.41-4build3 [61.3 kB]
Get:32 http://azure.archive.ubuntu.com/ubuntu noble/universe amd64 texlive-binaries amd64 2023.20230311.66589-9build3 [8529 kB]
Get:33 http://azure.archive.ubuntu.com/ubuntu noble/universe amd64 texlive-base all 2023.20240207-1 [21.7 MB]
Preconfiguring packages ...
Fetched 118 MB in 46min 34s (42.1 kB/s)

This is some Ubuntu auto-update step, downloading new texlive packages, which presumably shouldn't be happening afresh on every CI run! I hope this was just a one-off glitch, but I'm reporting it here in case some action is needed.

[Bryan Gin-ge Chen]

Very strange. My best guess is some kind of network hiccup. It doesn't look like something we have control over, unfortunately.

[Michael Rothgang]

Another instance: https://github.com/leanprover-community/mathlib4/actions/runs/20100617503/job/57670221999?pr=32690

[Snir Broshi]

I have one that beats both of these combined:
https://github.com/leanprover-community/mathlib4/actions/runs/20384108818/job/58581312606?pr=33111
4 hours and counting

[Snir Broshi]

Now it says "cancelled after 6h 5m"

[Snir Broshi]

Oh there's a time limit
image.png