Stream: new members

Topic: permission to push to GitHub

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?

Johan Commelin (Jul 09 2020 at 13:58):

Hey Scott, sure! One second.

Scott Morrison (Jul 09 2020 at 13:58):

Oh --- my username is semorrison

Johan Commelin (Jul 09 2020 at 13:58):

Ok, you should have an invitation email.

Johan Commelin (Jul 09 2020 at 13:58):

Yeah, I figured that out (-;

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

Thank you!

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

Scott Morrison (Aug 06 2020 at 11:05):

@Frederick Eidsnes Thøgersen, done!

Frederick Eidsnes Thøgersen (Aug 06 2020 at 11:06):

Thank you very much :+1:

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

Bryan Gin-ge Chen (Aug 17 2020 at 01:07):

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

Thanks!

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

Bryan Gin-ge Chen (Sep 22 2020 at 19:43):

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

Thank you!

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.

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

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.

Riccardo Brasca (Oct 05 2020 at 15:34):

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

Thank you!

Bryan Gin-ge Chen (Oct 05 2020 at 15:55):

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

Thank you!

Kevin Buzzard (Oct 16 2020 at 19:19):

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

Bryan Gin-ge Chen (Oct 16 2020 at 19:20):

@Kevin Buzzard Access given!

Last updated: May 16 2021 at 05:21 UTC