attending: Reynald Affeldt, Yves Bertot, Alessandro Bruni, Cyril Cohen, Pierre Roux, Enrico Tassi, Quentin Vermande

current state of release 2.4.0

• released
• packages in OPAM: main packages merged, some issue to check with finmap
• Nix: released real-closed, fourcolor and gaia, will need to release coqeal, check graph-theory, need to ask for a ssprove release (probably better to wait for analysis 1.10), waiting for Analysis 1.10 and new tarjan release

makefile for math-comp.github.io is outdated feel free to improve it

#1256 structures with one operation

• remaining failure with jasmin due to extraction: agreement? to remove jasmin from mathcomp CI for now until the issue is fixed on their side
• needs to fix a few last things but almost done

#1169 preorder

• squashed and rebased
• needs to recheck that we are not erasing recent changes in order
• need to check performance

#1338 ssrnum split and ordered {n,z}modules

• cut into multiple PRs:
  • splitting ssrnum
  • adding extended reals
  • generalize from zmodtype to nmodtype
  • adding new structure for pseudo-norm on zmodtype (better maps informal math practice)
• may need to squash and redistribute commits

package mathcomp-order

1. do the package
2. rebase preorder (#1169 preorder)
3. further split remaining of order

• solution: deprecate ssreflect package and split it into mathcomp-base and mathcomp-order PR doing the PR
• name can be improved until the PR is merged
• RA: basics looks better than base
• basic and basics used in mathlib and hott, better use base to not confuse with other libraries
• -base has a few occurences among debian packages (r-base, ros-base,...)
• or root ? (YB: content not elementary enough)
• core ?
• let's pursue the discussion in the PR

unifying the algebraic and bigop hierarchies

• intern to revive the HB branch attempting to merge the two hierarchies
• should be done on top of PR #1256 structures with one operation
• once done, reconcile work on relorder branch (work by Kazuhiko with Xavier Allamigeon, Pierre-Yves Strub and Quentin Canu on unpacked classes for order (subject is the relation instead of the type)), need to find where this branch is as it could serve as an inspiration for bigop hierarchies

monoid and comoid files name (in PR#1256)

• -> add_monoid and mul_monoid
• no, monoid.v (current monoid.v with multiplicative notation) and nmodule.v (current comoid, additive notation)
• size of files is reasonnable (about 1300 lines), no need to further split them

PR triage postponed to next time

chair for next meeting

• -> Cyril

announcing sharing day for April 30th

• -> Quentin