mathlib-bors acting on my behalf

Stream: mathlib4

[Geoffrey Irving]

I was curious where I was in the merge queue for https://github.com/leanprover-community/mathlib4/pull/9547 (for no particular reason), but clicking on the "Details" link next to "Waiting in queue" produced

Screenshot-2024-01-08-at-11.40.38AM.png

Is it possible to restrict this request to certain repositories? I'm not comfortable letting mathlib-bors act on my behalf for arbitrary repositories, but I am for anything lean and mathlib related. Alternatively, do I need mathlib-bors to act on my behalf to see the merge queue?

[Eric Wieser]

From the github docs:

The GitHub App can only do things that both you and the app have permission to do

[Eric Wieser]

So this is a slightly strange thing for bors to request (since it doesn't seem to have any permissions that would be attributed as actions anyway), but I think it's ultimately harmless

[Kim Morrison]

Also --- bors is not long for this world, so waiting a week may make this irrelevant. :-)

[Jeremy Tan]

Scott Morrison said:

Also --- bors is not long for this world, so waiting a week may make this irrelevant. :-)

Are we finally removing bors in favour of GitHub's built-in merge queue?

[Ruben Van de Velde]

Not likely

[Mauricio Collares]

No, GitHub's merge queue is worse than bors. Probably Mergify.

[Kim Morrison]

(Note that "worse than bors" is irrelevant at this point: we don't have a maintained bors installation available. The interim one is unlikely to keep going.)