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

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

Topics

• Postponed Stdlib split, ML tactics, and supporting theory (https://github.com/rocq-prover/stdlib/pull/207) (Andres Erbsen, 15min) (c.f. https://github.com/rocq-prover/rocq/pull/21080 to better see the Corelib part)
• Postponed 20827: Retain original variable names for patterns in Print HintDb (Jim Fehrle, 5 minutes) - this simple PR has been ready since July. Perhaps Pierre-Marie would finish the review and merge?
• Postponed 19761: Refine Hint Opaque/Transparent documentation (Jim Fehrle, 10 minutes) - still waiting for a complete review/merge after creating the PR 11 months ago. Thomas made some comments but has not gotten back to me again. More generally, if the team wants better documentation, we need reviewers to make that possible. I've made a number of non-trivial improvements in the past, but if there are no reviewers, it's a waste of time to attempt more.

Roles

• Chairman: Nicolas Tabareau
• Secretary:
• Attending: Andres Erbsen, Gaëtan Gilbert, Yann Leray, Nicolas Tabareau, Théo Zimmermann

Notes

We discussed improving and clarifying the reviewer guidelines for PRs, with the aim of broadening the pool of reviewers. Many people outside the core team may be fully qualified and willing to review, but they need clear guidance on what is expected of them.

Andres and Théo will work on updating the CEP #86 and propose PRs for that purpose.