Zulip Chat Archive

I can't change the visibility of the project unfortunately; only organization owners can. Can you see the contents though? I'm able to see the "two-sided ideals" project even though it's private, for example.

Vincent Beffara (Oct 25 2023 at 13:10):

All I can see is "this is not the webpage you are looking for"

Alex J. Best (Oct 25 2023 at 13:16):

I can see it, I don't think I have that much in the way of priveleges though. I can't make it public, perhaps a maintainer or admin can at https://github.com/orgs/leanprover-community/projects/11/settings

Anne Baanen (Oct 25 2023 at 13:26):

I have made it public.

Vincent Beffara (Oct 25 2023 at 13:34):

Wrong project, this is #11 on two-sided ideals, but from the URL above it should be #13

Alex J. Best (Oct 25 2023 at 13:38):

Oops, sorry for the confusion!

Anne Baanen (Oct 25 2023 at 13:42):

Now both are public :) Should I make #11 private again? @Jireh Loreaux

Vincent Beffara (Oct 25 2023 at 13:44):

Thanks!

Jireh Loreaux (Oct 25 2023 at 13:44):

If that's in reference to the two-sided ideal project, it's fine for it to be public. I never intended it to be private.

Yaël Dillies (Oct 25 2023 at 13:47):

Yeah it's really weird that we (= non-maintainers) can't create public projects anymore.

Anne Baanen (Oct 25 2023 at 13:51):

I'm going to see if there's a way to allow that again. I'd even say projects should be public by default...

Anatole Dedecker (Oct 25 2023 at 13:53):

I'm trying to change that right now

Anne Baanen (Oct 25 2023 at 13:53):

Setting "Allow members to change project visibilities for this organization" is now enabled! But I can't find where to set a default visibility

Anatole Dedecker (Oct 25 2023 at 13:54):

Ah I think we both changed the setting at the same time x) But indeed it says "projects will still be private by default".

Dagur Asgeirsson (Oct 26 2023 at 13:07):

I'm trying to create a "Github project" in mathlib, but it seems like I need to be a "member" of the leanprover-community organisation. Is that correct?

This discussion should probably also move to a new topic but I don't have permission to move messages.

Notification Bot (Oct 26 2023 at 13:14):

15 messages were moved here from #maths > Path lifting by Johan Commelin.

Adam Topaz (Oct 26 2023 at 14:13):

@Dagur Asgeirsson What project would you like to create? I can help with that (or any other maintainer can as well). I don't think there is any official policy regarding the creation of github projects.

Dagur Asgeirsson (Oct 26 2023 at 14:14):

"Towards solid abelian groups"

Yaël Dillies (Oct 26 2023 at 14:15):

In fact, you should be able to create the project. Does it tell you do not have the permission?

Dagur Asgeirsson (Oct 26 2023 at 14:17):

When I go to the projects tab in mathlib4, it only offers me to "link a project". That takes me to the leanprover-community organisation, where I don't see any way to create a project. But I'm sure I'm just missing something

Adam Topaz (Oct 26 2023 at 14:17):

https://github.com/orgs/leanprover-community/projects/15

Adam Topaz (Oct 26 2023 at 14:21):

I don't know whether all "collaborators" have write access to this project by default. Let me (or another maintainer) know if you have any issues adding items to this project.

Dagur Asgeirsson (Oct 26 2023 at 14:22):

Yeah I think you need to give me write access to the project, I can't do anything with it

Adam Topaz (Oct 26 2023 at 14:24):

you should now have an invite in your inbox

Yaël Dillies (Oct 26 2023 at 14:27):

Project 1, 5, 6, 10 are still private. I assume this is an oversight?

Floris van Doorn (Oct 26 2023 at 14:33):

I assume so too. I made them public.

Last updated: Dec 20 2023 at 11:08 UTC

leanprover-community / mathlib