Rocq Call 2026 05 12 - rocq-prover/rocq GitHub Wiki

Topics

  • Proposal and discussion on the organization of developments close to Rocq-core (i.e., micromega, equations, rocq-lsp, stdlib) (Nicolas T., 30min)

Roles

  • Chairman: Nicolas Tabareau
  • Secretary: Matthieu Sozeau
  • Attending: Enrico Tassi, Théo Zimmermann, Andres Erbsen, Pierre Roux, Pierre-Marie Pédrot, Yann Leray

Notes

How to deal with the official projects in the Rocq Prover Orgnization.

  • Théo: projects in the Rocq organization should be maintained by members the Rocq team (core + maintainers) and be kept under control of the Rocq team (not outside of the organization).

  • Nicolas: what should be the duty of the Rocq team w.r.t. projects in the Rocq organization ?

  • Théo: explicit the role and maintain a roadmap for each of these projects. Enrico and Matthieu agree.

  • Andres: what about deduplication? Should it be a goal of the roadmap? E.g. to state how it relates and is supposed to subsume other components functionality / replace them. Example of Equations/Function/Program.

  • Enrico: giving a clear message on what is supported, maintained and expected to evolve in the future and what will get only strictly necessary maintainaince is useful. Removes confusion for users.

  • Tabareau: what about dependency checking in practice, how to deal with multiple rocq versions for a given project e.g. elpi uses conditional compilation, Equations started using it and it seems the sanest way to go.

  • Enrico: synced releasing of all the projects in the Rocq prover organization should be easily doable.

  • Andres: how to support external projects outside of Rocq's CI.

  • Proposed policy by Pierre/Théo/Andres: reverse dependencies of any project in the CI should be in the CI.

  • Andres points to the different CI techs used in rocq-core and stdlib/math-comp/MetaRocq.

  • Enrico and Matthieu point to difficulties in using the nix toolbox and friction in doing updates.

    Might be too early to reuse the rocq-nix-toolbox for rocq's CI.

  • Théo points that it is a goal to have a single system for users to go to. Right now we provide rocq-nix-toolbox and the Docker images, which have only limited reverse dependency tracking.

  • Andres: there is an issue with the docker images and stdlib due to a pinned version issue.

  • Théo: there should be more tags to the docker images to select the stdlib version.

  • Andres: there should be a simple way for users to follow a common version for the packages released by the team.

  • Théo: proposes to sync the releases of the packages in the docker image and platform.

    Current process: please pick issues come much later than the rc release.

  • Andres: ask for a synced release of the rocq prover organization packages.

  • Théo: providing a canonical supported combination of Rocq packages at each release seems reasonnable, without forcing this as this only solution.

  • Andres: slight disgression about mathematical integers.

  • Enrico: agrees to move elpi to the organization.

  • TODO: think about other projects to be integrated.

  • TODO: summarize the expectations for projects in the Rocq Org, the maintainers and the release managment policy.

  • TODO: write roadmaps for each of the projects in the organization, and integrate them in the larger Rocq roadmap (to be freshened/detailed as well).

  • Reusing the setup to streamline releases of projects used by Enrico should help with the release of Rocq Prover organization packages.