Minutes January 26 2022 - math-comp/math-comp GitHub Wiki

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

• Selecting a mathcomp version for the Coq platform (cf this zulip thread). As of now I (Cyril) do not think we released the 4CT and OOT for mathcomp 1.14.0 yet (nor mathcomp 1.13.0 AFAIK).

  • 1.14 was selected
  • odd order and four color's CIs fixed
    • there were broken by mathcomp 1.13 but no released were done
    • the lack of tag ni four color prevents the update of Nix
    • TODO: Cyril to tag and Pierre to do the opam packages (edit: Pierre: I'll update the Nix ones too)

• Discuss potential migration of MathComp project to coq-community

  • Shall try to move some packages?
  • What are the reasons not to move a package?
  • Difference between packages using or not using coq-community tools?
    • We are already using the Nix tools from coq-community
    • We can use meta.yml but not to generate opam files
  • The change of urls would be the main reason
    • URLs in papers, in CIs, in old packages
    • need to change upstreams
  • Setting of email notifications in github?
  • Move the package, doubling it and leave a warning behind?
    • https://docs.github.com/en/repositories/creating-and-managing-repositories/transferring-a-repository
    • One needs to receive right to transfer to the target community
  • Try one and see how it goes
  • Let the webpage and the mathcomp behing (they are not Coq)
    • maybe not analysis (too big)
    • maybe not finmap or bigenough (not leaves)
    • move Tarjan?
  • TODOs:
    • Assia do the experiment with Apery and report (maybe not for the next meeting)
    • four-color would be a good candidate (Yves to be taking care of this one?)
    • both covers different sets of test points

• Number notations for rat, int, ring #841

  • have a number notation to be able to write say 42 instead of 42%:R in ring_scope
    • as of today it would be a nat by default
  • the difficulty was to update the CI
  • we need to first merge the overlays
  • Add number notation for rat
  • 3.14%Q is ok, (-2)%Q is fine
  • how many %N added? how many %R removed?
  • x + -(2%Q) and x + (-2)%Q are not the same, x + -(2)%Q and x - 2%Q are the same
  • what happens when we will add semi-rings?
  • two files touched in solvable and extrema, do we really need to open the ring scope?
    • because it uses zmodule-group compatibility layer?
    • TODO: Pierre to try