Stream: Coq devs & plugin devs

Topic: Enough privileges to tweak issues/PR tags


view this post on Zulip Rodolphe Lepigre (Dec 14 2023 at 12:28):

What is the policy on giving contributors more privileges on the Coq repo? I am sometimes annoyed that I cannot add/remove tags to (mostly my own) issues an PRs.

view this post on Zulip Gaëtan Gilbert (Dec 14 2023 at 12:30):

if you ask you're likely to get it

view this post on Zulip Karl Palmskog (Dec 14 2023 at 12:32):

probably there should be a gamification of Coq dev like in StackOverflow, with badges and the like for "first issue", "first PR", "first commit merged", etc., leading to more privileges over time

view this post on Zulip Gaëtan Gilbert (Dec 14 2023 at 12:32):

doubt

view this post on Zulip Karl Palmskog (Dec 14 2023 at 12:33):

surprisingly, people actually get motivated by that stuff

view this post on Zulip Karl Palmskog (Dec 14 2023 at 12:33):

I think there is anyway an informal gamification going on

view this post on Zulip Gaëtan Gilbert (Dec 14 2023 at 12:34):

anyway github's permission model doesn't have many steps for "more privileges over time"
there's

view this post on Zulip Karl Palmskog (Dec 14 2023 at 12:36):

you can get added to various teams, right? And I think there are privileges associated with teams for specific code

view this post on Zulip Pierre Roux (Dec 14 2023 at 12:37):

It's more like the "spam" you get when someone open a PR.

view this post on Zulip Gaëtan Gilbert (Dec 14 2023 at 12:42):

the teams subscribe you to review requests for that team and give you "merge stuff" rights
that's all

view this post on Zulip Gaëtan Gilbert (Dec 14 2023 at 12:43):

the merge rights are not restricted, so someone in ltac2-maintainers can eg merge a PR that only touches the kernel without issue

view this post on Zulip Théo Zimmermann (Dec 15 2023 at 10:15):

Indeed, we just trust people not to do this.

view this post on Zulip Théo Zimmermann (Dec 15 2023 at 10:16):

And for the record, we do not use all the levels of privilege that GitHub provides today. We give so-called "Write access" to members of the "Contributors" team because this allows also editing comments (e.g., from coqbot) and stuff like this. But again, we trust people that we put in "Contributors" not to abuse this.


Last updated: Oct 13 2024 at 01:02 UTC