Minutes March 08 2023 - math-comp/math-comp GitHub Wiki

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

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

  > 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