Coq Call 2024 04 23

• April 23rd, 4pm UTC+2 (Paris time zone offset)
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• CEP #83 (Pierre Roux, 25 min)
• CEP #86 (Andres Erbsen, 25 min)

Roles

• Chairman: Gaëtan
• Secretary: Théo

Notes

CEP 83 (boost stdlib development / split stdlib into another repo)

• CEP 83 may be an enabler for CEP 86.
• We need to see if we are on agreement on the motivations:
  • Disagreement on the amount of things that are no longer standard, but agreement that there are parts that are no longer standard.
  • Agreement that we cannot drop the stdlib because it is very much relied on.
  • Agreement that stdlib is not very much alive and not attractive compared to the rest of Coq / Coq ecosystem.
  • Agreement that there is an intimidation factor, but not necessarily for technical reasons.
  • Agreement that the teams maintaining Coq and the stdlib are mostly disjoint.
• The main controversial point is whether the current stdlib library should keep a special status:
  • Keeping the coq package depending on coq-stdlib is problematic from the point of view of Pierre and Cyril because it hides the rest of the Coq Platform to some users.
  • Andres prefers the dependency to remain, but not a strong no to removing the stdlib. In particular, he is worried about divergence in the ecosystem if different people use different libraries.
  • Cyril would also like a stdlib that everyone uses, but thinks we are pretty far from achieving that.
  • Pierre Rousselin adds that ease of usage should be kept in mind (takes the example of MathComp which is pretty hard to use compared to stdlib).
  • Théo proposes to consider separately the dual repo approach and the change in the package dependency structure. Pierre Roux reminds that there are two main objectives of making it easier to contribute to the stdlib and clarifying to the users what parts they should use and what parts they shouldn't use.
  • Cyril reminds that his main argument for dual repo is to rely on more external libraries / plugins in the stdlib.
  • Equation is mature and could be moved into the Coq repository.
  • Andres would like to keep the bar high to add dependencies on the stdlib, and then the dependencies could just as well be merged into Coq.
  • Cyril thinks that some external packages are mature enough to be relied upon, but there could be social issues preventing a move to the Coq repository. Furthermore, they provide layers of abstraction that protect against internal changes to Coq.
  • Gaëtan explains that the Coq repository is not meant to integrate every plugin, even the good ones.
  • Cyril says that we should ask Enrico what his opinions are about merging Coq-Elpi into Coq (for instance, would that hinder a quicker release cycle).
  • Pierre Rousselin highlights that the stdlib team will be very small. There seems to be an agreement on increasing the team, but not clear how to communicate on this.
• Stdlib split could happen (no strong opposition), but renaming from stdlib to roots is disagreed on. We will take a formal decision to do the split at the next Coq Call. The rest of the points in the PR (renaming, multi-package split, etc.) will be delayed until there is a stdlib WG and draft of stdlib roadmap (see last point below).

CEP 86 (making contribution to the stdlib less intimidating)

• Could be applied regardless of the split.
• Establish context-dependent guidelines for reviewing PRs. We should have more consistency on the reviewing guidelines. Théo is very enthusiastic about this.
• Having a path forward for imperfect additions. But Théo remarks that we have to take into account the cost of future maintenance, especially for additions that could be considered fragile.
• Compatibility policy: we need to clarify the policy for more flexibility, in particular we could skip deprecations if there is a clear upgrade path that allows to be compatible with two subsequent versions of Coq.
• We should make sure that PRs are not delayed too long because of unmerged overlays -> clarify the CI policy.
• New contributor advocate (based on Andres's experience when being a new contributor). coqbot could send a comment to new contributors encouraging them to call upon this person for any help or intervention (including in the case of a lack of reviews).

Overall, we need a stdlib WG and a stdlib roadmap and ensure consistency of the contributions with this roadmap. Discussion on whether to do a restricted or open call for participation to this WG.