Zulip Chat Archive

Stream: new members

Topic: build failure


view this post on Zulip Mark Gerads (Mar 01 2021 at 20:17):

It says

Changes approved

and Mathlib is being rebuilt again. Does this mean I don't need to do anything?

view this post on Zulip Eric Wieser (Mar 01 2021 at 20:18):

If bors says it's retrying, then you don't need to do anything

view this post on Zulip Eric Wieser (Mar 01 2021 at 20:19):

Although it's good practice to look at the logs to guess whether it's your fault

view this post on Zulip Bryan Gin-ge Chen (Mar 01 2021 at 20:19):

You pushed a new commit just now, so your PR was taken out of the queue. I've "delegated" the PR to you with bors d+, so you can put it back on the queue whenever you want.

view this post on Zulip Mark Gerads (Mar 01 2021 at 20:21):

I'll see what that means I need to do after it shows Mathlib as successfully built.

view this post on Zulip Bryan Gin-ge Chen (Mar 01 2021 at 20:23):

(All you need to do is put bors r+ on its own line in a GitHub comment.)

view this post on Zulip Eric Wieser (Mar 01 2021 at 20:25):

Note that bors failing doesn't even mean a conflict has appeared in master - it just means that when you combine the pile of PRs into a single build on top of master, they either conflict with each other or with master

view this post on Zulip Mark Gerads (Mar 01 2021 at 20:30):

Is it okay for me to merge it now then? I figure I should wait; 'tis more proper. I am excited to see this contribution in Mathlib.

view this post on Zulip Bryan Gin-ge Chen (Mar 01 2021 at 20:35):

Sure, I think it's safe enough! It'll join the other PRs in queue: https://app.bors.tech/repositories/24316


Last updated: May 11 2021 at 12:15 UTC