Minutes November 18 2020 - math-comp/math-comp GitHub Wiki

Release

• milestone 1.12.0: new PR popped
• Cyril volunteered

mczify:

• unanswered question from Mickael Soegtrop, he proposed to make packages
• Coq 8.12 version does not have all the functionalities, but it works
• what are mc based developments using zify?
  • not that we know of
• Kazuhiko needs to tag the revisions to release

Meta issue, if we drop support for Coq 8.9

• warnings for undeclared scope could be attended
• but there are still non-convertible ambiguous paths in ssralg even though it's about proof irrelevant content (feature request to Coq)
• we can merge /[apply] /[swap] /[dup]
• we can use under

=> we drop support for coq 8.9

discussing various PRs

• size_merge_sort_push
• finmap cannot be merged one month from the deadline -> next milestone
  • pro: visibility, using it inside mc,
  • cons: two versions of finset, major breaking change, when they merge