Minutes November 16 2022 - math-comp/math-comp GitHub Wiki

Participants: Cyril, Enrico, Julien, Laurent, Mohit, Reynald, Yves

  • release managers for 1.16

    • alpha release of mathcomp 2.0 for the winter school
      • might not be a public release
      • release managers: Enrico, Cyril
      • a Coq platform is being built for the winter school
    • after December 13 for 1.16:
      • release managers: Reynald, Cyril

  • RFC: https://github.com/math-comp/math-comp/pull/934

    • use MV for the division?
    • it would be nice to be able to search look for either the long and/or the short identifier(s) of a symbol
    • ler_pdivl_mulr -> ler_pZlMr? (nope for the Z) ler_pMVMr is horrible (Laurent) ler_pVlMr? (Yves) ler_pVl_Mr? (Yves)
    • shall we give up when there is _div and a short identifier? (and keep long identifiers in this case)
    • how long will warning stay? at least two releases...
    • laurent: this PR solves inconsistencies between natural numbers and order.v, that's good
    • cyril: uniformizing ssrnat.v and ssrint.v was a smaller initial goal, we should maybe split the PR in two (obvious renamings + less obvious ones) with the goal of uniformizing
      1. the renamings that are necessary
      2. consensual ones
      3. the trickier ones
      1. and 2. to integrate in the next release

  • port to HB #733

    • about adding semirings: timings to compile OddOrder (make -j1 on my laptop):

      • without semirings: 2074.59user 18.59system 35:21.32elapsed
      • with semirings: 2209.54user 13.78system 37:09.35elapsed So, that seems about 6% slower.

    • Cyril was fearing twice the time, we should however try to understand where it comes from, odd-order is the one using the most the hierarchy because of Galois' theory

    • Enrico: we have tools to profile line by line, expect the slow down to happen in the second part of the proof

    • analysis port still in progress (almost done ?)

      • we made the product topology go through
      • HB branch in wait for a rebase on top of masters

    • remainings TODO/FIXME

+++ algebra/mxalgebra.v
+(* FIXME: to be understood. If you remove card, then there is no speedup *)
+Lemma card_GL_predK n p : #|'GL_n.-1.+1(p)| = #|'GL_n(p)|. Proof. by []. Qed.
Enrico Tassi      2021-04-19 19:08 work around inefficiency in mxalgebra
~~> keep the FIXME for now?

https://github.com/math-comp/math-comp/blob/hierarchy-builder/mathcomp/algebra/mxalgebra.v#L2556

  • Enrico: this lemma was not here before, used a few lines below, in the old proof this lemma was not needed, the proof still goes though without the lemma, the speedup is less than 1s, guess: at the time it was taking certainly more time
  • the lemma should be put inside the proof, the comment is misleading
  • Cyril: if moved inside the proof, the speed up is not as good, the rewrite takes more time because the context is longer
  • live inspection of what's behind the GL notation, rewriting with .-1.+1 relies on the fact that n is greater than 2, conjecture: it is unrelated to HB because there is no inference at play, but not sure because it was really fast before... we still don't know what in HB is causing the slowdown, there is an inference at play with finite fields, (looking at GLgroup), time lost in the unification of the arguments, debugging using Set Debug "unification"
  • in the end the slowdown comes from a non trivial unification which becomes worse with flat packed classes
Pack T {| mixin1 n p1; ... ; mixinn n pn |}
=
Pack T {| mixin1 n.-1.+1 p1'; .... |}

where pi is such that (mixini n pi) reduces to (.. n.-1.+1 ..) and pi' is such that (mixini n.-1.+1 pi') reduces to (.. n.-1.+1 ..).

Since there are n mixins, instead of 1 mixin an 1 class, the new code has to perform the hard problem multiple times. In the actual problem there is also an unknown, to be filled in, but passing it explicitly does not completely remove the per problem.

The hack is to perform the unif problem on a smaller term, once, making the .-1.+1 bubble up, and rewrite everywhere, so that Coq has an easier time figuring out that the unitRing whatever of the maxtrix exists since the dimension is not 0.

It is unclear if HB could be instrumented to bubble up these syntactic size constraints so that the hard work is shared once per class, instead of once per mixin.