Coq Call 2023 11 21

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

Topics

• any hope to get #18164 merged before branching? (Pierre, 10 min)
• will #18032 ever be merged (Pierre, 10 min)
• 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)
• using ltac2 in stdlib? (Gaëtan, 15min)

Roles

• Chairman: Nicolas Tabareau
• Secretary: Yves Bertot

Notes

• We start a discussion on Ltac2: the conclusion is to move on with more adoption of Ltac2, even if it means adding a dependency of stdlib on Ltac2. There is a small problem with dune but stdlib is already a special case for dune so this should be fixable (Emilio volunteers some help)
• Pour la PR #18164 it should be mergeable. We really aim to have it before the RC release. (the 8.19 branch will be created on Nov. 27) the RC will be created on Dec. 11.
• #18032 was merged as a conclusion of the discussion
• concerning #17876 Pierre Roux made a comment to the effect that math-comp and math-comp analysis are really impacted by this PR, because of similar notations used in both developments.

Diverse questions

• There is a discussion on #18193. We agree to use the keyword "Attributes" for attributes that are valid for a whole file. We check for the agreement of Hugo and then merge.

• Theo had promised a description for a change of process concerning the description of releases (so that the Release Manager takes care of that part). Theo foresees that he will not be able to deliver in time for this release and asks that Matthieu takes the task of describing the release this time as before. This is agreed.

• Nicolas announces that a page has been created for the meeting in Nantes here

• Theo has teaching obligations that prevent from having meetings on Tuesdays at 4pm (Paris time). Yves suggests to move temporarily to Mondays. All present agree. We need to check with a wider audience about this, but next meeting will probably happen on Monday.