PRing to mathlib from forks

Stream: general

[Kevin Buzzard]

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?

[Bryan Gin-ge Chen]

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.

[Bryan Gin-ge Chen]

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 .

[Kevin Buzzard]

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

[Chris Hughes]

Done

[Kevin Buzzard]

@Ashwin Iyengar

[Kevin Buzzard]

Thanks.

[Jannis Limperg]

@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.

[Chris Hughes]

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

[Chris Hughes]

Maybe someone got there before me.

[Jannis Limperg]

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?

[Chris Hughes]

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

[Jannis Limperg]

That worked, thanks!

[Kevin Buzzard]

@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!

[Gabriel Ebner]

invite sent

[Ashvni Narayanan]

Thank you!