Rocq Call 2025 09 23

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

Topics

• 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) (may get postponed again..)
• 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?
• 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: Matthieu
• Secretary: Théo
• Attending: Pierre Roux, Jim, Enrico, Andres, Théo, Matthieu

Notes

• Coupling between the micromega plugin and supporting theory is a problem.
  • Pierre thinks that moving a part of the supporting theory in Corelib will help with evolving micromega, and would make it easier for Stdlib to support multiple Rocq versions. The issue is that the plugin code reference constants that are defined in the Stdlib.
  • Andres proposes an alternative solution with conditional compilation in Stdlib.
  • However, there is another issue raised by Pierre, which is to be able to use micromega without depending on Stdlib.
  • Andres points out a change that would be made worse by the proposed change (the removal of a constructor enumProof from an inductive in the micromega supporting theory). Pierre claims that this is a very particular case, but not representative.
  • Discussion of how to test the micromega plugin with and without this change (currently, we could test only the ML API, but for end-to-end testing we would need the change).
  • This change could make it easier for Frédéric Besson to make change to the micromega plugin, but he hasn't taken position publicly on this issue yet.
  • Question whether this particular case shows general issue with the Stdlib split, and whether we should end this experiment.
  • Discussion of whether it is justified that MathComp doesn't want to depend on Stdlib and whether Stdlib is slow to compile or not. More general discussion on whether we want to provide first-class support to projects not wanting to use Stdlib, or if instead we should just make Stdlib good enough to get more people to use it.
  • This split would separate definitions and lemmas about these objects. If we were to move the lemmas as well, it would require moving a large part of Stdlib as well to Corelib, which Andres would support.
  • No conclusion or compromise reached yet...
• Jim's PRs.
  • Pierre-Marie seems to be unavailable lately. Matthieu may be able to look at the PR himself and check whether the remaining comments (in particular from Yann) need to be taken into account.
  • Jim's second PR is a documentation PR with a long history of delays between authors' changes and reviews (and conversely). Discussion about the need for more coordination between authors and reviewers for large changes. Matthieu will ping Thomas Lamiaux about this PR, and if he is not available, maybe Andres can find time to look at it.