Minutes February 22 2023

Participants: Cyril, Enrico, Julien, Pierre, Reynald, Yves

question from last meeting about memory footprint:

• master: 0.71 GB
• hb: 1.57 GB
• hb+semiring: 1.73 GB

• measurement without parallelism
  • done with the command time
• Julien: do we have to optimize HB first to ensure that the slowdown can be eliminated in the future?
• Enrico: is it a peak or a constant increase?
• Cyril: why this increase for a structure that is not used?
  • Enrico: compilation of odd-order has been reported in an earlier meeting https://github.com/math-comp/math-comp/wiki/Minutes-November-16-2022

generalized additive and ring morphisms as well as matrices (and not just polynomials) in semiring branch:

• slowdown goes from 20% to 35%
• slowdown seems to mostly come from HB.instance lines
• compilation times (in s) [1]

• substructures not yet tested (although half of the work has already been done)
• it should be ok to push the change to the branch to enjoy the CI

PR triaging for MathComp 1.17 ?

• TODO(Reynald): look at PR #934 next week with Cyril
• About PR #944
  • do we really need to review new results as much as we review changes?
    • since new results are unlikely to break things
  • (this PR contains a backport from analysis (dependent fun, that was also in Abel in fact))
  • is it a question of the number of definitions w.r.t. the number of lemmas?
  • what about splitting_ahom which is long? could be reread and improved later
  • a few canonicals may require a bit of work when porting to HB
  • Enrico: why the - in the middle of line 202? /= should have the desired effect, maybe it is a bug
  • Reynald: is the do [suff ...] readable? should ?'s at line 104 be named?
  • Enrico: isn't the main criterion maintainability?
  • we should put issues w.r.t. master or TODOs in the code when merging instead of rebasing PRs
  • Yves: regular sprint code to deal with these issues?
• Similar problems with PR #207
  • Yves: What is left to do with this PR?
  • Cyril: this PR has already be cut into pieces and merged partially
• Cyril: we need to review what reviewers need to do get the PR through
  • first priority: documentation, definitions, notations, naming
  • second priority: consistent notations, meaningful lemmas, "completeness" of the set of lemmas
  • third priority: proofs (should at least look maintainable)
  • Yves: notations may be difficult to review sometime
  • Pierre: yet there aren't a lot of them
• have a changelog for each PR instead of a single changelog?
• have queues of PRs to avoid rebase when merging?

--

[1]

diff	hb	hb+semiring	file
-0.39	9.08	8.69	fingroup/action.v
-0.15	8.00	7.85	solvable/pgroup.v
-0.12	4.29	4.17	ssreflect/fintype.v
-0.09	8.32	8.22	solvable/center.v
-0.08	7.33	7.25	fingroup/fingroup.v
-0.05	1.34	1.29	ssreflect/eqtype.v
-0.04	1.44	1.40	ssreflect/fingraph.v
-0.04	4.13	4.09	ssreflect/finset.v
-0.04	5.13	5.09	fingroup/quotient.v
-0.04	5.29	5.25	ssreflect/bigop.v
-0.03	1.50	1.46	ssreflect/ssrnat.v
-0.02	0.07	0.05	ssreflect/ssreflect.v
-0.02	0.27	0.26	fingroup/all_fingroup.v
-0.02	1.41	1.39	solvable/commutator.v
-0.02	3.30	3.28	solvable/nilpotent.v
-0.01	0.57	0.55	ssreflect/all_ssreflect.v
-0.01	0.61	0.60	fingroup/presentation.v
-0.01	1.52	1.51	ssreflect/binomial.v
-0.01	2.07	2.06	solvable/gfunctor.v
-0.01	2.59	2.58	ssreflect/choice.v
-0.00	0.25	0.24	ssreflect/ssrbool.v
-0.00	1.01	1.01	ssreflect/div.v
-0.00	2.60	2.59	ssreflect/prime.v
0.00	0.04	0.04	ssreflect/ssrmatching.v
0.00	0.04	0.04	ssreflect/ssrnotations.v
0.00	0.07	0.07	ssreflect/ssrfun.v
0.00	1.09	1.09	ssreflect/finfun.v
0.00	1.20	1.20	ssreflect/tuple.v
0.00	2.00	2.00	fingroup/perm.v
0.01	0.41	0.42	ssreflect/ssrAC.v
0.01	1.94	1.94	ssreflect/path.v
0.01	4.19	4.20	ssreflect/seq.v
0.02	2.64	2.67	fingroup/automorphism.v
0.03	3.58	3.61	solvable/sylow.v
0.04	12.73	12.77	fingroup/gproduct.v
0.08	4.07	4.15	solvable/gseries.v
0.08	5.69	5.77	fingroup/morphism.v
0.10	1.78	1.88	ssreflect/generic_quotient.v
0.14	0.86	1.00	character/all_character.v
0.16	0.85	1.01	field/all_field.v
0.16	4.62	4.78	solvable/frobenius.v
0.17	0.62	0.78	solvable/all_solvable.v
0.18	52.97	53.15	ssreflect/order.v
0.26	5.54	5.80	solvable/alt.v
0.35	11.15	11.49	solvable/burnside_app.v
0.36	1.83	2.19	solvable/primitive_action.v
0.42	4.47	4.90	solvable/jordanholder.v
0.49	13.05	13.54	solvable/hall.v
0.61	4.26	4.87	solvable/cyclic.v
0.73	6.30	7.02	algebra/intdiv.v
0.84	9.54	10.38	solvable/abelian.v
0.90	2.43	3.33	algebra/all_algebra.v
1.26	3.73	4.99	field/cyclotomic.v
1.33	5.16	6.49	algebra/fraction.v
1.36	13.06	14.42	solvable/maximal.v
1.49	4.41	5.90	algebra/polyXY.v
1.61	13.06	14.66	algebra/interval.v
1.65	18.24	19.89	character/inertia.v
1.67	4.20	5.87	all/all.v
2.02	12.67	14.69	algebra/vector.v
2.23	7.41	9.64	solvable/finmodule.v
2.49	4.78	7.28	algebra/zmodp.v
2.75	12.05	14.81	character/vcharacter.v
2.77	13.61	16.38	algebra/ring_quotient.v
3.21	14.33	17.55	algebra/mxalgebra.v
3.31	9.35	12.66	algebra/polydiv.v
3.36	24.03	27.39	solvable/extraspecial.v
3.38	10.38	13.76	algebra/ssrint.v
3.58	14.94	18.52	character/integral_char.v
4.53	12.13	16.66	algebra/rat.v
7.97	10.59	18.56	algebra/mxpoly.v
8.18	11.53	19.71	field/separable.v
8.30	17.78	26.08	field/falgebra.v
9.07	28.10	37.16	field/galois.v
9.11	19.81	28.92	algebra/poly.v
9.35	30.95	40.30	character/character.v
9.58	18.75	28.32	field/algnum.v
9.77	31.58	41.34	field/algebraics_fundamentals.v
10.77	23.22	33.99	field/algC.v
10.93	9.30	20.22	character/mxabelem.v
11.41	36.87	48.28	character/mxrepresentation.v
11.89	32.25	44.14	solvable/extremal.v
13.10	31.33	44.44	character/classfun.v
15.89	17.41	33.29	algebra/countalg.v
16.33	56.28	72.61	algebra/ssrnum.v
17.25	33.37	50.62	field/fieldext.v
19.71	30.06	49.77	field/finfield.v
26.83	81.35	108.18	algebra/ssralg.v
27.57	17.30	44.87	field/closed_field.v
41.56	45.93	87.49	algebra/finalg.v
52.90	52.15	105.05	algebra/matrix.v