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

Topics

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