Rocq Call 2025 12 16 - rocq-prover/rocq GitHub Wiki

Topics

  • Rocq’n’share planning (Matthieu, 10min)
  • RocqPL dev session planning (Matthieu, 10min)
  • Planning for 9.2 release and discuss which open PR should be merge before freezing (Nicolas, 10min)
  • future of summary (https://github.com/rocq-prover/rocq/pull/21160) (Gaëtan, 15min)

Roles

  • Chairman: Nicolas
  • Secretary: Théo
  • Attending: Matthieu, Gaëtan, Yann, Enrico, PMP, Nicolas, Théo

Notes

Rocq'n'share

  • À Lausanne (EPFL) sur le campus (quatre salles).
  • Sponsorisé par la Fondation Informatique de Suisse. Possibilité d'aider les gens qui en auraient besoin avec cet argent ou celui du consortium.
  • Hôtels sur le campus, mais les tarifs sont élevés.
  • Dates : semaine du 22 au 26 juin (Théo pas dispo cette semaine-là).
  • Alternative : semaine du 29 juin au 3 juillet (en conflit avec ECOOP).

RocqPL dev session

  • Présents : Gaëtan, Matthieu, Yann, Cyril. Absents : Enrico (mais présent à CPP), PMP, Nicolas, Théo.
  • Seulement 45 minutes pour la session. (10 minutes de présentation ou bien focaliser sur une démo ?, 35 minutes de questions ? ou bien commencer par les questions ?)

Future of summary

  • pull request de Gaëtan (https://github.com/rocq-prover/rocq/pull/21160)
  • objectif d'aller vers moins d'état / code plus fonctionnel
  • discussion sur la manière de gérer les flags de debug / warning
  • éviter des bugs dans VsRocq
  • casse les plugins
  • Faut-il organiser un sprint pour effectuer rapidement les changements nécessaires dans Elpi sans que ça engendre des conflits avec la branche sur les univers ? PMP voudrait pouvoir merger la pull request rapidement, donc sans attendre Rocq'n'share. En tout cas, Enrico ne pourra pas aider avant POPL.
  • Informer les mainteneurs de plugins qu'on aura besoin de leur aide fin janvier ?
  • Mais stabiliser l'API d'abord ? Avec ou sans monades ? Le problème est qu'il s'agit d'une monade Reader sur un état potentiellement impur.

Release de Rocq 9.2

  • Nicolas est le RM désigné volontaire.
  • Branche début ou mi-janvier pour une release en mars.
  • PMP recommande de ne pas rajouter des changements importants au dernier moment et de plutôt polir les choses déjà dans la release (pas plus de features pour 9.2).
  • Une pull request de Thomas Lamiaux à revert pour la 9.2 ?
  • Attention à ne pas aller trop vite sur #21416.
  • Gaëtan aimerait avoir #21417, mais PMP n'est pas convaincu non plus.

Future maintenance de rocq-lsp, vsrocq, docker-rocq

  • Emilio est parti chez Lean FRO et n'a plus le droit de travailler sur Rocq
  • il est ok pour transférer la maintenance de rocq-lsp à Nicolas
  • proposition de transfert dans rocq-community en attendant de décider quoi transférer dans rocq-core. Nicolas et Josselin pourraient en être admin.
  • Erik est parti également dans le privé, et ne pourra plus maintenir docker-rocq. Sylvain va prendre le relais (visio ce matin avec Théo).