Rocq Call 2026 02 03

• 16:00 UTC+1:00 (CET, Paris time zone offset)
• https://rendez-vous.renater.fr/rocq-call

Topics

• Adding Yann Leray to the core team (proposed by Matthieu, 5min)
• vsrocq licensing (https://github.com/rocq-prover/vsrocq/issues/1195, Gaëtan, 10min)

Roles

• Chairman: Nicolas Tabareau
• Secretary: Pierre Roux
• Attending: Hugo Herbelin, Gaëtan Gilbert, Yann Leray, Guillaume Melquiond, Pierre Roux, Matthieu Sozeau, Nicolas Tabareau, Enrico Tassi, Theo Zimmermann

Notes

• Short reminder that https://github.com/rocq-prover/rocq/pull/21549 is waiting for explicit agreement from concerned parties before being merged
• vsrocq licensing https://github.com/rocq-prover/vsrocq/issues/1195
  • vsrocq is MIT but statically linked on rocq-runtime under LGPL, we have an issue
  • the license applying on vsrocq-server should be LGPL
  • probably also code copied from runtime (but maybe not much), so should be LGPL anyway
  • should we ask to authors? (Maxime and Romain) technically no, MIT allows being changed to LGPL
  • only thing that really need to be fixed is the licence of the package, not of the code itself
• Adding Yann Leray to the core team
  • Yann added two months ago to the kernel team (we should already know since there are notifications on Zulip)
  • also removed Emilio since he is no longer allowed to contribute to Rocq (question about retrieving the "former members" section of the old website)
  • what's the process to add someone to core team? being coopted by core team
  • previously, this was discussed privately, Yann leaving at this point
  • we have all the core team attending this meeting, but Jason, Yves and Pierre-Marie
  • we just want to be careful not to overload Yann while he is writing his PhD thesis
  • -> Ok