Coq Call 2025 03 04

• 2025-03-04, 4pm UTC+1 (Paris time zone offset)
• https://rendez-vous.renater.fr/coq-call

Topics

• Rocq 9.0 status (Pierre-Marie, Matthieu, 5min)
• Governance organisation/policies (see website) (Matthieu, 15min)
• RUDW in Paris (Matthieu, 10min)

Roles

• Chairman: Nicolas Tabareau
• Secretary: Théo Zimmermann
• Attending: Gaëtan Gilbert, Guillaume Melquiond, Pierre-Marie Pédrot, Pierre Roux, Matthieu Sozeau, Nicolas Tabareau, Enrico Tassi

Notes

• Rocq 9.0.0 release. There are a few PRs that remain to be merged. The tag should be set in the upcoming days. We plan for the switch to the new website and the rocq-prover organization to happen on March 12th. Théo needs to write to GitHub support and Nicolas and Matthieu need to write to Inria support to have the coq.inria.fr website redirect to rocq-prover.org on this day.
• We also discussed the need to decouple the documentation deployment of the stdlib from the one of Rocq. Matthieu has put this on his to-do list, but we do not consider this to be a blocker.
• Discussion about the governance update. Matthieu has removed all mentions of the coordination team from the document. The discussion has initially focused on the renewing process of the Project Leader. Two main options were discussed: unbounded mandate unless someone in the core team asks for a vote or the project leader resigns; explicit renewal each year without a vote if there is a single candidate. The conclusion was that the second solution is preferred because it forces us to think about this regularly. Then, we discussed the removal of the coordination team and what it should be replaced with (a consortium team, a roadmap team, each of them open to any core team members that wish to be part of it).
• The title and URL of the Rocq Team page should be changed from "Governance" to "Rocq Team" (Nicolas will look into this).
• We also discussed the fact that we need to communicate more about new recruitments / arrivals. We could have a Zulip channel where new arrivals (interns, PhD students, engineers, etc.) are presented.
• We discussed also how to relaunch the roadmap efforts, and to keep each other updated of ongoing work. One idea is to have 15 minutes at the start of the Coq Call every month about this.
• Matthieu would like to have an online WG before the next RUDW, which will happen in Paris on the week of June 23rd (to be confirmed). There will be a related event organized by Enrico on June 23rd. Discussion of the naming of the RUDW event. Convergence on the name Rocq'n'code.