Minutes May 19 2021 - math-comp/math-comp GitHub Wiki
Participants: Pierre Roux, Pierre-Yves, Reynald, Enrico, Kazuhiko, Cyril, Christian
- Summary of Call about adding metadata for search:
- Coq devs are in agreement that the feature is okay, but there is no agreement on implementation details
- parallel discussion in Inria formal math working group to hire an engineer
- Discussion: Should there be a rule about draft PRs (not) being milestoned?
- Consensus: maintain the invariant that only PRs that are ready for review are milestoned
- Discussion on specific draft PRs that were milestoned:
- PR501: stays in the 1.13.0 milestone, Cyril agrees to make it ready for review
- PR259:
- adding finmap to mathcomp is required before multinomials can be merged
- as long as there is no (other) use within mathcomp, both can stay outside of mathcomp
- conclusion: demilestoned, needs more work