I've seen several threads from some users asking for help. But one distinct thing I've noticed is that these threads only contain a brief description of the problem and some general description of code or goal state. I have to say that this is not a common thing in other communities. I haven't worked professionally, but generally I give a GitHub repo for context or some minimal example that demonstrates the issue I'm facing. And from what I've experienced this is generally the most common way folks ask questions in public communities. Could anyone explain to me why in this community posting only general information is somewhat more common? I'm not saying that showing a minimal example or giving complete project for context is the only good way to ask for debugging help, I'm just curious.
First, there are 3-4 people doing that a lot, but that's not typical and I'd set them aside. A difference is that this seems to be more tolerated than elsewhere.
For the rest, I think you're overestimating other communities, _or_ you've been in unusual ones.
asking for a minimal working example is definitely standard, and expert users tend to comply (before being asked), but
those are the minority (EDIT) those seem to be the minority
in my view, since this kind of community-detrimental behavior continues [despite advice and warnings] and is limited to a few accounts, people should consider reporting it
done — I'm trying to move the discussion to private, but the behavior in question has clearly gone on for a while and bothered multiple people
Would it be possible to add to Coq-Zulip's code of conduct some paragraph inspired by (or just a link to) Stack Overflow's advice on minimal reproducible examples ?
there's a Coq-Zulip code of conduct?
I think Pierre is referring to the general code of conduct: https://github.com/coq/coq/blob/master/CODE_OF_CONDUCT.md
by being a Coq official forum, the Zulip falls under this CoC (to my knowledge)
Tagging @Théo Zimmermann
I totally agree, there seems to have been a lot of waste of time because of people submitting coding problems without code or without enough context to reasonably point to a problem...
an augmented CoC could add specifics about giving reproducible examples under, say "Be considerate [with other people's time]". Or it could be a standalone point.
Furthermore, I noticed several times syntactically incorrect or incorrectly typed coq snippets (or just without calls to the libraries). We should ask posters to check before posting whether the code they post is self-contained and runs on a standard Coq version. Otherwise it's a total waste of time for us to try to answer.
On the other hand, it's OK to post a snippet which leads to an error, if the question is about a misunderstanding of the error message. Same thing whith an unresolved sub-goal.
FTR we added a section to the code of conduct.
Last updated: Nov 29 2023 at 21:01 UTC