Rocq Call 2026 04 28 - rocq-prover/rocq GitHub Wiki

Topics

Roles

  • Chairman: Nicolas Tabareau
  • Secretary: Matthieu Sozeau

Notes

  • next RM for 9.3 (Nicolas, 5min)

    • Planned march until september
    • Enrico and Nicolas together

  • adding ssreflect to Prelude ( https://github.com/rocq-prover/rocq/pull/21776 , Pierre, 20 minutes)

    • Pierre-Marie points that the prelude should get smaller not larger
    • Pierre and Cyril were not aware of that "policy"
    • Pierre, Cyril and Enrico: moving to prelude avoids later conflicts when choosing to import ssreflect in a dev not using it previously.
    • Pierre-Marie: but that is inherently non-modular, and will prevents conflicting interpretations later on.
    • Andres: not only notations but interpretations are imported, implicitly changing the global environment for everyone, with potential impact
    • Pierre: this does not force to use the additional tactics. should not have impact on anyone, as long as they don't use a conflicting notation (?).
    • Cyril: want to guarantee that news devs cannot be incompatible with working with a common "blessed" set of tactics, which should include ssr tactics.
    • Pierre-Marie: this PR doesn't achieve impossibility to break previous notations, as one can override them (?)
    • Hugo: this stems from past divergence on syntax between ssr and vanilla tactics.
    • Matthieu: propose to rather periodically run a check that Require Import ssreflect in prelude is compatible, a compromise to ensure more compatibility without growing the default grammar implicitly.
    • Pierre-Marie: parsing is inherently non-modular and this is adding more non-modular declarations affecting everyone. He argues we should rather make things more modular by not tying to a specific tactic set (even Ltac1).
    • ...
    • Conclusion: for now, let's run a poll, on preference for a more modular setup (but forcing explicit Require Ltac1 / Ltac2 / Ssreflect / ...) or to bake in the ssr syntax (w or w/o its intepretation) as soon as the Prelude is required. Pierre-Marie is on it.

  • micromega-plugin ( https://github.com/rocq-prover/stdlib/pull/251 , Pierre, 20 minutes)

    • Micromega PR (initially) backward-incompatible stdlib
    • Pierre's PR proposes to move micromega to a separate plugin independent from stdlib (only Corelib), and have the Stdlib part reuse the micromega ML code.
    • .v files for proofs are in separate libraries
    • The theories in stdlib and math-comp are very different (Z/Q/R vs algebra)
    • Pierre Roux: one cannot easily generalize the micromega tactics / interface to export
    • Pierre-Marie and Andres: why can't we use the existing abstractions and structures from the stdlib to avoid duplication?
    • Matthieu: Here my (not very well-informed) understanding of the discussion is that math-comp's instances (and bindings? to the micromega plugin code) differ significantly from the stdlib instances, so there's no possible reuse in that direction. Moving the math-comp structures back to the stdlib would be a very large scale endeavor. So, as Pierre argues, it's useful to have a micromega plugin with two instances, in the stdlib and math-comp. (Note: I might have gotten it wrong, the discussion/arguments were not entirely clear to me at least)
    • Frédéric said he was not sure how to decide on the best solution
    • Moving back to Corelib the proofs (but not the micromega-specific bindings?) in the Stdlib would be a possibility, but Andres argues this would be simplified by moving back the Stdlib into the main repo and avoid having multiple repos.
    • Pierre-Marie: it is going to be harder to maintain the micromega plugin due to API unstability (branches or conditional compilation might be needed) Pierre argues it is minor in this case.
    • Fréderic proposed to discuss some more with Pierre for the most workable solution for him.
    • No clear decision on the way to go forward on this particular topic.
    • The discussion went on about the stdlib being out or in the main repo and the stdlib's status. Matthieu: this will require another dedicated time for discussion.

Participants

Matthieu Sozeau, Enrico Tassi, Frédéric Besson, Hugo Herbelin, Nicolas Tabareau, Pierre Roux, Pierre-Marie Pédrot, Théo Zimmermann, Andres Erbsen, Cyril Cohen, Yann Leray, Reynald Affeldt.