Coq Call 2024 05 07

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

Present: Andres Erbsen, Pierre Roux, Hugo Herbelin, Pierre-Marie Pédrot, Romain Tetley, Matthieu Sozeau, Gaëtan Gilbert, Théo Zimmerman, Yves Bertot

Topics

• Take formal decisions about CEP #83 [Pierre, 20 min]
• How to describe at best the organization of the "Coq team" on the web site? [Hugo, 5 mins, posing the basis of a discussion]
• Primitive projections again: which positive/negative simulations, which algebraic presentations, which optimized representations, which control of reduction, which disambiguation of names? (see Zulip) [Hugo 10 minutes + discussion time]

Roles

• Chairman:
• Secretary: Yves Bertot

Notes

Concerning CEP #83

There is agreement on repository split, but not on other parts of the discussion. On top of having a dual repository, a team of maintainers should be clarified and the decisions to be taken for other parts of the discussion should be taken by that team. For instance, the build of the stdlib can already be organized in several sub-packages, but the fare of these sub-packages will be chosen later.

Concerns are expressed about the dependency of some plugins in OCaml code with respect to vernacular code from the library. For instance, Micromega depends on the real numbers. It would be good that interfaces are clarified in the future, but this cannot be done in the short term.

A prototype already makes it possible to show that it works. The dual repository approah will be a trial, with a possibility to revert if too many difficulties arise.

About the composition of the maintainer team, Pierre Rousselin also volunteered. Concerning the animation of this maintainer team, there is the difficulty of avoiding spending too much time on details, while there is still a need to agree on the global vision.

Yves mentions that some funding has also been secured to help Robbert Krebbers discuss convergence with stdpp. Normally, there should be a low need for synchronicity between stdlib and coq-core, especially have stdlib always compatible with latest coq-core should make contributions easier.

With respect to comminication, it should be about making it easier to gather people who want to contribute, and ultimately enabling the convergence of the various libraries of the system.

There is no need for big announcements, but the information about how to contribute should be as clear as possible.

About the renaming and the next release

Version 8.20 will be named Coq-8.20.

Organization of the Coq team on the Web site

Hugo requests for clarifications about Matthieu's proposal for a larger committee of coordination.

Matthieu explains that the goal is to take into account the fact he himself does not have time to get involved full time and having this coordination committee is to help him

Theo adds that the move is also an opportunity to highlight the many teams that are included in the evolution of the Coq system.

Hugo has a request about including Paul-André, as a representant his Inria team on the topic.

Hugo wants to propose an alternative organization, Matthieu agrees to look at it.

Primitive projections

Projections are represented in three different ways. the consensus is that there should be only on. The unfolded status of projection should be removed (consensus), there is no objection against removing the "constant" status but not everybody is sure it will work (especially porting might be a problem). In Hugo' experiments, Incompatibilities appeared only on Unimath and Hott. Matthieu expects Iris to be dependent on the constant mode. Hugo thinks it would be good to keep ways to control reduction with respect to conversion, even if there is no constant. There should be a list of names, but not necessarily associated to delta.

Hugo has more long-term plans, one concerning eta (on which PMP, Gaëtan, and Matthieu express serious doubts) the second long-term plan is about using compact representation for positive records.