Cyril Cohen (Nov 23 2022 at 13:21): Cyril Cohen (Nov 23 2022 at 13:21):Deprecation of Lemmas does not work, is there an agenda for fixing this? (cf coq/coq#12266) This looks like a very small thing that happens to make many people loose many precious minutes of time to circumvent. Hence my meta-question is in fact: how to upvote some issue?
Maxime Dénès (Nov 23 2022 at 13:30):On the meta question, I guess @Théo Zimmermann may have some suggestions. For this particular instance, I'm having a look now, trying add proper support for the deprecated attribute.
Théo Zimmermann (Nov 23 2022 at 13:39):My only suggestion is: team up with a mentor and implement the feature you are missing. We should definitely re-organize the annual CUDW.
Théo Zimmermann (Nov 23 2022 at 13:42):Longer term, I hope we can achieve some better organization of issues so that contributors can pick them up more easily.
Cyril Cohen (Nov 23 2022 at 13:42):Théo Zimmermann said:
My only suggestion is: team up with a mentor and implement the feature you are missing. We should definitely re-organize the annual CUDW.
Personally I'm not ready to do that for all issues I encounter ... I already work at too many levels up the software stack :confused:
Cyril Cohen (Nov 23 2022 at 13:43):(I will walk to Maxime's office for this one)
Gaëtan Gilbert (Nov 23 2022 at 13:45):maybe we should ask people for their top issue regularly (once a month? once after each release?)
eg open zulip or discourse thread, any user can post 1 issue
Théo Zimmermann (Nov 23 2022 at 13:47):In the meantime, you can already do this: https://github.com/coq/coq/issues?q=is%3Aissue+is%3Aopen+sort%3Areactions-%2B1-desc
Cyril Cohen (Nov 23 2022 at 14:57):This sorting completely ignores the feasibility (the first issue is solving the setoid hell :laughing:)
Théo Zimmermann (Nov 23 2022 at 15:18):Yes, but I think Gaëtan's proposal also ignored it :stuck_out_tongue: That's why I'm hoping for a more advanced way of organizing our issues and sorting our priorities but it's future work.
Ana de Almeida Borges (Nov 23 2022 at 15:20):What about the high priority label?
Théo Zimmermann (Nov 23 2022 at 16:13):We do not use that much. But there is no point on using such a label if there is no commitment from the team to address it. So the two things should be discussed together (how to prioritize and how to ensure that priority get worked on).
Maxime Dénès (Nov 24 2022 at 08:31):It would be a good idea to call users for upvoting the issues they want to see fixed.
Karl Palmskog (Nov 24 2022 at 08:45):for outsidecoq repo contributors, one worry is often that even if a solution is proposed as PR, it won't be merged or will require a long discussion process with lots of changes before it can be merged. It would be nice if one could know before working on some issue that, if a proposed PR solves the issue in some reasonable way, it will be processed quickly (unless there are unexpected CI issues, etc.).
Maxime Dénès (Nov 24 2022 at 09:02):it is very often hard to know in advance the technical implications of an issue (even for core developers), that could lead to PRs piling up before it can be fixed
Maxime Dénès (Nov 24 2022 at 09:03):what is typically done to avoid this effect is a building a roadmap, with some preliminary technical investigation to properly assess the technical difficulty of the various items
Théo Zimmermann (Nov 24 2022 at 09:28):Maxime Dénès said:
It would be a good idea to call users for upvoting the issues they want to see fixed.
No point in doing that (it could even be discouraging) if it's not part of an effort where developers commit time to address the issues that have been upvoted the most.
Enrico Tassi (Nov 24 2022 at 09:29):Karl Palmskog said:
for outside
coqrepo contributors, one worry is often that even if a solution is proposed as PR, it won't be merged or will require a long discussion process with lots of changes before it can be merged. It would be nice if one could know before working on some issue that, if a proposed PR solves the issue in some reasonable way, it will be processed quickly (unless there are unexpected CI issues, etc.).
I know this is sometime sad and frustrating, but I think this is the case for any software project that tries to enforce some quality standard.
When the change is user facing and not localized, I suggest one first does a CEP for the design (this is why they were introduced).
To my knowledge, long PR discussions only arise when the design is wrong to some dev, and this is can usually be discovered early, on the CEP or on a quick prototype.
Ideally a change which no dev feels important (out of the roadmap, which we don't have but we are building) is not going to be promptly reviewed, on the contrary stuff which is a priority will receive more attention. At least, this is what we aim at.
The problem with "one could know before working on some issue that" is that, in the past, has miserably failed to provide a good development process around the "white pass". I'm sorry, but it does not work well, especially for non trivial changes.
Maxime Dénès (Nov 24 2022 at 09:49):Théo Zimmermann said:
No point in doing that (it could even be discouraging) if it's not part of an effort where developers commit time to address the issues that have been upvoted the most.
There's a kind of chicken and egg problem. I still think this kind of input would be interesting, e.g. for Consortium engineers.
Théo Zimmermann (Nov 24 2022 at 10:12):There's a kind of chicken and egg problem.
I don't think that there is a chicken and egg problem because we already have huge amount of data which we do not properly exploit. That being said, if you think that this would be useful to you or specific developers, do not refrain from making such call.
Karl Palmskog (Nov 24 2022 at 10:19):if there is no "fast track" for PRs addressing smaller issues that are localized (e.g., in tools such as coqdoc), then they are likely going to be around for a long time (possibly forever)
Théo Zimmermann (Nov 24 2022 at 10:21):I should just produce stats on PR review time so that we are not discussing something completely virtual.
Théo Zimmermann (Nov 24 2022 at 10:22):In any case, you should know that PRs that change localized components result in review requests to different maintainers and as a consequence the processing time of the PR highly depends on reviewer availability for this component.
Karl Palmskog (Nov 24 2022 at 10:22):I sometimes get sufficiently annoyed to fix something small, but if nearly all devs (people who can merge) will put these very low in their priorities, this is a major disincentive
Théo Zimmermann (Nov 24 2022 at 10:22):So with stats, we could identify components which are not sufficiently well-maintained and devise specific actions for them (such as looking for new maintainers).
Théo Zimmermann (Nov 24 2022 at 10:23):You're aware that there are over 30 people with the power to merge PRs, right?
Karl Palmskog (Nov 24 2022 at 10:23):sure, but how many are actively merging anything?
Théo Zimmermann (Nov 24 2022 at 10:24):That's a good question and would also require some stats to answer.
Karl Palmskog (Nov 24 2022 at 10:26):I think signaling from some people who can merge would help a lot. Something like marking something "good first issue" but more fine-grained and going beyond "first issue".
Théo Zimmermann (Nov 24 2022 at 10:37):Can you clarify what you have in mind? I'm not sure I completely follow.
Karl Palmskog (Nov 24 2022 at 10:40):in smaller GitHub projects, sometimes issues are marked "good first issue", which is a kind of signal that the maintainer would welcome a solution and be nice when reviewing PRs. In Coq, maintainers of different subsystems might use issue tags to declare that they would welcome solutions to certain issues (the issues are not at the bottom of their priority list), and lead a PR to merge
Karl Palmskog (Nov 24 2022 at 10:45):one analogy might be with academics that have lists of bachelor-level or master-level projects (briefly described) that they would be happy to supervise.
Karl Palmskog (Nov 24 2022 at 10:49):if we can't do nudges like this, it would be helpful to make the general statistics for a subsystem publicly available. If it takes several weeks or months to even get a reaction for some PR, then everybody knows what to expect and can conserve their time
Théo Zimmermann (Nov 24 2022 at 11:34):Karl Palmskog said:
in smaller GitHub projects, sometimes issues are marked "good first issue", which is a kind of signal that the maintainer would welcome a solution and be nice when reviewing PRs. In Coq, maintainers of different subsystems might use issue tags to declare that they would welcome solutions to certain issues (the issues are not at the bottom of their priority list), and lead a PR to merge
This is a really good idea. So far the "good first issue" label has been used really erratically and with no such promises. Delegating to maintainers of components to tag specific issues like this would make a lot of sense.
Andres Erbsen (Nov 24 2022 at 16:59):I'd like to share my (relative outsider's) perspective here.
Last updated: Dec 07 2023 at 14:02 UTC