Zulip Chat Archive

Stream: general

Topic: continuous integration failing

Kevin Buzzard (Apr 30 2020 at 12:45):

The mathlib github page is currently proudly displaying this:

failing.png

Is that supposed to happen?

Gabriel Ebner (Apr 30 2020 at 12:50):

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

Kevin Buzzard (Aug 02 2020 at 10:41):

CI is failing on master:

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

Rob Lewis (Aug 02 2020 at 10:44):

I think this must be a glitch.

Kenny Lau (Aug 02 2020 at 11:05):

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

Kenny Lau (Aug 02 2020 at 11:06):

it builds now

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: Dec 20 2023 at 11:08 UTC