Agenda of the April 23rd 2019 meeting 9h30 to 12h30 - math-comp/math-comp GitHub Wiki

  • Discussing release model:
    • should we backport to 1.8.1 or refrain from merging pr for further milestones?
    • should we even have a 1.8.1 (backward compatible with 1.8.0)?
  • Roadmap for merging multinomials
  • Documentation

Minutes

Release model

  • Enrico (by mail): release every 1 year, sooner if more content
  • Georges: release minor versions for bugfixes, release every 6 month, and sooner if more content. What about development that goes to ssreflect, ssrbool and ssrfun? Should we put them in the stub files and in Coq at the same time.
  • Cyril: I have already asked Enrico, and we thought about putting them in stub files.

Conclusion:

  • Release every 6 month / 1 year, and sooner if more content
  • We put additional content to ssreflect, ssrbool and ssrfun both in Coq and mathcomp

CI and big changes

  • Georges: how to make the CI pass on breaking changes
  • Maxime: Coq uses overlays
  • Cyril: Erik has documented it here https://github.com/math-comp/math-comp/wiki/How-to-add-overlays-for-PRs and it takes into accounts some problems we have encountered.
  • Georges: There could also be a strategy of putting aliases for old names to new names, but does not like it
  • Cyril: Kazuhiko did this for the order branch, and we should remove them before merging
  • Georges: agrees

Avoiding issues with CHANGELOG

  • Georges: How to avoid having old PR put changes into the wrong section of the CHANGELOG? Recommends having one file for released CHANGELOG and another one for unreleased.

Various discussions on PR

we discussed the following PRs:

  • #302 Georges will review,
  • #203 Maxime will ping people,
  • #270 Kazuhiko and Cyril will adjust the final details before calling for reviews,
  • #328 Yves will do what he can and leave the rest to someone else and
  • #259 the PR will be merged without dependent finmap, which can be dealt with in a second round.

Multinomials roadmap

Merge of dependencies:

  • merge finmap (with or without dependent finfun)
  • merge order
  • merge near

Multinomials

  1. (Cyril) define alg_lift from https://github.com/hivert/Coq-Combi/blob/Shuffle/theories/Dendri/shufflealg.v define monom_lift. https://github.com/math-comp/multinomials/issues/19#issuecomment-417678133
  2. (Cyril) define eval as the compose of alg_lift and mon_lift (Cyril) define multinomials compositions using "lift"
  3. (PY) erase the beginning of mpoly and import monalg instead.

CHECKPOINT in September

  1. try to to adapt the rest of mpoly, heavily parallelisable:
    • order monomials
    • theory of eval
    • theory of composition
    • homogenous polynomials
    • theory of symmetric polynomials
  2. Extension to polynomials that are symmetric on a subset of variables

Documentation

Let's plan a special meeting. The participants may include Cyril, Assia, Georges, Marie, Reynald, Enrico...

Next meeting

Doodle https://framadate.org/5vp8jZ1embtJpLT8