Minutes February 8 2023 - math-comp/math-comp GitHub Wiki
Participants: Enrico, Laurent, Pierre, Yves, Reynald
news: docker image for MathComp 1.16 are ready
- https://hub.docker.com/r/mathcomp/mathcomp/tags?page=1&name=1.16
- this completes the release
elpi for Coq 8.17
ET: to be started
sval
about - https://github.com/math-comp/math-comp/pull/964
- instead of a definition try to
- to permute both notations
- 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 inssrfun.v
- try to remove it from
#733
port to HB- ET: minor progress (lacking time)
- two problems with the documentation
- we want to use the output of HB.about
- 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
- Problem:
- two problems with the documentation
- 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
- or use
- 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
- NB: the documentation of
discussion should we have order structures on the relations (like Monoids in bigop.v) and not just on the types (like in ssralg.v)?
following a- 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 |
- https://github.com/proux01/math-comp/tree/hierarchy-builder-semiring
- some patches have been applied to reduce the compilation
- see the last commits
- HB commands take more time
- e.g.,
finalg.v
which is made mostly of HB commands
- e.g.,
- no big slowdown during the proofs
- memory?
- NB: runners are only 4GB