Zulip Chat Archive

I'm trying to port a file and follow the instructions in
https://github.com/leanprover-community/mathlib4/wiki/Porting-wiki
When making a pull request on the mathlib4 repository, I tried making a branch directly on that repo, but don't have access rights:

ERROR: Permission to leanprover-community/mathlib4.git denied to mo271.
fatal: Could not read from remote repository.

Please make sure you have the correct access rights
and the repository exists.

Could someone grant me access rights, or should I just make a pull request from a fork?

Johan Commelin (Dec 29 2022 at 09:19):

@Moritz Firsching https://github.com/leanprover-community/mathlib4/invitations

Moritz Firsching (Dec 29 2022 at 09:20):

Thanks @Johan Commelin!

zbatt (Dec 29 2022 at 15:43):

Hi! I was told by @Ruben Van de Velde to ask for push access to the main repository for future PRs. Is this where to do that? My github is xoers. Thanks!

Ruben Van de Velde (Dec 29 2022 at 15:51):

Yep! @maintainers

zbatt (Dec 29 2022 at 15:51):

Thanks!

Johan Commelin (Dec 29 2022 at 15:57):

@zbatt https://github.com/leanprover-community/mathlib4/invitations

zbatt (Dec 29 2022 at 15:57):

thanks!

Maxwell Thum (Jan 03 2023 at 22:48):

Hi @maintainers, could I also get push access? My github is maxwell-thum.

Riccardo Brasca (Jan 03 2023 at 22:56):

Invite sent!

Maxwell Thum (Jan 03 2023 at 22:59):

Thank you very much!

Calvin Lee (Jan 07 2023 at 06:09):

Hello @maintainers! I'd like to join the mathport effort. My github is 4e554c4c. Could I have an invite to mathlib4?

Praneeth Kolichala (Feb 16 2023 at 21:02):

I ported NFA.lean. Could I have push access? (username: prakol16) @maintainers

Praneeth Kolichala (Feb 17 2023 at 04:21):

Ok well it seems NFA has a pull request opened (https://github.com/leanprover-community/mathlib4/pull/2334). Maybe I should have just started a new thread? Pinging @maintainers once again

Scott Morrison (Feb 17 2023 at 04:22):

@Praneeth Kolichala, invite sent.

Yury G. Kudryashov (Feb 17 2023 at 04:22):

@Jason Yuen, @Praneeth Kolichala already ported NFA.lean

Praneeth Kolichala (Feb 17 2023 at 04:41):

It's alright, it was good experience anyway. I'll avoid pushing since it seems that @Jason Yuen has already gotten most of it I assume, unless they want me to.

Jason Yuen (Feb 17 2023 at 05:01):

I closed my pr

Amelia Livingston (Mar 25 2023 at 23:22):

hi @maintainers, please could I have push access? My username is 101damnations. Thanks!

Eric Wieser (Mar 25 2023 at 23:25):