Stream: Coq devs & plugin devs

Topic: issue templates


view this post on Zulip Gaëtan Gilbert (Mar 05 2024 at 16:39):

not sure we need a coq call to decide this
is there any reason not to merge https://github.com/coq/coq/pull/14621 now?

view this post on Zulip Hugo Herbelin (Mar 05 2024 at 17:13):

Looks very cool! Maybe we merge and let it evolve with the practice?

About a few questions:

On a related note, I would split the inductive types label into inductive types and fixpoint because it is often unrelated. I find that reduction strategiesreferring to Strategy is too narrow. Maybe could it be renamed to control of reduction, referring to Strategy, Opaque, Tranparent, ... or generalized to include the reduction tactics (simpl, cbn, ...). Something about coqtop and coqc is missing (that could possibly put in Tools but Tools, currently starting with coqdoc is too narrow; so it could be Command line tools: coqtop, coqc, coqdoc, ... though I think I would put coqdoc and coq_makefile in their own category.

view this post on Zulip Théo Zimmermann (Mar 05 2024 at 20:07):

For the labels, feel free to do such changes directly.

view this post on Zulip Théo Zimmermann (Mar 05 2024 at 20:08):

For the PR, feel free to push a commit adding the "if any" if you think they are necessary. I didn't because none of the text boxes are compulsory.

view this post on Zulip Théo Zimmermann (Mar 05 2024 at 20:08):

I think indeed it doesn't need a Coq Call discussion probably.

view this post on Zulip Gaëtan Gilbert (Mar 08 2024 at 16:38):

merged
reminder that https://github.com/coq/coq/issues/new still produces a non-template issue (it is also linked as "open a blank issue" in a de-emphasized position from the template chooser)

view this post on Zulip Théo Zimmermann (Mar 12 2024 at 14:42):

This is still listed as a discussion point on https://github.com/coq/coq/wiki/Coq-Call-2024-03-19, but it could be removed now, right?

view this post on Zulip Gaëtan Gilbert (Mar 12 2024 at 14:43):

dnoe


Last updated: Oct 13 2024 at 01:02 UTC