I will be bug squashing some bugs this evening. I will be on BBB: https://bbb.inria.fr/gal-afg-2va-fun

At the moment, looking at the internals of coqdep to fix some spurious warnings about plugins not being found: https://github.com/coq/coq/issues/11026

Are you planning a specific strategy to the bug squashing party? i.e. sort by oldest and see if the issues are still replicable, etc?

What is the strategy if something did not really work in older versions of Coq, but it has been fixed in newer versions?

If it has been fixed then we can close the issue.

Depending on the bug it might be worth adding a test case to the test-suite.

Oldest issues are fine to go through

All issues have been labelled but some are labelled better than others

A good place to start is the `kind: bug`

label

Or if you have a specific component in mind, then the `part: coqdep`

label for instance will have a lot of issues concentrated on that

Labels can be found here: https://github.com/coq/coq/labels

Cool, what about issues that do not give details? i.e. "Something does now rok on Windows" without specifying Win version nor Coq version? Shall we try to ping the reporters?

If there is a linked development but no minimal test case for instance, then we can add a `needs: minimization`

label for future minimizing work.

For now, I cannot elevate your labeling privileges so you can ping me here to label things.

For issues that really don't have any details then just put them here and we can close them.

FYI we are on BBB if you want to chat on audio

Also finding minimal examples for bugs is quite important, if anybody is interested I can show how the bug minimizing scripts from coq-tools can be used to do this.

Thanks! I'll go through some issues later (Eastern time) and post the links here (esp for those who might need a re-labelling or may be incomplete/closed)

Small contribution (just questions tbh)

Higher-order question: Are there any plans to narrow down the number of tags and relabel everything with the elements of the new smaller set?

=============

https://github.com/coq/coq/issues/2338

`Which version of Windows? There is a much newer comment (from 2020) without much info. This issue is not labelled as kind:bug; should we go for it and ask for more info?

==============

https://github.com/coq/coq/issues/2372

I am confused, but is this still open in newer versions?

Maybe relabel with discussion / redesign?

==========

https://github.com/coq/coq/issues/2417

(Maybe I'm wrong) but I thought this has been fixed (or I'm just missing the point of this issue)?

Hanneli Tavante said:

Small contribution (just questions tbh)

Higher-order question: Are there any plans to narrow down the number of tags and relabel everything with the elements of the new smaller set?

AFAIK there are no plans to make the number of tags smaller. cc @Théo Zimmermann Perhaps we can have a discussion about this, since it is necessary to document the utility and function of tags. I also don't believe having a smaller number of tags is particularly useful at the moment. We have 2.5k issues, so having a small set of tags will make it impossible to search for specific things.

https://github.com/coq/coq/issues/2338

`Which version of Windows? There is a much newer comment (from 2020) without much info. This issue is not labelled as kind:bug; should we go for it and ask for more info?

I think it would be good to ask for more information, I can label it as bug. AFAIK we jump through some hoops in order to get the correct windows path. We should definitely try to reproduce on other platforms to make sure it is a windows bug. cc @Michael Soegtrop

https://github.com/coq/coq/issues/2372

I am confused, but is this still open in newer versions?

Maybe relabel with discussion / redesign?

====

https://github.com/coq/coq/issues/2417(Maybe I'm wrong) but I thought this has been fixed (or I'm just missing the point of this issue)?

Seems like these have been addressed. Thanks for highlighting!

Regarding number of labels, when we got past a certain point we introduced the current categories, and they have been helpful to make subsequent growth more manageable. At this point, I also do not know what we would gain by reducing the number, but sure, this is up for debate.

Sorry, I should have explained better the labelling suggestion... There are over 100 labels, so it can be a bit tricky to label issues appropriately. I agree the gain may be not significant. It could help the reportes to do a better tagging.

What I think would really help is a document explaining how to label issues, and which would explain the various categories. Currently, all we have is https://github.com/coq/coq/blob/master/CONTRIBUTING.md#helping-triage-existing-issues (and https://github.com/coq/coq/blob/master/CONTRIBUTING.md#understanding-reviewers-feedback for labels that apply to PRs).

I'm trying to have a look at issues tagged "part:IDE".

One question that I should have asked yesterday during Gaëtan's session: when you fix an issue, do you run the test-suite locally on your machine, or do you rely only on CI? Maybe it depends on the confidence that you have in your fix?

You can run it locally on your machine if you like, but there is nothing stopping you from submitting a *draft* PR on GitHub.

Running the test-suite locally is sometimes more convenient, but not necessary.

Théo Zimmermann said:

What I think would really help is a document explaining how to label issues, and which would explain the various categories.

IINM not everyone can label issues, and that means there will often be a lag between the creation of an issue and its labeling. So it's not only that people don't know which labels to use, it's also that sometimes they can't label at all. And the people who can are more likely to understand the labeling scheme anyway.

I analysed https://github.com/coq/coq/issues/15604. It is easy to understand, but I'm not sure what the right fix is.

FWIW, we're pretty open to adding new people to our Contributors team so that they can help with issue triaging.

More questions on open issues:

====================

https://github.com/coq/coq/issues/2456

I thought this issue had been closed on this PR https://github.com/coq/coq/pull/500 , no?

Any idea of what's left?

====================

https://github.com/coq/coq/issues/2465

Same here, there is a PR https://github.com/coq/coq/issues/10701

===================

https://github.com/coq/coq/issues/2494

Sorry, what is the purpose of an issue to a FAQ?

=================

https://github.com/coq/coq/issues/2514

Maybe I'm missing something, but is this still an issue in newer versions?

https://github.com/coq/coq/issues/2465

Same here, there is a PR https://github.com/coq/coq/issues/10701

that's not a PR

https://github.com/coq/coq/issues/2514

Maybe I'm missing something, but is this still an issue in newer versions?

it's still an issue

Sorry about 2465, I got confused

========

https://github.com/coq/coq/issues/2689

Maybe we can label this one as a bug?

There is a follow-up - https://github.com/coq/coq/issues/2690 saying 2689 is not a bug (I don't fully get the reason), but 2690 is not labelled as a bug either.

============

The first one seems like a user error to me

But the second one might be an actual bug

I've labelled it as a bug for now, but it is really to do with the design of the fsetdec tactic.

Last updated: Jan 29 2023 at 15:02 UTC