Zulip Chat Archive

Stream: general

Topic: PRing to mathlib from forks


view this post on Zulip Kevin Buzzard (Mar 28 2020 at 14:28):

Am I right in thinking that PR's from non-master branches of mathlib are for some CI reason preferred to PR's from forks? If so, and if this isn't going to change any time soon, what is the preferred way to get someone like https://github.com/shingtaklam1324 added to the list of people who are allowed to write to non-master branches of mathlib? Usually I just ask Rob but I am reluctant to pester him every time and it's only him and Simon who I know for sure can do it. Who can do it?

view this post on Zulip Bryan Gin-ge Chen (Mar 28 2020 at 14:30):

I've just sent him an invite. The list of people who should be able to do it is at the bottom of the mathlib README.

view this post on Zulip Bryan Gin-ge Chen (Mar 28 2020 at 14:45):

By the way, for future requests, I just set up a "Zulip user group" so that you can ping all of the mathlib maintainers like this: @maintainers .

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 10:33):

@maintainers could GitHub user ashwiniyengar (a number theory PhD student in London) have push access to non-master branches of mathlib? Thanks.

view this post on Zulip Chris Hughes (Apr 23 2020 at 11:12):

Done

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 11:16):

@Ashwin Iyengar

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 11:24):

Thanks.

view this post on Zulip Jannis Limperg (Apr 27 2020 at 22:19):

@maintainers could I get push access to non-master branches of Lean (Github: JLimperg)? I'm preparing a PR to make case tags suck less.

view this post on Zulip Chris Hughes (Apr 27 2020 at 22:22):

It's telling me you already do have write access.

view this post on Zulip Chris Hughes (Apr 27 2020 at 22:22):

Maybe someone got there before me.

view this post on Zulip Jannis Limperg (Apr 27 2020 at 22:28):

That's weird, I'm still getting ERROR: Permission to leanprover-community/lean.git denied to JLimperg. Am I using Git wrong? Could it be that you checked mathlib rather than lean?

view this post on Zulip Chris Hughes (Apr 27 2020 at 22:49):

Yeah, I checked mathlib. Oops. You've been added to Lean

view this post on Zulip Jannis Limperg (Apr 27 2020 at 23:10):

That worked, thanks!

view this post on Zulip Kevin Buzzard (Aug 02 2020 at 18:07):

@maintainers could @Ashvni Narayanan github username laughinggas have push access to non-master branches of mathlib? Her and I are working on bundling subrings. Thanks!

view this post on Zulip Gabriel Ebner (Aug 02 2020 at 18:09):

invite sent

view this post on Zulip Ashvni Narayanan (Aug 02 2020 at 20:01):

Thank you!


Last updated: May 13 2021 at 22:15 UTC