Minutes March 22 2023 - math-comp/math-comp GitHub Wiki
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
https://github.com/math-comp/math-comp/issues/892#issuecomment-1471642279
adding example(s):- 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
- NB: in general, we do not want to cut, say,
- Nobody has been assigned the task for now
https://github.com/math-comp/math-comp/pull/934 (renaming long suffixes)
progress report onexprzpMzl
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 ofp
- not sure:
- use
Z
for the division?- TODO: use
MV
for the division
- TODO: use
BLR
ok because we see it as a groupeqrNLR
ok also
- use
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