Stream: Coq users

Topic: (Lack of) Coq renaming


view this post on Zulip Peter Sewell (Oct 12 2022 at 08:28):

Is there any progress on the renaming of Coq? Sorry if I've missed it - I don't often use this zulip - but I've seen nothing. Within the community, perhaps habit can blind one to the problem, but when talking externally, with industry folk, department colleagues, students, and funding bodies, the historical name really isn't acceptable - and increasingly obviously so. I had hoped the previous discussion and survey would get somewhere...

view this post on Zulip Karl Palmskog (Oct 12 2022 at 08:31):

in the context of the Coq Community Survey 2022, we analyzed survey responses on the Coq renaming in the Coq Survey Working Group. You can see some of the results in this set of slides [slide page 39 and forward]. We have continously kept the Coq Core Team in the loop on our survey data analyses, but they have as-yet not made public any decision.

view this post on Zulip Théo Zimmermann (Oct 12 2022 at 10:43):

To add to Karl's comment, the Coq Community Survey WG has published a series of blog posts on the survey results and we (the WG) hope to add one about the renaming results in the coming weeks (mostly repeating, and perhaps extending a little, what has already been presented in the Coq workshop). As for the core team, we have discussed the matter several times based on the survey result, but the final decision is not completely settled yet (although, TBH, the question is no longer whether there will be a renaming).

view this post on Zulip Peter Sewell (Oct 12 2022 at 13:27):

Thanks both. I'll optimistically look forward to progress in due course.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 12 2022 at 13:53):

I think I can also share that we found some unexpected (and annoying) issues in the process, so that for sure has created IMHO significant delays in the discussion

view this post on Zulip Paolo Giarrusso (Oct 12 2022 at 18:14):

way to bury the lede @Théo Zimmermann — but I'll resist the temptation to retweet your reveal :-)

view this post on Zulip Peter Sewell (May 07 2023 at 08:30):

Still optimistically looking forward to progress?

view this post on Zulip Peter Sewell (May 07 2023 at 08:34):

(I wonder, while writing a grant proposal that currently has 94 regrettable references to genitalia...)

view this post on Zulip Théo Zimmermann (May 07 2023 at 19:17):

There will be more news on this topic, but in the meantime, just consider that the process has not stalled and is still moving at :turtle: pace.

view this post on Zulip Philipp G. Haselwarter (May 08 2023 at 23:17):

I caught myself googling for Coq maximally inserted earlier today. Please, make it stop.


Last updated: Jun 16 2024 at 02:41 UTC