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?)
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.
I think I'll go with the second option if that's OK with everyone. cc @nicolas tabareau @Matthieu Sozeau @Yves Bertot
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.
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.
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.
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.
Done (PR opened and merged).
My follow-up PR: https://github.com/coq/ceps/pull/93
@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)
yes, we will do
Last updated: Oct 13 2024 at 01:02 UTC