Agenda of the December 10th 2018 meeting 9h30 to 12h30 - math-comp/math-comp GitHub Wiki

Agenda of the December 10th 2018 meeting 9:30 - 12:30

  • Status of the next meeting, which should happen in February, and date and location should have been picked by then, cf https://framadate.org/k3esao1uTosdxIMO
  • news from the libraries, current live projects, longer term ones : status, goals, merge plans,…
    • Demo of new ssreflect features (should be release in June 2019, and usable in released mathcomp from December 2019)
    • Demo of near by Cyril
  • Making a new release? 1.7.2? 1.8.1? Discuss API change policy (e.g. what exactly do we guarantee by increasing x, y or z, in a x.y.z version of mathcomp)
  • Animation of the community and changing/confirming a privileged medium of interaction between user and dev (following up #244)
  • current pull requests / bug reports
    • PR for integration of finmap into mathcomp (should be available in December)
  • if times allows: documentation/website/wiki/book/gallery

Minutes:

  • Next meeting: we fix February 2019 in Sophia-Antipolis, but we let people update the doodle and fix the date by mail later
  • ssr/ipats2:
    • `[^ … ]` -> bug: should honor `Arguments .. : rename`
    • `()` -> remove?
    • TODO: (next PR?) remove exception for `move=> []`
    • `/3/` non existent -> error
    • `ltac:(…)` -> check scope bound variables
    • `/ltac:x [ ]` -> dispatch and not case
  • near:
    • `∀ x, \near ..` + `near=> x` + `near: x` to hide an existential
    • abstract/near: merge?
  • release:
    • GG thinks that using semantic versioning is hard because even minor changes (renaming) break things
    • we talk next time about making the release
  • documentation:
    • website: kill ssr2 website (TODO: Maxime)
    • communication channel that is easier than the mailing list, that is very technical
    • we could open a gitter and collect FAQ
    • who devotes time to that channel?
    • doodle for discussing this, 2h (TODO: Cyril)
  • PR:
    • CI, do things on on gitlab.com (TODO: Cyril)
    • other PR (finmap, permutations) discussed later then the authors will be ready
    • `_ : Type` merge + changes (TODO: Cyril)
⚠️ **GitHub.com Fallback** ⚠️