Zulip Chat Archive

Stream: general

Topic: Github build failed with no diagnostics


view this post on Zulip Eric Wieser (Apr 15 2021 at 11:36):

Any idea what happened here?

https://github.com/leanprover-community/mathlib/runs/2350890535?check_suite_focus=true

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 13:06):

This happened to me too, and then a few hours later I got a diagnosis. @Gabriel Ebner do you think this is something to do with the recent "build twice" idea?

view this post on Zulip Gabriel Ebner (Apr 15 2021 at 13:07):

I think this is a github issue. If it was on our end, there would be a build log.

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 13:09):

Here's my version: https://github.com/leanprover-community/mathlib/runs/2346014022 . I take back my assertion that it started working later -- this must have been another commit.


Last updated: May 08 2021 at 10:12 UTC