Minutes March 22 2023

discussion on strategy for rebasing

Conclusion:

• squash the PR using hierarchy-builder
• cherry-pick MathComp commits one by one on top of the squashed PR
  • preserve the invariant that each commit compiles

Discipline from now:

• master -> branch V1
• PR hierarchy-builder -> branch V2
• a commit on a branch should be backported to the other

find a date for the mathcomp 2 sprint.

• Reynald and Pierre to meet on Tuesday to make a doodle

adding example(s): https://github.com/math-comp/math-comp/issues/892#issuecomment-1471642279

• Idea by Michael:
  • create a repo with examples to attract users
  • this is reminiscent of a previous discussion about a gallery/showcase
• ask Laurent who has many examples in his mathcomp-extra
• Yves: we have been working on an example using finite types
• Cyril: put together the examples of the schools
• Laurent: also has an example in French (Le Monde)
• small files might be good for examples
  • NB: in general, we do not want to cut, say, ssralg.v into pieces though
• Nobody has been assigned the task for now

progress report on https://github.com/math-comp/math-comp/pull/934 (renaming long suffixes)

• exprzpMzl maybe not a good idea
• the followings are ok:
  • normCDeq, lter_pdivlMr, in_segmentDgt0Pr
• should we give up on the following?
  • https://github.com/math-comp/math-comp/blob/47ed7ee3d762fe122290c031f565f73ee49e881b/CHANGELOG_UNRELEASED.md?plain=1#L124-L173
  • TODO: no, but use _p instead of p
• not sure:
  • use Z for the division?
    • TODO: use MV for the division
  • BLR ok because we see it as a group
  • eqrNLR ok also

discussion about the scope discipline and order displays, particularly with extended reals

• c.f., the discussion in math-comp/980 (time permiting, this is maybe more an Analysis point as extended reals are still there)
• postponed to MathComp-Analysis meeting