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?
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.
My only suggestion is: team up with a mentor and implement the feature you are missing. We should definitely re-organize the annual CUDW.
Longer term, I hope we can achieve some better organization of issues so that contributors can pick them up more easily.
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:
(I will walk to Maxime's office for this one)
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
In the meantime, you can already do this: https://github.com/coq/coq/issues?q=is%3Aissue+is%3Aopen+sort%3Areactions-%2B1-desc
This sorting completely ignores the feasibility (the first issue is solving the setoid hell :laughing:)
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.
What about the high priority label?
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).
It would be a good idea to call users for upvoting the issues they want to see fixed.
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.).
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
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
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.
Karl Palmskog said:
for outside
coq
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.).
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.
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.
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.
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)
I should just produce stats on PR review time so that we are not discussing something completely virtual.
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.
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
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).
You're aware that there are over 30 people with the power to merge PRs, right?
sure, but how many are actively merging anything?
That's a good question and would also require some stats to answer.
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".
Can you clarify what you have in mind? I'm not sure I completely follow.
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
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.
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
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.
I'd like to share my (relative outsider's) perspective here.
Last updated: Jun 04 2023 at 19:30 UTC