Stream: Coq devs & plugin devs

Topic: Rocq roadmap


view this post on Zulip Gabriel Scherer (Oct 04 2024 at 07:42):

At the last Coq Call, the "rocq roadmap" document was discussed and I asked where to suggest changes to the document. People suggested it could be added to the https://github.com/coq/ceps (and merged?), so that we can send PRs against that. Has this been done yet? I wrote some local change proposals and I don't know where to send them. (Should I use this Zulip thread for this?)

view this post on Zulip Théo Zimmermann (Oct 04 2024 at 08:19):

Thanks for your reminder. I was thinking about this as well yesterday night. I see two options: either the current roadmap is copied to the repo and PRs are made against it. Or the current roadmap becomes a PR and people can review / suggest changes in the PR interface. And I have a feeling that the second method is better to allow more discussion, although it has also the risk that discussions don't converge.

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

I think I'll go with the second option if that's OK with everyone. cc @nicolas tabareau @Matthieu Sozeau @Yves Bertot

view this post on Zulip Gabriel Scherer (Oct 04 2024 at 08:24):

Both options are fine. They differ a bit in who does the work: if we send PR for changes, each change-proposer is responsible for proposing a specific rewording and iterate on it based on other people's feedback. If there is a single PR, the author of that PR will act as the "editor" and will have to keep iterating the PR in reaction to feedback in comments -- which may contain specific change proposals, but also more vague comments.

view this post on Zulip Théo Zimmermann (Oct 04 2024 at 08:31):

Indeed. In the second option, I would merge (or let other Coq core team members merge) uncontroversial suggestions quickly. But any vague comments may or may not eventually be acted upon.

view this post on Zulip Théo Zimmermann (Oct 04 2024 at 08:32):

We may also choose to go for the second option first, but not wait to long before merging the PR and moving to the first option then.

view this post on Zulip nicolas tabareau (Oct 04 2024 at 09:16):

I am more for the first option as the long-term roadmap has already been discussed during several meetings. I would like to avoid non-converging discussion on it. It seems the first option will favor constructive changes.

view this post on Zulip Théo Zimmermann (Oct 04 2024 at 10:16):

Done (PR opened and merged).

view this post on Zulip Gabriel Scherer (Oct 04 2024 at 20:18):

My follow-up PR: https://github.com/coq/ceps/pull/93

view this post on Zulip Théo Zimmermann (Oct 09 2024 at 05:56):

@nicolas tabareau Can we easily update the hosted version of the roadmap from the version in the CEPs repo? (to account for the two commits from Gabriel that were already merged)

view this post on Zulip nicolas tabareau (Oct 09 2024 at 06:39):

yes, we will do


Last updated: Oct 13 2024 at 01:02 UTC