Rocq Call 2026 03 31 - rocq-prover/rocq GitHub Wiki

Topics

  • Governance rules approval procedure (Matthieu, 10min)
  • Policy with respect to LLM-generated PRs and such (Nicolas, 20min)

Roles

  • Chairman: Nicolas Tabareau
  • Secretary:
  • Attending:

Notes

Rocq Governance Updates

  • Add Yann Leray to the Rocq Core team and remove Yves Bertot
  • Clarify the process for renewing the team leader
  • Rephrase the statement on “attention to compatibility”
  • Specify that the rocq-core Zulip channel is the primary communication channel for Rocq developers
  • Note that Belenios votes require members’ email addresses
  • Close the coqdev mailing list
  • Move Equations into the Rocq Prover GitHub org
  • Fix the broken Code of Conduct link; reference HR resources and detail the reporting procedure (cf. Django).

Discussion on Generative AI Contributions

The team agreed that it is not yet necessary to take strong decisions on the use of generative AI contributions.

At this stage, there are still very few pull requests involving LLM-generated code in the Rocq codebase.

So far, only one such PR has been merged, consisting of a simple bug fix.

The team recommends monitoring the situation and drawing inspiration from existing discussions in the open-source community before adopting a more formal policy.

Relevant references: