Attendees: Yves Bertot, Alessandro Bruni, Cyril Cohen, Pierre Roux, Kazuhiko Sakaguchi, Quentin Vermande

postponed

We agreed to rename GRing.exp to GRing.pown What about expn in ssrnat and expz in ssrint Naming inconsistencies with natmul, intmul, natexp (monoid), expgn (fingroup) Kazuhiko proposes to use mul(r|g)(n|z) and exp(pow?)(r|g)(n|z), see comments here and here Pierre worries that the change may be too large for 1 PR (we have time since we just released). Kazuhiko argues that it should be done in the same release. Alessandro recalls that the motivation was to make things uniform with MathComp Analysis. We should discuss it again with Reynald

Kazuhiko is porting is Docker CI to Nix on stablesort. Being able to specify the list of combinations of versions to test and specific commits for each version is nice. There is an issue when testing Rocq 9.1.0, where multiple versions of Rocq get installed. Pierre and Kazuhiko discuss a few technical issues.

Consistent naming convention:

• all_*.v for re-exportation files (all.v is dangerous because there may be conflicts without warning) We need to choose between all_num.v and all_num_theory.v and keep the directory names consistent.

PR1504 is ready, but we may want to rename alg_theory to alg.

As of now, ssralg.v re-exports nmodule.v, is that correct? Same question with theory modules re-exportation? Kazuhiko thinks we should not re-export files, but re-export theory modules (so that the user only has to import one module and get all the reverse dependent ones). If we split order and re-export theory modules, we can use Order.Theory everywhere and import the previous one. This would need to be documented. The content of a sub-library with a all.v exportation file should be documented either as a README.md file or in the all.v file.

Next meeting on January 7th. Pierre volunteers.