Stream: Coq devs & plugin devs

Topic: Unlabeled issues


view this post on Zulip Ali Caglayan (Jul 06 2021 at 23:04):

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

view this post on Zulip Théo Zimmermann (Jul 07 2021 at 07:54):

Yes @Ali Caglayan. Thank you for proposing your help!

view this post on Zulip Théo Zimmermann (Jul 07 2021 at 07:55):

You can put part: labels to indicate the component (and even create new part: labels if components are missing).

view this post on Zulip Théo Zimmermann (Jul 07 2021 at 07:56):

You can put kind: labels to indicate the nature e.g. kind: bug or kind: enhancement + kind: wish.

view this post on Zulip Théo Zimmermann (Jul 07 2021 at 07:56):

You can use needs: labels in case information is missing or action is needed, e.g. needs: feedback / needs: answer / needs: triage.

view this post on Zulip Théo Zimmermann (Jul 07 2021 at 08:01):

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.

view this post on Zulip Théo Zimmermann (Jul 07 2021 at 08:02):

Closing issues is the thing to do if you notice that a bug has been resolved in recent Coq versions.

view this post on Zulip Théo Zimmermann (Jul 07 2021 at 08:04):

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).

view this post on Zulip Théo Zimmermann (Jul 07 2021 at 08:05):

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).

view this post on Zulip Ali Caglayan (Jul 07 2021 at 09:22):

@Théo Zimmermann I don't see an invitation on github, I should just receive a notification right?

view this post on Zulip Théo Zimmermann (Jul 07 2021 at 09:22):

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.

view this post on Zulip Ali Caglayan (Jul 07 2021 at 09:24):

Ah excellent, thanks!

view this post on Zulip Emilio Jesús Gallego Arias (Jul 07 2021 at 09:40):

@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?

view this post on Zulip Ali Caglayan (Jul 07 2021 at 09:47):

That sounds like a great idea! I would be willing to help out.

view this post on Zulip Théo Zimmermann (Jul 07 2021 at 10:21):

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.

view this post on Zulip Théo Zimmermann (Jul 07 2021 at 10:22):

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.

view this post on Zulip Ali Caglayan (Jul 07 2021 at 10:31):

Is it generally worth removing the assignees added by coqbot?

view this post on Zulip Ali Caglayan (Jul 07 2021 at 10:32):

I've seen quite a few of those.

view this post on Zulip Théo Zimmermann (Jul 07 2021 at 11:59):

Yes, it was probably a mistake to keep the assignees from Bugzilla.

view this post on Zulip Gaëtan Gilbert (Jul 09 2021 at 07:08):

when closing issues which got solved at some point it may be worth considering adding a test

view this post on Zulip Ali Caglayan (Jul 09 2021 at 11:17):

How should I add a test for an anomaly that becomes an error message? How do I distinguish between the two?

view this post on Zulip Gaëtan Gilbert (Jul 09 2021 at 11:25):

Fail does not catch anomalies
If you want to test the specific error message you can also use an output test

view this post on Zulip Ali Caglayan (Jul 09 2021 at 11:48):

Really? I have an example where Fail catches anomalies:

Set Printing Universes.
Definition foo@{i j}(A:Type@{i})(B : Type@{j}) : True.
Proof.
  Fail constr_eq_strict (Type@{i}) (Type@{j}). (*normal expected failure*)
  Fail constr_eq_strict (Type@{i}) (Type@{i+1}). (*Anomaly*)
  Fail constr_eq_strict (Type@{i+1}) (Set). (*Anomaly*)
  Fail constr_eq_strict (Type@{i+1}) (Type@{j}). (*Anomaly*)
  Fail constr_eq_strict (Type@{i}) (Type@{max(i,j)}). (*Anomaly*)

This is https://github.com/coq/coq/issues/13825

view this post on Zulip Gaëtan Gilbert (Jul 09 2021 at 11:52):

that's an invalid_argument, not an anomaly
(it says anomaly uncaught exception because the error printer is wonky)

view this post on Zulip Gaëtan Gilbert (Jul 09 2021 at 11:55):

so for that you have to use an output test

view this post on Zulip Ali Caglayan (Jul 09 2021 at 11:56):

But this bug hasn't been fixed yet :-) It was just an example of the behavior of Fail

view this post on Zulip Ali Caglayan (Jul 09 2021 at 11:56):

But does that mean there are two bugs with 13825? The actual anomalies and the error messages?

view this post on Zulip Gaëtan Gilbert (Jul 09 2021 at 12:01):

just the error message, there is no anomaly

view this post on Zulip Gaëtan Gilbert (Jul 09 2021 at 12:03):

https://github.com/coq/coq/pull/14626

view this post on Zulip Ali Caglayan (Jul 09 2021 at 12:21):

I've added issues I've recently closed to the test-suite https://github.com/coq/coq/pull/14627

view this post on Zulip Ali Caglayan (Jul 10 2021 at 14:30):

@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.

view this post on Zulip Gaëtan Gilbert (Jul 10 2021 at 15:58):

you should request review from coq/test-suite-maintainers when you open PRs adding tests (separately from the fix)

view this post on Zulip Théo Zimmermann (Jul 10 2021 at 20:43):

Ali Caglayan said:

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.

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.

view this post on Zulip Gaëtan Gilbert (Jul 10 2021 at 20:46):

does needs: minimal example mean the current example is too big or that there is no current example?

view this post on Zulip Columbus (Jul 10 2021 at 20:52):

Maybe 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 :)

view this post on Zulip Ali Caglayan (Jul 10 2021 at 22:44):

I've created a needs: minimization label. I'll begin to use it.


Last updated: Oct 21 2021 at 21:03 UTC