Hoskinson runners

Stream: general

[Yaël Dillies]

Did we switch to the Hoskinson runners? :open_mouth:
https://github.com/leanprover-community/mathlib/actions/runs/2881041418 mentions hoskinson4.

[Junyan Xu]

did you notice it reported an error at Build mathlib: src/analysis/convex/slope.lean#L103

[Yaël Dillies]

Actually, I hadn't. Thanks! Why isn't it showing up as usual?

[Junyan Xu]

It's at the bottom of the page https://github.com/leanprover-community/mathlib/actions/runs/2881041418/attempts/1 below two other error messages, one of which is the usual "lost connection", and the other an obscure long message I never seen ... I saw you triggered a rerun so I guessed you didn't notice.