Stream: Coq devs & plugin devs

Topic: Deprecated lemmas and upvoting issues


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip Cyril Cohen (Nov 23 2022 at 13:43):

(I will walk to Maxime's office for this one)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Cyril Cohen (Nov 23 2022 at 14:57):

This sorting completely ignores the feasibility (the first issue is solving the setoid hell :laughing:)

view this post on Zulip 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.

view this post on Zulip Ana de Almeida Borges (Nov 23 2022 at 15:20):

What about the high priority label?

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.).

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Nov 24 2022 at 09:29):

Karl Palmskog said:

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

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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Nov 24 2022 at 10:23):

sure, but how many are actively merging anything?

view this post on Zulip Théo Zimmermann (Nov 24 2022 at 10:24):

That's a good question and would also require some stats to answer.

view this post on Zulip 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".

view this post on Zulip Théo Zimmermann (Nov 24 2022 at 10:37):

Can you clarify what you have in mind? I'm not sure I completely follow.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Andres Erbsen (Nov 24 2022 at 16:59):

I'd like to share my (relative outsider's) perspective here.


Last updated: Feb 05 2023 at 23:30 UTC