Agenda of November 14th 2019 meeting 10:00 to 11:00 - math-comp/math-comp GitHub Wiki

Agenda

  • next mathcomp release?
  • installation instructions (reported from previous meetings)
  • followup of the last meeting
    • finmap status
    • PR 270 status
    • documentation for naming conventions of structures and modules (incoming PR on CONTRIBUTING.md)

Minutes

Release

  • Coq 8.10 is out, should we release?
  • Enrico: takes 3h top, maybe good time since we are in a stable situation
  • GG: a finmap related change should go in before, something about general induction, eg elim: x {2}x (ltnSn x); it could break on sets built on finmap since there are more occurrences of the set. We could avoid breakage with an helper lemma. GG does the PR.
  • Plan: we add the lemma for general induction then we release, RM are GG and Yves
  • RM postpone PR and issues from milestone 1.10 to 1.11

Finmap

  • last meeting we thought about a generalization/factoring involving generic quotients. Still to be integrated.
  • GG: there is an open design question for predicates on a finite domain

PR270

  • progress report: 1 renaming to do before merge
  • some improvements can be made afterwards
  • let's merge just after the release

Documentation of naming conventions

  • merged

Next fortnightly meeting is scheduled Nov 27 10AM do discuss finmap