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

• revive https://github.com/math-comp/math-comp/pull/709
  • original problem: some delay before a PR is taken in charge, it was a tentative solution, now recruiting more people is a more likely solution
  • Reynald: we have been more reactive recently but Cyril is spending much time
  • Yves: I am afraid that people wouldn't find legitimate to declare themselves in a codeowners file
  • Cyril, Christian: we do not need to do the review alone
  • Assia: codeowners could be the one to decide assignees
  • Yves: the role of the assignee is essential procedural, isn't it?
  • Enrico: notify a different number of people according to the file (say 10 for ssreflect.v, 2 for character.v)
  • Laurent: shouldn't this meeting be used to find reviewers/assignees? Cyril: this should be the exception
  • Laurent: let's experiment the codeowners file?
  • Conclusion: we'll experiment but move the assignments of people to directories to Zulip
• the status of the CI failures for multinomials and coqeal (eg. #781) (CD)
  • Pierre: for multinomials, problem with native; for coqeal, problem with Nix
  • Laurent: problem with timeouts, Pierre: change the solver?, Cyril: that should come from the coq-community templates
  • Enrico: we should try opam 2.1 to enjoy optimizations, TODO: ask Erik.
  • the solution should be transparent to other people
  • the error marked as a bigenough one was actually a problem with native compilation
  • Bertot: where does the complexity comes from? Nix? dune?, Cyril: there is a sanity check on the Nix side that helps, Laurent: complexity may come from the multiplication of tests
• fixing a release date? (CD)
  • tentative date: November 2
• I (Kazuhiko) am porting apery to MathComp dev (see math-comp/apery#3 and math-comp/apery#4) and have observed several performance issues with rat. For example, rewrite addr0 and congr (_ * _)%R can be significantly slower than before. I guess that interlocking rat operators made computation (unification, conversion, and normalization) slower. Is there anything we can do on the MathComp side?
  • // can cause exponential slowdown because of hnf, examples are reported with the PR, we should maybe revert the PR?
  • there are actually two recent PRs about rationals
    • interlocking: https://github.com/math-comp/math-comp/pull/766
    • gaia: https://github.com/math-comp/math-comp/pull/798 　+ Enrico providing information about reduction machines (compute, lazy) but hnf is a different part of the code
  • Cyril observed that hnf duplicate code despite a let
  • should discriminate be implemented using some lazy strategy?
  • TODO: ask Maxime, open an issue on Coq?
• If it is a proper subject for this meeting (I've been invited by Cyril to join), I (Florent Hivert) would like to integrate my development (Coq-Combi see https://github.com/hivert/Coq-Combi) as a side project of Math/Comp.
  • pros and cons? is it just increased visibility?
  • core members get push access, you also get caching from Nix
  • use coq-templates to produce packages https://github.com/coq-community/templates ?
  • added to the math-comp hierarchy by transferring ownership