There are currently ~600 issues without labels. Can I help label them? https://github.com/coq/coq/issues?q=is%3Aissue+is%3Aopen+no%3Alabel
Yes @Ali Caglayan. Thank you for proposing your help!
You can put
part: labels to indicate the component (and even create new
part: labels if components are missing).
You can put
kind: labels to indicate the nature e.g.
kind: bug or
kind: enhancement +
You can use
needs: labels in case information is missing or action is needed, e.g.
needs: feedback /
needs: answer /
I've invited you to join our Contributors team so that you have write access to the Coq repository. Note that beyond the ability to add or remove labels, it also gives you the ability to close / reopen issues or adding / removing milestones.
Closing issues is the thing to do if you notice that a bug has been resolved in recent Coq versions.
It also gives you the ability to edit comments from anyone, which can be useful to add formatting (e.g. code blocks) or to update the top post with new information (e.g., if you could reproduce in a more recent version of Coq).
Finally, because of a limitation of GitHub, it also gives you the power of accidentally pushing new branches to the Coq repository. So watch out and avoid doing this, as we prefer the main repo to only contain "official" branches (
master and release branches).
@Théo Zimmermann I don't see an invitation on github, I should just receive a notification right?
No, I think you should get an e-mail. But you can also go to https://github.com/coq and you should see an invitation.
Ah excellent, thanks!
@Ali Caglayan indeed any issue triaging is super welcome, thanks! I do think tho that we could benefit a bit of a more organized effort, in the spirit of Debian's Bug Squashing Parties, so indeed maybe we should try to organize one some day, wdyt?
That sounds like a great idea! I would be willing to help out.
Yeah I agree. Such a coordinated event would also be useful because people could discuss together when they are not sure what to do with a bug, and this could help share expertise and ideas.
BTW, something else that you can do is remove assignees when these do not make sense anymore (e.g. they were imported from the Bugzilla system 4 years ago) or ping the people who self-assign to ask them if they still intend to tackle the bug or should remove their assignments.
Is it generally worth removing the assignees added by coqbot?
I've seen quite a few of those.
Yes, it was probably a mistake to keep the assignees from Bugzilla.
when closing issues which got solved at some point it may be worth considering adding a test
I've added issues I've recently closed to the test-suite https://github.com/coq/coq/pull/14627
@Théo Zimmermann Should I create a
needs: minimal example label for issues that need a minimal reproducible example? This might also be useful for coqbot.
you should request review from coq/test-suite-maintainers when you open PRs adding tests (separately from the fix)
Ali Caglayan said:
Théo Zimmermann Should I create a
needs: minimal examplelabel for issues that need a minimal reproducible example? This might also be useful for coqbot.
Yes, that sounds like a good idea. More generally feel free to create any label that you feel is missing, especially if they belong to existing categories.
needs: minimal example mean the current example is too big or that there is no current example?
needs: minimization? I think there the connotation would be clear, that an example already exists, but it is too large. Or
needs: smaller example, who knows what the minimum actually is :)
I've created a
needs: minimization label. I'll begin to use it.
Last updated: Feb 01 2023 at 16:03 UTC