Minutes December 1 2021

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

• https://github.com/math-comp/math-comp/pull/808 made me think that we may (or may not) want to ad a Number Notation in rat, to be able to write numerical constants as 42 or 3.14 in rat_scope (Pierre (but I won't be available on December 1st))
  • Cyril:
    • desirable indeed, and also for ring
  • Reynald: isn't it the role of %:R?
  • Cyril:
    • this could alleviate inefficiencies (due to hnf, due to discrimiante) in rat
  • TODO: experiment with a number notation in rat (and also in ring)
    • Pierre: will do a draft PR (note added after the meeting)
  • Kazuhiko: the good thing with _%:~R (for int) is that it is an additive function (or a ring morphism if the codomain is a ring). I think we should rather include GRing.natmul in the interface of zmodType
  • Cyril: MathComp relies a lot on 1%:R is 1 and putting natmul in the interface would break this property
• status of https://github.com/math-comp/docker-mathcomp/issues/12
  • because of stdlib-shims, coq-elpi requires at least OCaml 4.07 https://github.com/coq/opam-coq-archive/pull/1826
  • not fixable on Enrico's side
  • we are left with the option of upgrading the docker image with OCaml > 4.05
  • TODO: ping Erik
  • NB: during the last release Cyril add to fix the following file https://github.com/math-comp/docker-mathcomp/blob/master/images.yml whose fix is not yet reflected in the documentation
  • other refererences:
    • https://github.com/coq-community/docker-coq/issues/30
    • https://github.com/coq/opam-coq-archive/blob/master/released/packages/coq-elpi/coq-elpi.1.11.2/opam
• HB and OOthm
  • Enrico:
    • odd-order-theorem compiles with the HB-version of MathComp but is not fast (half an hour)
  • Cyril:
    • why does it not work with Coq 8.13?
      • see the CI ouput here https://github.com/math-comp/hierarchy-builder/actions/runs/1523253447
    • NB: mathcomp becomes twice as slow (+ 10 minutes), odd-order was 12 minutes
  • Reynald:
    • minor fix following to the port of finmap to hierarchy-builder
  • Cyril:
    • discussing the remaining issue related to ssrnum with HB
  • further discussions on the performances of the CI
    • see https://github.com/math-comp/hierarchy-builder/runs/4374642904?check_suite_focus=true
  • Enrico: how does Coquelicot use MathComp?