Rocq Call 2025 10 07 - rocq-prover/rocq GitHub Wiki

Topics

  • implementing right-assoc as NEXT op SELF and further simplify gramlib implem to ignore associativities (c.f. #21072 and #21126 , Pierre, 20 min)
  • giving micromega its own repo #21080 (Pierre, 15 min)

Roles

  • Chairman: Nicolas Tabareau
  • Secretary: Nicolas Tabareau
  • Attending: Julien Cretin, Andres Erbsen, Enrico Tassi, Sylvain Borgogno, Théo Zimmerman, Pierre Roux, Emilio Gallego, Gaëtan Gilbert, Nicolas Tabareau

(NB: I forgot to note who were attending, please note your name if it is missing)

Notes

  • implementing right-assoc as NEXT op SELF and further simplify gramlib implem to ignore associativities (c.f. #21072 and #21126 , Pierre, 20 min)

We agreed on adding a deprecation warning and then simplify gramlib implem.

  • giving micromega its own repo #21080 (Pierre, 15 min)

This proposal has shed light again on the fact that splitting Stdlib from the Rocq repo is still not agreed upon as a good move. One of the main point in favor of splitting is to permit the development of the Stdlib independently from Rocq and the Corelib.

We agreed on trying to go back to RFC083 and collect the needs, and pros/cons from users and developers.

To make sure that the RFC summarize properly the discussion, we will do a call for volunteers on Zulip to follow the discussion and update the RFC.