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).