Minutes October 20 2021 - math-comp/math-comp GitHub Wiki

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
    • 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