Coq Call 2024 02 05

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

Topics

• CI runner shortage (Gaëtan, 15min)
• scheme registration names (https://github.com/coq/coq/pull/18299 and https://github.com/coq/coq/pull/18549) (Gaëtan, 15min)
• would we try to set Set Printing Projections by default? (Hugo, 5-10min)
• taking a decision w.r.t. the constant associated to a primitive projection (Hugo 5-15min)
  • remove it, eta-expanding any expression referring to a not-applied-enough projection, possibly experimenting using notations to hide the eta-expansion, counting on beta-conversion to identify the applied projection with the applied eta-expansion of the projection
  • give it a proper status and inform the kernel that it is always defined so as to be able to identify the full application of the Const with the corresponding Proj node whenever needed
• finding a name for the variant of simpl that never unfolds "simpl never" constants (#18581, Hugo 5-15min): simpl+, strict simpl, or also simpl with never/simpl with fully_never as particular case of a general form of simpl with database-of-constants, ...

Roles

• Chairman: Matthieu
• Secretary: Matthieu

Notes

• Inria CI having issues, throttling creations of VMs, resulting in many more timeouts on our CI runs. The team managing the runners hope to bring more runners soon. In the meantime we turned 2 bench machines into CI runners. Not a permanent solution. We could use scaleway runners as the platform does, Romain is investigating. PLEASE AVOID DOING FULL CIs, UNLESS BEFORE MERGING in the meantime.

• Schemes: we will try to give a uniform naming + an alias scheme for the current naming.

• Primitives: leaning towards removing the comp constant and using eta expansion

• simpl never not really never... Why not an attribute to Arguments instead, or a break (small incompatibilities apparently) ?