Skip to content

Minutes February 8 2023

Jump to bottom Edit New page
Pierre Roux edited this page Feb 9, 2023 · 3 revisions

Participants: Enrico, Laurent, Pierre, Yves, Reynald

news: docker image for MathComp 1.16 are ready

elpi for Coq 8.17

ET: to be started

about sval

  • https://github.com/math-comp/math-comp/pull/964
  • instead of a definition try to
    1. to permute both notations
    2. put the second on in only parsing
  • the system should print the first one when there are two arguments
    • try to remove it from eqtype.v since it is duplicating in ssrfun.v

port to HB #733

  • ET: minor progress (lacking time)
    • two problems with the documentation
      1. we want to use the output of HB.about
      2. the hyperlinks of all the contents generated by HB.about are not in the code
        • Problem: coqdoc does not support having several things pointing to the same place
        • PR to coqdoc in progress that should go though but won't be ready in time
  • YB: Thomas could help
    • prototype within 15 days?
    • still, work on Search is happening in parallel
  • ET: first version of the documentation without the hyperlinks
    • or use coqdoc master to do the documentation for the first release
  • alpha-release does not need to be in sync with MathComp-Analysis
  • LT: to help for the documentation
    • NB: the documentation of ssralg.v was started

following a discussion should we have order structures on the relations (like Monoids in bigop.v) and not just on the types (like in ssralg.v)?

  • LT: about the order on monomials for grobner
    • would like to parameterize on another order with more properties (transitivity, irreflexive, well-founded, compatibility properties)
    • order notation not on the type but on the relation?
      • like the monoid laws in bigops
    • why is he the only one to have this problem?
    • ET: add another small hierarchy of orders wouldn't be a solution? ping Cyril or Kazuhiko

addition of semirings to HB port (where are the slowdowns?)

  • Per file timing (in s) with Coq 8.16 on my old laptop (total without semirings: 30min, with semirings: 36min (+20%))
diff HB HB+semiring file
52.95 80.07 133.02 algebra/finalg.v
28.66 29.30 57.95 field/closed_field.v
25.55 48.09 73.64 field/finfield.v
24.67 69.70 94.37 algebra/matrix.v
21.61 18.05 39.67 character/mxabelem.v
21.54 28.28 49.81 algebra/countalg.v
20.82 133.05 153.87 algebra/ssralg.v
16.23 59.16 75.39 solvable/extremal.v
15.93 53.02 68.95 field/fieldext.v
15.22 90.83 106.05 algebra/ssrnum.v
14.21 29.89 44.10 field/algnum.v
11.20 49.46 60.66 character/classfun.v
10.71 27.79 38.50 field/falgebra.v
10.36 18.86 29.21 algebra/mxpoly.v
9.91 29.08 38.99 algebra/poly.v
9.07 55.16 64.24 field/algebraics_fundamentals.v
8.92 35.49 44.41 field/algC.v
8.27 18.92 27.18 field/separable.v
7.57 20.73 28.30 character/vcharacter.v
6.56 52.27 58.83 field/galois.v
5.61 23.11 28.71 algebra/mxalgebra.v
5.44 20.42 25.86 algebra/ring_quotient.v
4.41 25.77 30.18 character/integral_char.v
4.30 18.59 22.89 algebra/rat.v
4.08 18.04 22.12 algebra/polydiv.v
3.60 6.88 10.47 algebra/polyXY.v
3.37 43.41 46.78 solvable/extraspecial.v
3.35 67.27 70.61 character/mxrepresentation.v
2.87 7.53 10.39 algebra/zmodp.v
2.66 16.14 18.80 algebra/ssrint.v
2.44 32.75 35.19 character/inertia.v
2.08 6.33 8.40 all/all.v
2.02 19.73 21.75 algebra/vector.v
1.70 53.91 55.61 character/character.v
1.66 12.08 13.73 solvable/finmodule.v
1.46 8.14 9.60 algebra/fraction.v
1.40 19.84 21.25 algebra/interval.v
1.02 3.52 4.55 algebra/all_algebra.v
1.02 17.38 18.40 solvable/abelian.v
0.84 6.38 7.22 field/cyclotomic.v
0.84 10.43 11.27 algebra/intdiv.v
0.69 7.37 8.06 solvable/cyclic.v
0.57 8.53 9.11 solvable/jordanholder.v
0.48 20.46 20.95 solvable/burnside_app.v
0.47 24.68 25.14 solvable/maximal.v
0.33 6.86 7.18 solvable/sylow.v
0.25 1.73 1.98 character/all_character.v
0.23 1.72 1.95 field/all_field.v
0.19 1.12 1.31 solvable/all_solvable.v
0.10 8.78 8.88 solvable/frobenius.v
0.09 2.95 3.04 ssreflect/generic_quotient.v
0.04 0.10 0.14 ssreflect/ssreflect.v
0.02 10.71 10.72 solvable/alt.v
0.00 0.13 0.13 ssreflect/ssrfun.v
-0.01 0.41 0.40 ssreflect/ssrbool.v
-0.01 0.08 0.07 ssreflect/ssrnotations.v
-0.02 0.10 0.07 ssreflect/ssrmatching.v
-0.03 2.50 2.48 ssreflect/eqtype.v
-0.06 3.63 3.57 solvable/primitive_action.v
-0.06 1.00 0.94 ssreflect/all_ssreflect.v
-0.06 0.59 0.54 fingroup/all_fingroup.v
-0.07 1.28 1.21 fingroup/presentation.v
-0.12 3.94 3.83 solvable/gfunctor.v
-0.16 2.18 2.02 ssreflect/tuple.v
-0.17 6.42 6.25 solvable/nilpotent.v
-0.20 2.08 1.88 ssreflect/finfun.v
-0.22 2.87 2.65 ssreflect/fingraph.v
-0.25 2.12 1.86 ssreflect/div.v
-0.28 3.02 2.74 ssreflect/binomial.v
-0.29 11.95 11.65 fingroup/fingroup.v
-0.31 3.05 2.74 ssreflect/ssrnat.v
-0.34 3.88 3.54 fingroup/perm.v
-0.36 2.81 2.44 solvable/commutator.v
-0.39 5.08 4.70 fingroup/automorphism.v
-0.39 3.88 3.49 ssreflect/path.v
-0.47 4.84 4.38 ssreflect/choice.v
-0.50 7.87 7.37 solvable/gseries.v
-0.56 5.21 4.66 ssreflect/prime.v
-0.72 7.50 6.79 ssreflect/finset.v
-0.78 8.14 7.37 ssreflect/seq.v
-0.78 10.56 9.79 fingroup/morphism.v
-0.87 9.19 8.32 ssreflect/bigop.v
-0.87 7.87 7.00 ssreflect/fintype.v
-0.99 22.72 21.73 fingroup/gproduct.v
-1.25 2.02 0.76 ssreflect/ssrAC.v
-1.36 15.61 14.25 solvable/pgroup.v
-1.86 25.91 24.05 solvable/hall.v
-1.96 17.98 16.02 fingroup/action.v
-2.02 16.50 14.48 solvable/center.v
-2.13 11.31 9.18 fingroup/quotient.v
-6.29 82.61 76.33 ssreflect/order.v
Add a custom footer

Clone this wiki locally