Stream: general

Topic: bors

Kevin Buzzard (Apr 12 2020 at 08:46):

Am I the only one who finds this a bit creepy:

Reid Barton (Apr 12 2020 at 13:00):

No.

Reid Barton (Apr 12 2020 at 13:01):

I was going to comment on it earlier, but as far as I can tell it's the picture for the bors github user and so we couldn't change it.

Gabriel Ebner (Apr 12 2020 at 13:03):

What is the creepy part? The unnecessarily large heading? The name of the bot? The logo?

Reid Barton (Apr 12 2020 at 13:04):

For me mainly the logo, I don't know what bors is.

Reid Barton (Apr 12 2020 at 13:05):

Other than this bot, I mean

Gabriel Ebner (Apr 12 2020 at 13:08):

I always thought it's a Russian name, but I guess I mixed it up with Boris. This is the official explanation for the name:

It’s a reference to a 1953 sci-fi novel 17 about the robot, Bors, that ran the world’s last surviving government.

Reid Barton (Apr 12 2020 at 13:11):

Now that you mentioned it, the font is unnecessarily large as well

Gabriel Ebner (Apr 12 2020 at 14:06):

The bors-ng project is reasonably active. You could submit a PR to change the font size.

Gabriel Ebner (Apr 12 2020 at 14:08):

If anybody wants to test changes on a live bors instance, I've set up a personal bors here: https://borslein.herokuapp.com/ This is deployed from by bors-ng fork, feel free to submit a PR if you want to test something: https://github.com/gebner/bors-ng
borslein.png

Kevin Buzzard (Apr 12 2020 at 14:08):

An alternative approach is for us all to start using that size font, so it's less obvious that bors is being so loud.

Bryan Gin-ge Chen (Apr 12 2020 at 15:07):

Sadly, Zulip doesn't increase the font size, it just bolds and underlines.

Gabriel Ebner (Apr 12 2020 at 18:45):

PR fired: https://github.com/bors-ng/bors-ng/pull/930 Here's an example of the proposed comment style: https://github.com/gebner/mathlib/pull/3#issuecomment-612657757

Sebastian Ullrich (Apr 12 2020 at 20:27):

Bryan Gin-ge Chen said:

Sadly, Zulip doesn't increase the font size, it just bolds and underlines.

$\Large\text{\textbf{You can shout in maths though}}$

Bryan Gin-ge Chen (Apr 14 2020 at 01:13):

@Gabriel Ebner's PR to bors was merged: bors is much calmer now.

Reid Barton (Apr 14 2020 at 01:18):

thanks @Gabriel Ebner !

Patrick Massot (Apr 14 2020 at 07:54):

Thanks! We still get the creepy eye. Can we choose that?

Kevin Buzzard (Apr 14 2020 at 07:58):

The octopus was much funnier :-)

Gabriel Ebner (Apr 14 2020 at 08:34):

The octopus is the bors instance I've set up myself (to test my bors PRs). It is possible to switch mathlib over to it if we want, we'd just need to remove the bors app and add the borslein app.

Patrick Massot (Apr 14 2020 at 08:42):

Would it be slower? Does it use your own machine?

Gabriel Ebner (Apr 14 2020 at 08:49):

No, it's hosted on the free tier of heroku (a cloud hosting service). Sometimes it takes a few seconds to load the https://borslein.herokuapp.com page, but I don't think this causes any problems for bors r+ comments and such.

Patrick Massot (Apr 14 2020 at 08:50):

Then the only downside is it would display the octopus for every bors message, not only good news, right?

Johan Commelin (Apr 14 2020 at 08:51):

Maybe it can randomly show either the octopus or an upside down octopus to compensate for that?

Gabriel Ebner (Apr 14 2020 at 08:52):

Errm, yes. The picture you see next to the bors comments is the logo of the bot. Every bot can only have one logo. You can choose between a friendly octopus or a government robot eye.

Patrick Massot (Apr 14 2020 at 08:52):

Then we need a more neutral logo.

Patrick Massot (Apr 14 2020 at 08:53):

Does it have to be an emoji or can it be any picture?

Mario Carneiro (Apr 14 2020 at 08:53):

what's wrong with the government robot eye?

Patrick Massot (Apr 14 2020 at 08:54):

It's creepy.

Mario Carneiro (Apr 14 2020 at 08:54):

it's your friendly neighborhood bors

Johan Commelin (Apr 14 2020 at 08:55):

https://en.wikipedia.org/wiki/Bors

Gabriel Ebner (Apr 14 2020 at 08:56):

https://en.wikipedia.org/wiki/The_Last_of_the_Masters

Johan Commelin (Apr 14 2020 at 08:57):

Johan Commelin (Apr 14 2020 at 08:59):

Gabriel Ebner said:

https://en.wikipedia.org/wiki/The_Last_of_the_Masters

But that is their Bors.... maybe you can use the other Bors as inspiration?

Johan Commelin (Apr 14 2020 at 09:00):

How about :guard: ? It's less creepy, but it's still the one who decides whether you'll get to the master or not...

Kevin Buzzard (Apr 14 2020 at 09:39):

I really don't actually care about the creepy eye that much. I do think it's good that it's stopped shouting, because its messages were easy enough to spot because of the creepy eye, but I hope that some passing silly comment by me is not actually the sole reason that people are pouring their time into turning the creepy eye into some other random pic.

Scott Morrison (Apr 21 2021 at 01:35):

I am confused about bors. Currently #7186 shows a red X, but when I look at the CI output at the bottom of the PR, the only indicated problem is a line that says "bors, merge conflict", with a red X to the left. Clicking on the red X takes me to https://app.bors.tech/repositories/24316/log#batch-138379, where #7186 appears in two different lines:

21/04/2021, 07:39:08    Batch 138379    Failed  #7289 #7266 #7251 #7211 #7186 #7131 #7100 #7024
21/04/2021, 07:39:04    Batch 138401    Waiting to run  #7186 #7131 #7024

What does this mean? In particular, am I meant to do anything? My instinct is that if there's a red X is it my fault, so usually at this point I would just merge master again, possibly type bors merge again, and see what happens. But I suspect this is something that will resolve itself, and it is actually a bad indicator from bors to put a red X at this point...

Bryan Gin-ge Chen (Apr 21 2021 at 01:41):

My understanding is that the red X + "merge conflict" just means that the most recent batch had a merge conflict of some kind (either with master or between the PRs). You can just let bors test out the batches as usual unless you feel like investigate more closely.

Scott Morrison (Apr 21 2021 at 01:43):

I feel like this would be much more useful as an orange dot than a red X. :-(

Scott Morrison (Apr 21 2021 at 01:43):

To me red X says it's my fault and needs fixing. If it just needs more time it definitely shouldn't be a red X.

Bryan Gin-ge Chen (Apr 21 2021 at 01:44):

You can raise an issue at the bors repo, though I suspect it won't be high on the maintainer's priority list.

Scott Morrison (Apr 21 2021 at 01:49):

Okay, I tried to explain at https://github.com/bors-ng/bors-ng/issues/1227, we'll see how badly I get flamed. :-)

Bryan Gin-ge Chen (Apr 21 2021 at 02:00):

Haha, I don't think you'll be flamed; in my experience the maintainer's been great about jumping on crashes etc, but there are a bunch of little tweak / feature requests in the issues (some from me!) that haven't gotten much attention.

Julian Berman (Apr 21 2021 at 02:01):

I don't think they can make that orange dot if I follow, the red ex is just a GitHub status check, no? There's only 3 statuses, successful, failed (this) or pending (shows nothing)

Bryan Gin-ge Chen (Apr 21 2021 at 02:03):

I think pending is a orange (yellow to my eyes) dot. Nothing means no checks have run, right?

Julian Berman (Apr 21 2021 at 02:03):

huh, interesting, is there a dot there and I never noticed...

Julian Berman (Apr 21 2021 at 02:05):

yeah seems you're both right, guess I never noticed.

Scott Morrison (Apr 21 2021 at 02:16):

(Sorry, shouldn't have suggested I might get flamed. Just intended to say I didn't feel qualified making a suggestion there.)

Oliver Nash (Apr 22 2021 at 17:22):

I think bors might be ignoring some "ready to merge" PRs that failed as part of an earlier batch. I have in mind #7181 and #7266 which have each been "ready to merge" for about two days but looking at this list I think I see others.

Oliver Nash (Apr 22 2021 at 17:23):

I am well aware that certain people are currently working heroically to address our CI time issues (esp. with Leanchecker) but I wonder is there a way remind bors that these apparently forgotten PRs exist?

Bryan Gin-ge Chen (Apr 22 2021 at 17:31):

There isn't any automated way at the moment, thanks for pointing these out; I've put them on the queue.

Yaël Dillies (Sep 30 2021 at 05:39):

bors merged #9444 but didn't delete the branch. Is it an accident or some expected change in behavior?

Yaël Dillies (Sep 30 2021 at 17:05):

#9412 might have been yeeted off the queue. Can a maintainer check?

Bryan Gin-ge Chen (Sep 30 2021 at 17:06):

Looks to me like it's still in the queue right now: https://app.bors.tech/repositories/24316

Yaël Dillies (Sep 30 2021 at 17:12):

Oh this page is very interesting? Is there a Zulip shortcut to itsimilar to #queue? Maybe #bors?

Johan Commelin (Sep 30 2021 at 17:19):

@Bryan Gin-ge Chen :this: sounds like a nice idea.

Bryan Gin-ge Chen (Sep 30 2021 at 17:37):

:point_right: #bors

Yaël Dillies (Sep 30 2021 at 17:41):

Love it! Thanks! :heart_kiss:

Yaël Dillies (Sep 30 2021 at 17:41):

That's what I call being responsive.

Yaël Dillies (Mar 25 2022 at 11:25):

#12045 has not been picked up by #bors.

Yaël Dillies (Mar 25 2022 at 11:36):

Doesn't seem to have worked :thinking:

Anne Baanen (Mar 25 2022 at 11:39):

Now it's going!

Yaël Dillies (Mar 25 2022 at 11:40):

Poor machine :sweat_smile:

Anne Baanen (Mar 25 2022 at 11:42):

bors does not feel, bors does not care, bors exists solely to prevent you from merging :eye:

Moritz Doll (Mar 25 2022 at 12:30):

maybe you should thank bors more often for doing a good job :rolling_on_the_floor_laughing:

Yaël Dillies (Apr 07 2022 at 10:18):

#13133 was yeeted off the queue

Riccardo Brasca (Apr 07 2022 at 10:35):

I've delegated it.

Yaël Dillies (Apr 10 2022 at 08:40):

Welp, bors merged it twice :sweat_smile:

Last updated: Dec 20 2023 at 11:08 UTC