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.
if you ask you're likely to get it
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
doubt
surprisingly, people actually get motivated by that stuff
I think there is anyway an informal gamification going on
anyway github's permission model doesn't have many steps for "more privileges over time"
there's
you can get added to various teams, right? And I think there are privileges associated with teams for specific code
It's more like the "spam" you get when someone open a PR.
the teams subscribe you to review requests for that team and give you "merge stuff" rights
that's all
the merge rights are not restricted, so someone in ltac2-maintainers can eg merge a PR that only touches the kernel without issue
Indeed, we just trust people not to do this.
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