Coq Call 2024 02 19

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

Topics

• Enlarging the coordinators team (Matthieu, 10min)
• Discuss about how to organize the (long-term) roadmap (Gaëtan, 10min)
• Proposition to talk about primitive projections: which positive/negative simulations, which algebraic presentations, which optimized representations, which control of reduction, which disambiguation of names? (see Zulip, Hugo 10-30 minutes)
• About reduction strategies (part of CEP #85, Hugo):
  • we may allow constructors in the transparency state to control iota-reduction, the same way as we can already control primitive projections reduction by name of projection?
  • removal of the user access to hnf?
  • better document the role of flags (e.g. is iota needed to trigger a Proj and is delta needed to trigger a Const unfolding, or only the transparency state matters?)
• How to make progress on #18397 (API of declare.ml). I need help about what to do to go in the good direction (Hugo, 5-15 minutes)
• Would it be worth to move Utf8.v to Init? (Hugo, 5 minutes)

Roles

• Chairman: PMP
• Secretary: Théo

Notes

• Matthieu proposes to not be the only one in charge of coordination. Proposal is for Yves, Nicolas and Théo to join the "coordination team". The Coq Team page would be modified to reflect this change. Idea to better display various teams in charge of component maintenance and their decision power on their components. Digression on maintenance of extraction component, stdlib component, etc.
• Do we need a meeting to work on the long-term roadmap? Physical WG proposed. We did not find a good timing for that, so instead we will do a weekly one-hour meeting on the roadmap. Matthieu is going to propose to go back to Tuesdays for the Coq Call, and to do the roadmap meeting before, at 3pm.
• Utf8 discussion. Not everyone likes Utf8, so putting it in Init would force it on people who don't want it (it would be used in printing by default). Digression on potential Pollack inconsistencies and actual inconsistencies because of Unicode. So, the conclusion is no. [Added Hugo: each UI should document how to enter unicode characters easily]
• declare.ml discussion. Lack of assignee, but the PR is not controversial. Pierre Roux will assign himself and merge. Related discussion on resolving the inconsistencies between Variable and Context and the possible incompatibilities resulting from this
• hnf discussion, given that this tactic does not perform head-normal-form reduction. Related discussion on PR #18580 and on the performance issues encountered by PMP in #18672. There are two algorithms, one for reduction and one for conversion. PMP's PR changed the conversion, but a proposal would be to change the reduction instead (user-visible improvement).