Minutes June 16 2021 - math-comp/math-comp GitHub Wiki

Participants: Pierre, Enrico, Christian, Kazuhiko, Reynald

Reminder: 1.13.0 to be released by the end of the month. Time to check the milestone?

• PR 503:
  • Christian: It is a minor change that causes major breakage in four-color, postponed, turn into a draft PR
• PR 501:
  • Cyril: will be complete and ready to merge by the end of next week
  • Christian: need to adapt the title
  • we can postpone the not so needed changes and use the new syntax when it fits
• Issue 698:
  • Cyril: will be complete and ready to merge by the end of next week
• PR 752:
  • Cyril: to come back to it but this should be light
  • Christian: questioning the naming of big_rev_mkord
• PR 740:
  • Kazuhiko: pushed his changes
• About HB NFI:
  • Christian: the new HB master refuses to compile NFI
  • Make NFI a warning in the next HB release?
• PR 689:
  • to be closed by 740
• PR 440:
  • Kazuhiko: constants provided by ssralg should be qualified by GRing Module, lemmas have to be exported by defining aliases, a new lemma should be accompanied by an alias to be added in the Theory module
  • Enrico: unit_key need not be exported, right?
  • Kazuhiko: to reorganize ssralg.v like order.v but later, for 1.13 just compare tag 1.12 and check

There is a request from Florent Hivert to have a list of external contributors somewhere. It probably also makes sense to update the list of authors.

• Enrico: AUTHORS.md is outdated
• Reynald: put the list of names in the changelog?
• Enrico: go back in time to update the changelog, announcements message can be found online:
  • 1.8, 1.10, 1.11 are on Coq Club
  • 1.5, 1.6, 1.7, 1.9 are in the ssreflect ML
  • 1.12 is on discourse