Minutes February 23 2022 - math-comp/math-comp GitHub Wiki

Participants: Reynald, Assia, Christian, Cyril, Enrico, Laurent, Pierre, Yves

discuss packaging discipline #851
- current strategy is ok
- it may cause some issue with constraint solvers (as pointed to by Kazuhiko)
agenda of migration to coq-community
- everything went well with the migration of Apery
  - need files for CI and opam
    - Appery was already using coq-community templates
  - transfer ownership
    - ask all authors their agreement (best effort)
- Georges fine with moving the 4ct, Yves to do the migration
- Cyril: having everything in one organization is a way to say that a set of packages is consistent
- see https://coq-community.org for an organized list of packages according to topics
  - in the future, add a category for MathComp?
  - how are badges attributed?
- Christian:
  - coq-community is rather for long-term maintenancem
  - maybe not that many actively developed projects (well, there is VST)
- Cyril: primary objective is optimizing engineering about the CI
Nix CI is currently broken for Coq master (but master remains tested on gitlab CI)
- the problem seems to be on the coq-community side
- Cyril hinting at a tentative solution
  - a dependency to OCaml needs to be made explicit, Cyril to do a blind PR but would maybe need to hand over to Theo
dropping support of Coq 8.11 and 8.12 to merge #841, #842 and #832? (number notations for ring, int and rat)
- seems to be ok
- Coq 8.12 had a number of problems (for which there was a patch-level anyway)
- Enrico: the objective of maintaining compatibility with 2-3 versions was to make transition easier from one version to another
Enrico and Cyril: say a few words about reverse coercions (coq/coq#15693)?
- goal: get rid of phantom types and, e.g., avoid the use of curly brackets in MathComp's notations
- will simplify HB and thus MathComp 2.0
- Yves: it would be nice to have an overlay for users to see the difference