Zulip Chat Archive

Stream: general

Topic: continuous integration failing


view this post on Zulip Kevin Buzzard (Apr 30 2020 at 12:45):

The mathlib github page is currently proudly displaying this:

failing.png

Is that supposed to happen?

view this post on Zulip Gabriel Ebner (Apr 30 2020 at 12:50):

We know about it. It is not serious. It will be fixed.

view this post on Zulip Kevin Buzzard (Aug 02 2020 at 10:41):

CI is failing on master:

https://github.com/leanprover-community/mathlib/runs/937258397

view this post on Zulip Rob Lewis (Aug 02 2020 at 10:44):

I think this must be a glitch.

view this post on Zulip Kenny Lau (Aug 02 2020 at 11:05):

I clicked the re-run button (wait, I can do that??)

view this post on Zulip Kenny Lau (Aug 02 2020 at 11:06):

it builds now

view this post on Zulip Rob Lewis (Aug 02 2020 at 11:09):

Note that CI on master is almost completely unnecessary. It only matters if someone pushes directly to master. There are no CI steps anymore that are master-specific and the same commit has to build in bors' staging branch in order to be merged.


Last updated: May 17 2021 at 22:15 UTC