Coq Call 2024 03 05

• March 5th (back to Tuesday! (IINM)), 4pm UTC+1 (Paris time zone offset)
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• CEP #83 about stdlib (Pierre Roux, Cyril Cohen, 25min)

Roles

• Chairman: Enrico
• Secretary: Enrico (+ Pierre?)

Notes

We only discussed the first item, and in particular two sub items:

• Qualify the stdlib (as in From XXX Require). Everybody was in favor of going in this direction, although XXX is not so clear, since the natural value for XXX would be Coq but that is in the process of becoming Rocq.
• Splitting the stdlib (see below)

Splitting

Many aspects were discussed with some confusion/entanglement between splitting stdlib from Coq and splitting the stdlib into subparts. Most of the discussion is about the former, mainly in the form of Mono-Multi repo models, although the CEP is also, maybe mostly, about the other.

• Motivation: (by Cyril) is to be able to use Elpi/Equations/Paramcoq in order to improve the stdlib. This is also the case if we want to promote to standard some parts of mathcomp (which uses Elpi, for example)

• Motivation: cut down compile time of Coq HH, PMP: compile time is not really an issue HH: there is a little development overhead at doing overlays for plugins like Elpi, Equations or Metacoq compare to working with them in a common directory

• Distribution: (Theo) the platform can serve as a mean to re-assemble bits into a thing called stdlib (now the platform has levels, core and extended, it could have one called std)

• Documentation: we don't have a way to aggregate the doc, that seems a requirement for the distribution of a fragmented std. (Andres) doc is not the main problem of the stdlib today, rather process (delay in PR).

• Technical issues raised:

  • Git modules can be used to aggregate the dev environment, but are ugly with little tooling
  • Monorepo is not well supported by github
  • Proposal of a mixed approach, submodules in Coq for Elpi/Equations/ParamCoq, so that the stdlib can stay where it is but use these

• The lack of proper tooling for both approaches was raised multiple times, as well as the need to find a solution with the tools that we have today.