Rocq Call 2025 04 15 - rocq-prover/rocq GitHub Wiki

Topics

  • call for Stdlib maintainers and contributors (Pierre, 20 min) https://hackmd.io/@LRv6jptJQiaWq01NSRp9QA/SJ7zAuFpJg
  • Future of Nix + Rocq (Théo, 20 min):
    • rename and officialize the Nix Toolbox/migrate to Rocq Prover organization? (also rename the Zulip channel)
    • evolve list of maintainers to reflect reality?
    • populate list of Nix packagers?
    • add Nix guides next to opam guides on https://rocq-prover.org/docs/using-opam?
    • migrate Rocq repo to use Nix Toolbox?
    • status of recommending Nix Toolbox for RDCT (Reverse Dependency Compatibility Testing)?

Roles

  • Chairman: Matthieu Sozeau
  • Secretary: Pierre Rousselin
  • Attending: Cyril Cohen (second half of meeting), Pierre Roux, Théo Zimmermann, Guillaume Melquiond, Gaëtan Gilbert

Notes

Rocq-call 25/04/15

Tue Apr 15 17:08:06 CEST 2025

Call to contributors for stdlib (Pierre Roux)

https://hackmd.io/qHwpTDpmTvyoelTtmwZAFA

It should be good to have maintainers of other popular libs (stdpp, mathcomp, extlib, ...) in the stdlib team.
People with experience with designing libs are very welcome.
TZ: Maybe list the different ways and levels of contributions
Goal: in June organize a visio call to launch development (to be scheduled with interested people)
MS: maybe in conjunction with Rocq'n share
Guillaume Melquiond: the call for contribution should be more practical about how to contribute,
it is also too long, we may add a TL;DR
Pierre Roux: main idea is that the stdlib is in this state for historical reasons, we want to revive it
TZ: summary with "there was no team dedicated for several years, we now want one and have a dedicated repository"
GM, TZ and PR agree that the context could be shortened
Why join? Present it as a good experience.

  • vision
  • people we need (1 person of each library, ...)
  • tasks/kinds of contributors Pierre Rousselin: spend some time to polish the call today/tomorrow

Remove the "make the stdlib standard again" (very bad joke nowadays)

Nix (Théo Z)

nix toolbox to rename
suggests to migrate it to rocq-prover to make it an official rocq-prover project,
like already planned for docker images and docker-opam-action

  • change the maintainer list of the nix toolbox (Pierre Roux, Vincent, Cyril more active)
  • if it's an official project of rocq-prover, the maintainers can be part of the rocq teams on the website

Mathieu Sozeau : agrees to make it part of rocq-prover, add doc in website at the same level as opam installation
TZ : indeed, add nix-toolbox in the website with doc more tutorial like, if it's not done before rocq'n share, I can work on it then
TZ: there is a default.nix inside the rocq repo with some jobs in the CI, remove this default.nix (redundant with nixpkgs and outdated) and the nix jobs in the CI and replace it with nix-toolbox, with some GitHub actions tests (minimal set, don't duplicate all reverse dependency tests already done in gitlab CI)
Cyril: already a flake (more or less up to date, based on nixpkgs) in rocq repo, keep it
issue : for the moment, nix-toolbox only supports github actions, not the gitlab ci, so better keep our current gitlab CI setup for RDCT (reverse dependency testing) for now

Cyril :

  • maybe migrate the toolbox to flake (could be done "easily" by using flake as a wrapper to the current toolbox)
  • there is duplication of work between the platform and the nix-toolbox (picking a curated list of package versions)
  • there are 2 tools to work with nix and opam : opam-nix and opam2nix

TZ: maybe appimage generated by nix could become the binary for linux (in replacement of abandonned snap, would be made easier by rocq now being a single binary)

A new engineer will work on the platform but then maybe could help with the nix-toolbox.

Should we recommend the nix-toolbox for reverse-dependency testing ?
yes, should Write a doc
Maybe during the rock'n share event ?

packaging teams (TZ)

Added teams in rocq-prover for people packaging rocq

  • opam packaging (ask Karl and other current maintainers of opam repo if they wants to join)
  • nix packaging
  • debian packaging
  • ... make visible these kinds of contribution
    be able to tag these teams with e.g. @rocq-prover/packaging
    It would help release managers to contact packagers.

(end of official meeting here, Guillaume and Matthieu leaving)

Longer discussion about Stdlib call

Cyril

  • would be better to setup a roadmap/governance/main technical choices (use of modules / canonical structures / type classes / HB...) before doing the call, otherwise high risk for the call not to be very appealing
  • about technical choices: keeping modules won't get us very far / won't scale, good indications that an HB/elpi based solution could cover both the needs for math (à la mathcomp) and PL (à la stdpp)
  • will be a need for codevelopment with Rocq itself (improve Search for instance, to be able to provide instantiated results (e.g. looking for lemmas about nat should provide lemmas about semirings))
  • looking at mathlib, good genericity seems key for success (even mathcomp is kinda basic in its lowest levels compared to it)
  • having a less basic lib may not be ideal for teaching purposes? should the Stdlib be a teaching tool? in practice when teaching we tend to "rebuild" step by step the standard things

questions about dependencies of Stdlib that should be officially supported

Decision: let Cyril lead a roadmap writing effort in the coming weeks/months and discuss it at a forthcoming Call, wait for that roadmap before doing any open call