I just saw Théo's plans for Coq issue management. In particular, I want to comment on the following:
- A documented known issue which is not receiving activity should be closed.
- Any known issue receiving new activity (a new comment or a contributor self-assigning the issue) should be reopened (and reclosed if it becomes stale again).
In practice, this means that most issues at any time will either be closed or become closed soon. And this means that users reporting issues will need to search among closed issues to figure out if what they are reporting is a duplicate (which probably will not happen). This to me is a big disincentive to report issues at all, since either an issue was already reported and known and then closed, or it's a new issue that very likely will become known and then closed.
regardless of how having many open issues might be bad in other respects, at least casual users can figure out if something similar was reported quite easily and pile on to that discussion
Why is it bad to have many open issues? My first answer is something like "we get overwhelmed and it's hard to prioritize". But closing stale or known issues does not seem to me to really help with that.
IMO the best thing about Théo's proposal is the effort to document known issues. That seems like a really great idea. Then it would be important to have a way of distinguishing unsolved but documented issues from unsolved and undocumented issues. But this does not need to be the open/closed status of the issue, it could just be some special tag.
For sure, the part "closing known documented but stale issues" doesn't have to be implemented and can be debated or replaced by something else entirely. But my impression is that the current state of things makes navigating the list of open issues hard enough so that, in practice, there are many issues that still get reported multiple times and the list of open issues is not helpful to the users who want to contribute fixes either. The integration of known issues in the documentation should ease both things: figuring out if an issue is known already, knowing where to contribute with new reproduction cases / insight, and also knowing what are the known issues regarding a component and picking up something that is currently not worked on. Our contributing documentation should then point rather clearly toward these resources.
one important point where tooling can likely help is locating and dealing with duplicates. There has to be a bunch of approaches to this based on learning and the like.
For long-standing issues that aren't likely to be fixed soon, I agree on documenting them... eg semantics of cbn and simpl are not ideal, but most changes (especially to simpl) are likely to have huge impacts...
But otherwise, one can just use planning tools — Agda has the “icebox” milestone for things that aren’t going to be fixed anytime soon. A stalebot that tagged things with such a milestone seems much more tolerable to me.
More tolerable than closing, correct? But you also seem to imply that some known issues are not worth documenting. Is this really your point?
what does documenting mean? I don't think we want to dump hundreds of issues in the refman
a complete spec for both simpl
and cbn
seems a good idea.
you need that anyway if you’re actually trying to use Arguments
I don't think we want to dump hundreds of issues in the refman
I guess we should prioritize documenting known issues that are most commonly puzzling users and see where we go from there.
that’s a better idea
on the other extreme, an iceboxed crash is hopefully not something that will go in the manual?
nobody’s going to rely on the crash, so you always have the option of changing the behavior. Meanwhile, the issue tracker is enough documentation.
but I’m probably making a very different point: some bugs aren’t bugs anymore, but just “X has a cursed spec that we’re stuck with”, so they’re part of the manual.
for another example, no chance to make simpl never
do what it says; at best, we can rename that (with deprecation) to a better name if one exists (maybe simpl lazily
?)
Gaëtan Gilbert said:
what does documenting mean? I don't think we want to dump hundreds of issues in the refman
Actually I'm curious about what the number will be, but indeed it is high; and Coq has not the best reputation because of them, so we better start trying to realize about it
Last updated: Oct 13 2024 at 01:02 UTC