Stream: Coq devs & plugin devs

Topic: Closing of known issues


view this post on Zulip Karl Palmskog (Nov 12 2021 at 13:49):

I just saw Théo's plans for Coq issue management. In particular, I want to comment on the following:

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.

view this post on Zulip Karl Palmskog (Nov 12 2021 at 13:53):

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

view this post on Zulip Ana de Almeida Borges (Nov 12 2021 at 14:09):

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.

view this post on Zulip Théo Zimmermann (Nov 12 2021 at 14:19):

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.

view this post on Zulip Karl Palmskog (Nov 12 2021 at 14:21):

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.

view this post on Zulip Paolo Giarrusso (Nov 12 2021 at 17:37):

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

view this post on Zulip Paolo Giarrusso (Nov 12 2021 at 17:41):

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.

view this post on Zulip Théo Zimmermann (Nov 12 2021 at 18:01):

More tolerable than closing, correct? But you also seem to imply that some known issues are not worth documenting. Is this really your point?

view this post on Zulip Gaëtan Gilbert (Nov 12 2021 at 18:06):

what does documenting mean? I don't think we want to dump hundreds of issues in the refman

view this post on Zulip Paolo Giarrusso (Nov 12 2021 at 18:15):

a complete spec for both simpl and cbn seems a good idea.

view this post on Zulip Paolo Giarrusso (Nov 12 2021 at 18:17):

you need that anyway if you’re actually trying to use Arguments

view this post on Zulip Théo Zimmermann (Nov 12 2021 at 18:17):

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.

view this post on Zulip Paolo Giarrusso (Nov 12 2021 at 18:17):

that’s a better idea

view this post on Zulip Paolo Giarrusso (Nov 12 2021 at 18:17):

on the other extreme, an iceboxed crash is hopefully not something that will go in the manual?

view this post on Zulip Paolo Giarrusso (Nov 12 2021 at 18:19):

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.

view this post on Zulip Paolo Giarrusso (Nov 12 2021 at 18:21):

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.

view this post on Zulip Paolo Giarrusso (Nov 12 2021 at 18:26):

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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 13 2021 at 11:42):

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: Feb 02 2023 at 15:04 UTC