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)
• implementation plans for namespaces, CEP #25 (HH, 5-10 min, if Enrico and/or Cyril are there)
• reflection on CEP #73 (more complicated match), useful for small inversion and for the parametricity plugins (HH, 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)
• removal of recovery mechanism of camlp5/coqpp #17876: seems that sometimes it will not be possible to have code working with two consecutive versions of parent libraries (Pierre, 10-15 min, less urgent, can be postponed)

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.