Attendees : Reynald Affeldt, Cyril Cohen, Pierre Roux, Kazuhiko Sakaguchi, Quentin Vermande

now only waiting for an infotheo release, then nixpkgs will be done and backporting on OPAM (which is lacking CI)

• Currently, ssralg.v is about 7.7k lines long. We will probably need to split it soon.
• The change is not urgent, unless someone wants to add more structures very soon, e.g., unitSemiRingType, semiFieldType, unitSemiAlgType, and Euclidean domains (#742).
• How should we split the file, e.g., creating a new file dedicated to unit(Semi)RingType and below? What should be the names of the new files?

• will need to add new structures, not even counting the ones currently in CoqEAL
• no urgent need, except maybe discrete rings (from CoqEAL) to do tensor products for differential geometry
• how to restructure the Theory and so on modules? should it be done before or after the split?
• could take inspiration from the ssrnum.v restructuring
• would loose the GRing.... qualification, except maybe using NES
• we should test more NES, so that the day it work we can implement (and test it) in Rocq
• should we test on a leaf (like Analysis) first? why not
• names of files splitted from ssralg.v? structures without/with multiplicative inverse?
  • algebra.v? (structures without multiplicative inverse) maybe not a good name for a file
  • three components: commutative algebra (Z-modules, ring, modules), multiplicative inverse, third component?(characteristic and decfield?)
  • keep the morphisms in same files as structures (structures are almost useless without morphisms)
  • -> split in three

• needed for polynomial evaluation (need to commute coefficients and variables)
• could we have a more general condition?
• could be an application of Quentin's work (set subtypes recurring issue)
• needs more discussion in Lyon

Also missing the join of ring morphism and order morphism (order preserving ring morphisms)

• documentation is scattered in Rocq website, mathcomp, analysis, opam?
• we should organize a new mathcomp school (last one was in 2022 with buggy MC2 initial version)
• need some standardization (standard library, common between MC and stdpp for instance, including unifying framework between typeclasses and canonical structures)

• Reynald to {impr,rem}ove the page and announce it

Cyril