Ali Caglayan (Feb 15 2022 at 19:05): Ali Caglayan (Feb 15 2022 at 19:05):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
Hanneli Tavante (Feb 15 2022 at 19:47):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?
Ali Caglayan (Feb 15 2022 at 20:14):If it has been fixed then we can close the issue.
Ali Caglayan (Feb 15 2022 at 20:14):Depending on the bug it might be worth adding a test case to the test-suite.
Ali Caglayan (Feb 15 2022 at 20:14):Oldest issues are fine to go through
Ali Caglayan (Feb 15 2022 at 20:15):All issues have been labelled but some are labelled better than others
Ali Caglayan (Feb 15 2022 at 20:15):A good place to start is the kind: bug label
Ali Caglayan (Feb 15 2022 at 20:15):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
Ali Caglayan (Feb 15 2022 at 20:16):Labels can be found here: https://github.com/coq/coq/labels
Hanneli Tavante (Feb 15 2022 at 20:17):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?
Ali Caglayan (Feb 15 2022 at 20:19):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.
Ali Caglayan (Feb 15 2022 at 20:19):For now, I cannot elevate your labeling privileges so you can ping me here to label things.
Ali Caglayan (Feb 15 2022 at 20:19):For issues that really don't have any details then just put them here and we can close them.
Ali Caglayan (Feb 15 2022 at 20:20):FYI we are on BBB if you want to chat on audio
Ali Caglayan (Feb 15 2022 at 20:23):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.
Hanneli Tavante (Feb 15 2022 at 20:38):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)
Hanneli Tavante (Feb 16 2022 at 16:09):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)?
Ali Caglayan (Feb 16 2022 at 18:06):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!
Théo Zimmermann (Feb 16 2022 at 21:09):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.
Hanneli Tavante (Feb 16 2022 at 21:17):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.
Théo Zimmermann (Feb 17 2022 at 07:34):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).
Jean-Christophe Léchenet (Feb 17 2022 at 09:10):I'm trying to have a look at issues tagged "part:IDE".
Jean-Christophe Léchenet (Feb 17 2022 at 09:28):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?
Ali Caglayan (Feb 17 2022 at 09:31):You can run it locally on your machine if you like, but there is nothing stopping you from submitting a draft PR on GitHub.
Ali Caglayan (Feb 17 2022 at 09:32):Running the test-suite locally is sometimes more convenient, but not necessary.
Ana de Almeida Borges (Feb 17 2022 at 10:23):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.
Jean-Christophe Léchenet (Feb 17 2022 at 10:43):I analysed https://github.com/coq/coq/issues/15604. It is easy to understand, but I'm not sure what the right fix is.
Théo Zimmermann (Feb 17 2022 at 11:27):FWIW, we're pretty open to adding new people to our Contributors team so that they can help with issue triaging.
Hanneli Tavante (Feb 17 2022 at 16:22):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?
Gaëtan Gilbert (Feb 17 2022 at 16:46):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
Gaëtan Gilbert (Feb 17 2022 at 16:47):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
Hanneli Tavante (Feb 17 2022 at 16:53):Sorry about 2465, I got confused
Hanneli Tavante (Feb 17 2022 at 21:17):========
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.
============
Ali Caglayan (Feb 17 2022 at 21:30):The first one seems like a user error to me
Ali Caglayan (Feb 17 2022 at 21:30):But the second one might be an actual bug
Ali Caglayan (Feb 17 2022 at 21:30):I've labelled it as a bug for now, but it is really to do with the design of the fsetdec tactic.
Last updated: Jun 11 2023 at 00:30 UTC