Zulip Chat Archive

Stream: new members

Topic: permission to push to GitHub


view this post on Zulip Scott Morrison (Jul 09 2020 at 13:57):

Hi, I'm pretending to be a new user who wants to make a pull request to mathlib. Could someone please give me permission to push a branch?

view this post on Zulip Johan Commelin (Jul 09 2020 at 13:58):

Hey Scott, sure! One second.

view this post on Zulip Scott Morrison (Jul 09 2020 at 13:58):

Oh --- my username is semorrison

view this post on Zulip Johan Commelin (Jul 09 2020 at 13:58):

Ok, you should have an invitation email.

view this post on Zulip Johan Commelin (Jul 09 2020 at 13:58):

Yeah, I figured that out (-;

view this post on Zulip Apurva Nakade (Jul 16 2020 at 23:48):

Hi, I'm working on some linear algebra theorems to mathlib (hoping to get to Spectral theorem) and need to make a pull-request to add documentation to linear_algebra/direct_sum_module and close #3418. Could I get permission to push a branch? My Github username is apurvnakade

view this post on Zulip Bryan Gin-ge Chen (Jul 16 2020 at 23:51):

@Apurva Nakade https://github.com/leanprover-community/mathlib/invitations

view this post on Zulip Apurva Nakade (Jul 16 2020 at 23:51):

Thank you!

view this post on Zulip Frederick Eidsnes Thøgersen (Aug 06 2020 at 11:02):

Hi, I am a "semi-new" user currently following Scott Morrison's tutorial. I have a project with Professor Buzzard with regards to local fields. The last two months, I have just been practicing Lean, but I now plan to start making some pull requests to mathlib. Would it be possible to request that someone may give me permission to push a branch? I believe my git username is: FrederickThogersen

view this post on Zulip Scott Morrison (Aug 06 2020 at 11:05):

@Frederick Eidsnes Thøgersen, done!

view this post on Zulip Frederick Eidsnes Thøgersen (Aug 06 2020 at 11:06):

Thank you very much :+1:

view this post on Zulip Kenji Nakagawa (Aug 17 2020 at 01:06):

Hi, I'm working on some ring theory things, such as a third Noetherian definition, and adding a few facts about integral domains (and hopefully eventually dedekind domain things). Can I get permission to push a branch? My github username is mushokunosora

view this post on Zulip Bryan Gin-ge Chen (Aug 17 2020 at 01:07):

@Kenji Nakagawa Invite sent! https://github.com/leanprover-community/mathlib/invitations

view this post on Zulip Kenji Nakagawa (Aug 17 2020 at 01:07):

Thanks!

view this post on Zulip Jia Ming (Sep 22 2020 at 19:39):

Hello! I'm snooping around order.lattice and thought I could make some small improvements, may I have permission to push a branch to mathlib? My username is jiaminglimjm

view this post on Zulip Bryan Gin-ge Chen (Sep 22 2020 at 19:43):

@Jia Ming invite sent! https://github.com/leanprover-community/mathlib/invitations

view this post on Zulip Jia Ming (Sep 22 2020 at 19:43):

Thank you!

view this post on Zulip Patrick Massot (Sep 22 2020 at 19:44):

You should discuss a bit your improvement ideas here before spending too much time coding, just to make sure you won't waste time.

view this post on Zulip Jia Ming (Sep 22 2020 at 19:58):

Ah right, noted, i was just too excited hahah. It's a really small change, so i hope i dont waste anyone else's time too much

view this post on Zulip Patrick Massot (Sep 22 2020 at 19:58):

Oh I meant your time.

view this post on Zulip Patrick Massot (Sep 22 2020 at 19:59):

I don't want you to invest too much time only to find out that what you had in mind is already in mathlib somewhere or undesirable for some reason.

view this post on Zulip Riccardo Brasca (Oct 05 2020 at 15:34):

Hi all, can I have permission to push to github? My username is riccardobrasca

Thank you!

view this post on Zulip Bryan Gin-ge Chen (Oct 05 2020 at 15:55):

@Riccardo Brasca Invite sent! https://github.com/leanprover-community/mathlib/invitations

view this post on Zulip Riccardo Brasca (Oct 05 2020 at 15:56):

Thank you!

view this post on Zulip Kevin Buzzard (Oct 16 2020 at 19:19):

Hi. Can Imperial undergrad Xiang Li, github userid Lix0120, have push access to non-master branches?

view this post on Zulip Bryan Gin-ge Chen (Oct 16 2020 at 19:20):

@Kevin Buzzard Access given!


Last updated: May 16 2021 at 05:21 UTC