Rocq Call 2025 12 16

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

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).