Zulip Chat Archive

Stream: general

Topic: Hoskinson runners


Yaël Dillies (Aug 18 2022 at 09:18):

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

Junyan Xu (Aug 18 2022 at 09:23):

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

Yaël Dillies (Aug 18 2022 at 09:26):

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

Junyan Xu (Aug 18 2022 at 13:48):

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.


Last updated: Aug 03 2023 at 10:10 UTC