Coq Call 2023 11 14

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

Topics

• roadmap update (Gaëtan, 10min)
• what/how to retain things in CI when removing deprecation requires a lot of work (e.g. #18164 ) (Pierre 15-20 min)
• fiat crypto remaining failures (Gaëtan, 10min)
• stabilization of user syntax for library file deprecation/warning (PR #18193, currently: command Library Attributes #[...] + new attribute information="...") (Hugo, 5-10 min)
• discussing potential fixes for https://github.com/coq/coq/issues/18281, an issue with primitive projection constants in conversion (Rodolphe & Janno, 10-15min)

Roles

• Chairman: Nicolas Tabareau
• Secretary: Matthieu Sozeau

Notes

• Roadmap update.
  • change of name: waiting for lawyers before we plan a freeze and renaming
  • no difficult blocking points identified on any of the short term projects.
• fiat remaining failures: more input needed to analyse the issue.
• feedback on the CI by Pierre Rousselin. Emilio points out that tooling could greatly help with the problems encoutered (notable Coq universe to do large-scale changes).
• Primitive projection vs constant issue by Janno: no easy way around the bug. Pierre-Marie proposes getting rid of the compatibility layer and rather eta-expanding on the fly to avoid this issue. But the opaque constants also are used to gain performance on the user side. We'll have a specific meeting on this issue (starting by a channel on Zulip).