Minutes May 18 2022 - math-comp/math-comp GitHub Wiki

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

• state of the HB port: #733
  • CI goes through for Coq 8.13--8.15 but not for coq-dev
    • includes odd-order, CoqEAL, etc. see this comment
    • no blocking issue
    • Cyril can make the CI goes through with Nix, Pierre will try
  • we cannot port mathcomp-analysis yet
  • Cyril:
    • the blocking issue for mathcomp-analysis is harder to solve than thought
    • there is a pattern that is not handled by HB
      • problem: the source and the target of the norm operator are the same for absolute value
      • numDomain and normedZmodule in mathcomp (ssrnum.v)
    • numDomain has a norm that goes from the carrier to itself
    • normedZmodule has a norm and a parameter such that the norm might not go to itself
    • original motivation: share the theory of both norm operators
    • is it still a good idea in the context of HB?
    • Assia: why not having a mixin for norms and use if to define numDomain and normedZmodule?
      • Cyril: in mathcomp 1.x there was a trick to avoid defining one more intermediate structure in the hierarchy. In HB this common mixin is defined as such and inference during one of the uses of this mixin is the missing feature
    • see ssrnum.v line 175
    • normedZmodule should be understood as a first step towards an R-module with scalars, the parameter needs to be a partially ordered Z-module
    • problem summary: a mixin has parameters (genuine parameter or other mixin), the problem occurs when a parameter is a mixin that depends on another mixin
    • minimal example
      • problem: local canonical instances cannot be declared in Coq
    • solutions:
      • the creation of local canonicals in a future version of Coq
      • implementing a coq-elpi elaboration based on section variables, section definition, and section canonicals,
      • changing the design pattern of HB to defer the problem to TC resolution and/or coq-elpi clauses,
      • separating the absolute value and the norm which means change notations for norms in analysis and adding (propositional) equalities between them when applicable. (This last solution does not solve the core problem in HB though)
• lra (and nra and psatz): PR (and questions about large constants in nat)
  • we should soon get lra for mathcomp
  • large constants represented with natural numbers are still problematic
    • there is a Coq limit at 5000
    • Yves: can one change the bound specifically for mathcomp?
    • Kazuhiko: support larger constants by pre-processing?
    • performance bottleneck is in reification (the Coq parser)
    • decision: not really a problem, don't do anything (at least until someone really complains with a use case)
  • see example in PR