Minutes March 08 2023

Participants: Reynald, Cyril, Enrico, Thomas, Yves, Julien, Kazuhiko, Pierre

now that 8.17 is coming out, should we drop 8.15 in HB port? (would enable the use of reverse coercions)

• Yes
• MathComp is supporting at least two versions of Coq to allow for people to transition slowly
  • Nobody knows of a MathComp project stuck with an old version of Coq
• TODO: fix HB so that the names produced are better-looking
  • see https://github.com/math-comp/hierarchy-builder/issues/328

now that we have semirings, should we try declaring a semiring instance on nat?

• Pierre will try in the HB branch
• the two orders on nat (the one in ssrnat and the one in order) are not interchangeable
• there would be the same issue with the semiring instance on nat
• TODO: provide a small tactic to convert between goals?
  • in the form of an Ltac to change all the operators in the context

followup of last meeting discussion about being less strict on accepting contributions

• the change in policy needs to be made public
  • not in the contributing guide but rather as an announcement
• add a number of points as a checklist to the template for PRs?
  • should be made of trivial points
  • no more than ten checkboxes
  • using the items discussed during the last meeting might just worsen the situation
• there should be a list for the reviewer of the PR and for the creator of the PR
• TODO(short term): add a checkbox to link to the contributing guide
• TODO(long term): make the same knowledge available to the developer and the reviewer
• a linting tool is difficult to achieve

PR triaging for MathComp 1.17

• https://github.com/math-comp/math-comp/pull/944 has been fixed since the last meeting
  • but this is a draft PR
  • need a bit more time to be completed (in particular documentation)
• https://github.com/math-comp/math-comp/pull/934
  • TODO: Cyril and Reynald to meet [2023-03-10 Fri 10:30] for 30 minutes
• KS: should \max be in fun_scope rather than order_scope?
  • because it is a definition that takes a function
  • TODO: open an issue
• TODO(RA): check about min_fun/max_fun in MathComp-Analysis

oothm and semiring, help fixing it needed (blocks coq-elpi release for 8.17 hence AT for 8.17)

• AT = algebra tactics
• Enrico: this was fixed yesterday night
• Was it because of the semiring addition or was it here before?
  • Pierre: since the semiring addition, error related to the morphisms

Nix CI seems off on the HB branch

• look at the error message for 8.17 in https://github.com/math-comp/math-comp/pull/733:

  > File "./forms.v", line 136, characters 2-24:
  > Error: The reference GRing.isScalable.Build was not found in the current
  > environment.

• TODO(cyril): to investigate

Multinomials (at least remind and advertise there will be a meeting)

• poll: https://framadate.org/gNRLbYxxDxYQrYwq
• topic: several orderings on multinomials, this calls for a refactoring using monalg.v that defines monomials algebras
  • Cyril: multinomials was in a middle of a refactoring

do a sprint to put the documentation of MathComp 2.0 in order

• one week sprint
• two leaders to decide the protocol, framadate during May and June
• Enrico is not volunteering
• Reynald and Pierre volunteered

issue by Pierre:

• after an Open ring_scope and Open order_scope, 0 and 1 become top and bottom!
• TODO: open a PR about this problem
  • maybe have a new scope for people that rely on 0 and 1 being top and bottom