Zulip Chat Archive

Stream: mathlib4

Topic: repo access

David Loeffler (Feb 13 2023 at 19:27):

One of my mathlib3 PR's has ended up modifying a ported file. I'd like to request push access to the mathlib4 repo, so I can create a matching mathlib4 PR.

Johan Commelin (Feb 13 2023 at 19:34):

@David Loeffler voila: https://github.com/leanprover-community/mathlib4/invitations

David Loeffler (Feb 13 2023 at 19:35):

Thanks!

David Loeffler (Feb 19 2023 at 01:54):

OK, the mathlib4 forward-port PR is ready for review (with updated mathlib3 Git sha) at !4#2263.

I see there's a spreadsheet for keeping track of forward-ports, but that still has this PR listed as "awaiting mathlib3 review". Is there something I need to do in order to update this?

Yaël Dillies (Feb 19 2023 at 09:36):

You can change it yourself by clicking on the card in the Github UI.

David Loeffler (Feb 19 2023 at 15:38):

You can change it yourself by clicking on the card in the Github UI.

I can see the spreadsheet, but not change its contents.

Yaël Dillies (Feb 19 2023 at 16:12):

even from the PR itself?

Eric Wieser (Feb 19 2023 at 17:25):

Yeah, it looks like only maintainers can edit it. This was just an experiment by me

Yaël Dillies (Feb 19 2023 at 18:03):

I'm not a maintainer but I can edit it. Probably because I'm a reviewer?

Eric Wieser (Feb 19 2023 at 18:51):

Yeah, I just granted mathlib-reviewers access

Last updated: Dec 20 2023 at 11:08 UTC