Minutes January 12 2022 - math-comp/math-comp GitHub Wiki

Participants: Reynald, Assia, Christian, Cyril, Enrico, Karl, Kazuhiko, Pierre, Yves

  • Discuss the release process and timing in light of the changed Coq and Coq Platform release processes. See CEP 52 and the discussion at coq-community/reglang#40
    • timing release for the coq/mathcomp/platform
    • CD: we want to release before the platform
    • KP: pointing at the faster pace that would imply
    • ET (> CD): should we synchronize with the Coq release?
    • CD: release the known working version or make a release for the purpose of the platform?
    • ET: how painful is it to release MathComp?
    • CD: release process not that bad (3 hours with two people), the difficult part is cleaning the milestone
    • ET: force release put pressure on the users
    • KP: waiting also put pressure
    • CD: too long release cycle forces users to wait for their changes to appear and forces them to keep a copy
    • YB: is it just a matter of deciding at each release or to have a general rule?
    • ET: it depends on the release
    • CD: the previous version of MathComp would still be working
    • ET: communication the intent asap could be enough
    • AM: how to communicate?
    • KP: sync with the Coq release
    • YB: release candidate period for Coq?
    • KP: in general, one month
    • CC will be one of the release manager for the next release
    • CC: the current changelog is quite short, not sure these things are blocking
    • YB: we should follow a short release policy
    • ET/CC: minor release (in content) major release (in version number) set for wednesday next week
  • Providing contribution perspectives to MathComp users and improving the organization maintenance. See Issue 831
    • KP: already discussed by Theo and CC in previous meeting, interested in making users use the templates in coq-community, mathcomp is an organization in itself
    • CC: ways to be more inviting for contributors, guide in writing
    • KP: goals is to make contributions easier
    • AM: we are lacking man-power and are willing to attract contributors, mathcomp's github was created before coq-community
    • KP: coq-community has laxer standards, we want to have a big archive for publicity
    • CC: most projects in the mathcomp hierarchy should be in coq-community, maybe even mathcomp, have coqbot do merges?
    • ET: do all projects have webpages?
    • KP: we do not have yet good automation for this
    • CD: the mathcomp organization is big enough to stand alone
    • KP: no barrier to hold the mathcomp webpage on coq-community
    • CD: coq-community provides help to do updates, it provides examples and templates
    • KP: new templates on the way
    • AM: discuss next week if we want to migrate some projects
    • YB: there is a taxonomy of projects (linked to a paper, active maintenance or not)
    • KP: invite Theo or KP to work on the templates
  • number notations for rat, int, ring (Pierre (I'll may be 10 to 15 minutes late))
    • PR: to be able to write 42 instead of 42%:R
    • ET: should be doable in the vernacular
    • PR: only for rat, for ring we need ocaml
    • rescheduled to the next meeting