Participants: Reynald Affeldt, Cyril Cohen (chair), Pierre roux, Enrico Tassi, Quentin Vermande (secretary)

Mathcomp engineer

• Tasks to be executed ** Readable doc. We want a tool (not specific to mathcomp) that interacts with Coq's API to retreive informations (may this is too much). ** changelog ** back/formardport files from MCx to MCy/between branches/from a user repo to the main repo ** general porting, things (e.g. computable maths) to MC, coqeal to Trocq ** maintenance, e.g. fix warnings ** write issues on github
• Period? We would like a permanent contract. There will be some training time.
• Profile? User. Someone able to criticize and merge non-strategic code.
• Shared with Coq? To discuss with Coq project's coordinators. Which status? MC engineer or Coq engineer? Coq engineer would be weird if we want to assign specifically MC tasks

Teams

• What are the needs? Is it important that some do not have all permissions?
• Coq: 3 levels: no permissions, permissions on labels, merge permissions
• MC: parallel universes, 8 teams ** CAD does not make sense anymore ** The only project it makes sense to distinguish is analysis ** Temporary teams for particular projects (e.g. finmap coding sprint) ** remove CI, CAD, move the reporters to the core team ** give sensible permissions in each repo, e.g. missing permissions to core in HB

#311 ([meta-issue] Cleanup using features of Arguments):

• Remove nosimpl in favor of simpl never.
• PR1162 removes them, so we will be able to close this.

Problems with the release process

• The CI is very slow, every manipulation costs a lot of time
• Release process too long and difficult, e.g. backporting PRs, updating the doc, change a boolean flag somewhere in the config file
• Putting the release notes in the release is absurd
• The CI has a lot of false negatives, there is always something that does not work and require a little modification

PR 1162 (Droping support for Coq 8.16 and 8.17)

• We merge (and drop Coq 8.16 and 8.17), we do not use nosimpl anymore
• We keep nosimpl to be backward compatible for the users
• Side note, in HB, every projection should be declared simpl never (issue 411)

Universe issue while porting validspd to MC2

To be investigated offline.

Finmap coding sprint

• We might need the cs hook in order to do the infrastructure of finset with coq-elpi.
• If Georges finished his prototype we can go on.
• Meeting on the 07/02 replaced by a mini finmap sprint to do the infrastructure with coq-elpi.