Porting to HB

[gares]

This Pull Request is about porting the hierarchy of hand declared algebraic structures to the language of hierarchy-builder.

Rules for contributing to the documentation of this PR:

• Tick the boxes down here when:
  • the file is taken by you to work on its documentation,
  • when it is complete (changelog included).
• Add your commits here (no force push)
• All commits you push must compile.

Tasks:

• Use the graph of MC files with live info about this PR in order to pick your next task (the dependency graph is generated by this branch which is slightly broken to maximize parallelization from where we stand)
  • blue nodes are taken by someone 🚧
  • green nodes are ported
    • solid green background means finished
    • yellow background mean compiles ✅
• A file containing no Structure and no Canonical should just work and requires no doc update.
• A file with Canonical but no Structure requires using HB.instance instead but no doc update.
• A file containing Structure requires doc update.

Progress:

• countalg.v finished (9 Structure, 153 Canonical)
  • 🚧 countalg.v taken
  • ✅ countalg.v compiles but needs more work
• finalg.v finished (11 Structure, 358 Canonical)
  • 🚧 finalg.v taken
  • ✅ finalg.v compiles but needs more work
• fraction.v finished (0 Structure, 52 Canonical)
  • 🚧 fraction.v taken
  • ✅ fraction.v compiles but needs more work
• intdiv.v finished (0 Structure, 4 Canonical)
  • 🚧 intdiv.v taken
  • ✅ intdiv.v compiles but needs more work
• interval.v finished (1 Structure, 26 Canonical)
  • 🚧 interval.v taken
  • ✅ interval.v compiles but needs more work
• matrix.v finished (0 Structure, 96 Canonical)
  • 🚧 matrix.v taken
  • ✅ matrix.v compiles but needs more work
• mxalgebra.v finished (2 Structure, 17 Canonical)
  • 🚧 mxalgebra.v taken
  • ✅ mxalgebra.v compiles but needs more work
• mxpoly.v finished (0 Structure, 8 Canonical)
  • 🚧 mxpoly.v taken
  • ✅ mxpoly.v compiles but needs more work
• polydiv.v finished (0 Structure, 2 Canonical)
  • 🚧 polydiv.v taken
  • ✅ polydiv.v compiles but needs more work
• poly.v finished (0 Structure, 89 Canonical)
  • 🚧 poly.v taken
  • ✅ poly.v compiles but needs more work
• polyXY.v finished (0 Structure, 5 Canonical)
  • 🚧 polyXY.v taken
  • ✅ polyXY.v compiles but needs more work
• rat.v finished (0 Structure, 44 Canonical)
  • 🚧 rat.v taken
  • ✅ rat.v compiles but needs more work
• ring_quotient.v finished (6 Structure, 55 Canonical)
  • 🚧 ring_quotient.v taken
  • ✅ ring_quotient.v compiles but needs more work
• ssralg.v finished (27 Structure, 149 Canonical)
  • 🚧 ssralg.v taken
  • ✅ ssralg.v compiles but needs more work
• ssrint.v finished (0 Structure, 29 Canonical)
  • 🚧 ssrint.v taken
  • ✅ ssrint.v compiles but needs more work
• ssrnum.v finished (8 Structure, 201 Canonical)
  • 🚧 ssrnum.v taken
  • ✅ ssrnum.v compiles but needs more work
• vector.v finished (3 Structure, 56 Canonical)
  • 🚧 vector.v taken
  • ✅ vector.v compiles but needs more work
• zmodp.v finished (0 Structure, 27 Canonical)
  • 🚧 zmodp.v taken
  • ✅ zmodp.v compiles but needs more work
• character.v finished (2 Structure, 13 Canonical)
  • 🚧 character.v taken
  • ✅ character.v compiles but needs more work
• classfun.v finished (0 Structure, 58 Canonical)
  • 🚧 classfun.v taken
  • ✅ classfun.v compiles but needs more work
• inertia.v finished (0 Structure, 5 Canonical)
  • 🚧 inertia.v taken
  • ✅ inertia.v compiles but needs more work
• integral_char.v finished (0 Structure, 1 Canonical)
  • 🚧 integral_char.v taken
  • ✅ integral_char.v compiles but needs more work
• mxabelem.v finished (2 Structure, 11 Canonical)
  • 🚧 mxabelem.v taken
  • ✅ mxabelem.v compiles but needs more work
• mxrepresentation.v finished (3 Structure, 85 Canonical)
  • 🚧 mxrepresentation.v taken
  • ✅ mxrepresentation.v compiles but needs more work
• vcharacter.v finished (0 Structure, 10 Canonical)
  • 🚧 vcharacter.v taken
  • ✅ vcharacter.v compiles but needs more work
• algC.v finished (0 Structure, 89 Canonical)
  • 🚧 algC.v taken
  • ✅ algC.v compiles but needs more work
• algebraics_fundamentals.v finished (0 Structure, 0 Canonical)
  • 🚧 algebraics_fundamentals.v taken
  • ✅ algebraics_fundamentals.v compiles but needs more work
• algnum.v finished (0 Structure, 21 Canonical)
  • 🚧 algnum.v taken
  • ✅ algnum.v compiles but needs more work
• closed_field.v finished (0 Structure, 0 Canonical)
  • 🚧 closed_field.v taken
  • ✅ closed_field.v compiles but needs more work
• cyclotomic.v finished (0 Structure, 0 Canonical)
  • 🚧 cyclotomic.v taken
  • ✅ cyclotomic.v compiles but needs more work
• falgebra.v finished (3 Structure, 61 Canonical)
  • 🚧 falgebra.v taken
  • ✅ falgebra.v compiles but needs more work
• fieldext.v finished (1 Structure, 138 Canonical)
  • 🚧 fieldext.v taken
  • ✅ fieldext.v compiles but needs more work
• finfield.v finished (0 Structure, 39 Canonical)
  • 🚧 finfield.v taken
  • ✅ finfield.v compiles but needs more work
• galois.v finished (1 Structure, 40 Canonical)
  • 🚧 galois.v taken
  • ✅ galois.v compiles but needs more work
• separable.v finished (0 Structure, 0 Canonical)
  • 🚧 separable.v taken
  • ✅ separable.v compiles but needs more work
• action.v finished (1 Structure, 29 Canonical)
  • 🚧 action.v taken
  • ✅ action.v compiles but needs more work
• automorphism.v finished (0 Structure, 5 Canonical)
  • 🚧 automorphism.v taken
  • ✅ automorphism.v compiles but needs more work
• fingroup.v finished (1 Structure, 16 Canonical)
  • 🚧 fingroup.v taken
  • ✅ fingroup.v compiles but needs more work
• gproduct.v finished (0 Structure, 28 Canonical)
  • 🚧 gproduct.v taken
  • ✅ gproduct.v compiles but needs more work
• morphism.v finished (3 Structure, 14 Canonical)
  • 🚧 morphism.v taken
  • ✅ morphism.v compiles but needs more work
• perm.v finished (0 Structure, 23 Canonical)
  • 🚧 perm.v taken
  • ✅ perm.v compiles but needs more work
• presentation.v finished (0 Structure, 0 Canonical)
  • 🚧 presentation.v taken
  • ✅ presentation.v compiles but needs more work
• quotient.v finished (0 Structure, 14 Canonical)
  • 🚧 quotient.v taken
  • ✅ quotient.v compiles but needs more work
• abelian.v finished (2 Structure, 8 Canonical)
  • 🚧 abelian.v taken
  • ✅ abelian.v compiles but needs more work
• alt.v finished (0 Structure, 6 Canonical)
  • 🚧 alt.v taken
  • ✅ alt.v compiles but needs more work
• burnside_app.v finished (0 Structure, 24 Canonical)
  • 🚧 burnside_app.v taken
  • ✅ burnside_app.v compiles but needs more work
• center.v finished (0 Structure, 7 Canonical)
  • 🚧 center.v taken
  • ✅ center.v compiles but needs more work
• commutator.v finished (0 Structure, 4 Canonical)
  • 🚧 commutator.v taken
  • ✅ commutator.v compiles but needs more work
• cyclic.v finished (0 Structure, 4 Canonical)
  • 🚧 cyclic.v taken
  • ✅ cyclic.v compiles but needs more work
• extraspecial.v finished (0 Structure, 1 Canonical)
  • 🚧 extraspecial.v taken
  • ✅ extraspecial.v compiles but needs more work
• extremal.v finished (2 Structure, 4 Canonical)
  • 🚧 extremal.v taken
  • ✅ extremal.v compiles but needs more work
• finmodule.v finished (0 Structure, 27 Canonical)
  • 🚧 finmodule.v taken
  • ✅ finmodule.v compiles but needs more work
• frobenius.v finished (0 Structure, 0 Canonical)
  • 🚧 frobenius.v taken
  • ✅ frobenius.v compiles but needs more work
• gfunctor.v finished (4 Structure, 14 Canonical)
  • 🚧 gfunctor.v taken
  • ✅ gfunctor.v compiles but needs more work
• gseries.v finished (0 Structure, 0 Canonical)
  • 🚧 gseries.v taken
  • ✅ gseries.v compiles but needs more work
• hall.v finished (0 Structure, 0 Canonical)
  • 🚧 hall.v taken
  • ✅ hall.v compiles but needs more work
• jordanholder.v finished (0 Structure, 8 Canonical)
  • 🚧 jordanholder.v taken
  • ✅ jordanholder.v compiles but needs more work
• maximal.v finished (2 Structure, 7 Canonical)
  • 🚧 maximal.v taken
  • ✅ maximal.v compiles but needs more work
• nilpotent.v finished (0 Structure, 8 Canonical)
  • 🚧 nilpotent.v taken
  • ✅ nilpotent.v compiles but needs more work
• pgroup.v finished (0 Structure, 9 Canonical)
  • 🚧 pgroup.v taken
  • ✅ pgroup.v compiles but needs more work
• primitive_action.v finished (0 Structure, 1 Canonical)
  • 🚧 primitive_action.v taken
  • ✅ primitive_action.v compiles but needs more work
• sylow.v finished (0 Structure, 0 Canonical)
  • 🚧 sylow.v taken
  • ✅ sylow.v compiles but needs more work
• bigop.v finished (4 Structure, 35 Canonical)
  • 🚧 bigop.v taken
  • ✅ bigop.v compiles but needs more work
• binomial.v finished (0 Structure, 0 Canonical)
  • 🚧 binomial.v taken
  • ✅ binomial.v compiles but needs more work
• choice.v finished (1 Structure, 5 Canonical)
  • 🚧 choice.v taken
  • ✅ choice.v compiles but needs more work
• div.v finished (0 Structure, 0 Canonical)
  • 🚧 div.v taken
  • ✅ div.v compiles but needs more work
• eqtype.v finished (0 Structure, 5 Canonical)
  • 🚧 eqtype.v taken
  • ✅ eqtype.v compiles but needs more work
• finfun.v finished (2 Structure, 1 Canonical)
  • 🚧 finfun.v taken
  • ✅ finfun.v compiles but needs more work
• fingraph.v finished (0 Structure, 2 Canonical)
  • 🚧 fingraph.v taken
  • ✅ fingraph.v compiles but needs more work
• finset.v finished (0 Structure, 13 Canonical)
  • 🚧 finset.v taken
  • ✅ finset.v compiles but needs more work
• fintype.v finished (0 Structure, 6 Canonical)
  • 🚧 fintype.v taken
  • ✅ fintype.v compiles but needs more work
• generic_quotient.v finished (3 Structure, 26 Canonical)
  • 🚧 generic_quotient.v taken
  • ✅ generic_quotient.v compiles but needs more work
• order.v finished (9 Structure, 501 Canonical)
  • 🚧 order.v taken
  • ✅ order.v compiles but needs more work
• path.v finished (0 Structure, 0 Canonical)
  • 🚧 path.v taken
  • ✅ path.v compiles but needs more work
• prime.v finished (0 Structure, 1 Canonical)
  • 🚧 prime.v taken
  • ✅ prime.v compiles but needs more work
• seq.v finished (0 Structure, 4 Canonical)
  • 🚧 seq.v taken
  • ✅ seq.v compiles but needs more work
• ssrAC.v finished (0 Structure, 1 Canonical)
  • 🚧 ssrAC.v taken
  • ✅ ssrAC.v compiles but needs more work
• ssrbool.v finished (0 Structure, 0 Canonical)
  • 🚧 ssrbool.v taken
  • ✅ ssrbool.v compiles but needs more work
• ssreflect.v finished (4 Structure, 6 Canonical)
  • 🚧 ssreflect.v taken
  • ✅ ssreflect.v compiles but needs more work
• ssrfun.v finished (0 Structure, 0 Canonical)
  • 🚧 ssrfun.v taken
  • ✅ ssrfun.v compiles but needs more work
• ssrmatching.v finished (0 Structure, 0 Canonical)
  • 🚧 ssrmatching.v taken
  • ✅ ssrmatching.v compiles but needs more work
• ssrnat.v finished (0 Structure, 4 Canonical)
  • 🚧 ssrnat.v taken
  • ✅ ssrnat.v compiles but needs more work
• ssrnotations.v finished (0 Structure, 0 Canonical)
  • 🚧 ssrnotations.v taken
  • ✅ ssrnotations.v compiles but needs more work
• tuple.v finished (1 Structure, 25 Canonical)
  • 🚧 tuple.v taken
  • ✅ tuple.v compiles but needs more work
• all_ssreflect.v finished
  • 🚧 all_ssreflect.v taken
  • ✅ all_ssreflect.v compiles but needs more work
• all_fingroup.v finished
  • 🚧 tuple.v taken
  • ✅ all_fingroup.v compiles but needs more work
• all_algebra.v finished
  • 🚧 all_algebra.v taken
  • ✅ all_algebra.v compiles but needs more work
• all_solvable.v finished
  • 🚧 all_solvable.v taken
  • ✅ all_solvable.v compiles but needs more work
• all_field.v finished
  • 🚧 all_field.v taken
  • ✅ all_field.v compiles but needs more work
• all_character.v finished
  • 🚧 all_character.v taken
  • ✅ all_character.v compiles but needs more work
• all.v finished
  • 🚧 all_character.v taken
  • ✅ all_character.v compiles but needs more work

Overlays

• Port to hierarchy builder Abel#75
• Port to Hierarchy Builder algebra-tactics#71
• Port to MathComp 2 analysis#951
• Port to Hierarchy Builder coq-community/bits#20
• tutorial mathcomp-2 coq-community/comp-dec-modal#10
• Porting to HB coq-community/coqeal#57
• https://github.com/proux01/coquelicot
• tentative port of finmap.v to HB finmap#84
• Port to Hierarchy Builder coq-community/fourcolor#44
• Port to Hierarchy Builder coq-community/gaia#11
• Port to MathComp 2 coq-community/graph-theory#25
• https://gitlab.inria.fr/coqinterval/interval/-/tree/hierarchy-builder
• Port to Hierarchy Builder mczify#39
• Port to Hierarchy Builder multinomials#42
• [wip] port to HB odd-order#37
• Porting to MathComp HB real-closed#38
• Port to MathComp 2 coq-community/reglang#46
• Port to MathComp 2 coq-community/tarjan#24

[gares]

Nix CI is broken:

error: value is a list while a set was expected, at /home/runner/work/math-comp/math-comp/default.nix:13:1

[gares]

@CohenCyril is this gitlab CI pipeline a new thing?

[CohenCyril]

You also need to add a only printing notation with the holes to preserve the printing upon simplification.

[gares]

@CohenCyril @pi8027 can you check if the recent locking in rat helps this example: 5e84326
I suspect it just gets slowed in this branch, but that it is already problematic.

[proux01]

Here is a squashed and rebase branch: https://github.com/math-comp/math-comp/tree/hierarchy-builder-rebased
(but I cannot force push here)

[proux01]

Rebase force pushed, the previous state (before squashing everything) is saved in https://github.com/math-comp/math-comp/tree/hierarchy-builder-before-rebase_2022_05_04

[proux01]

So, here is the state of the CI:

• I dropped planB
• coq-dev is borken on Nix CI (I understand that coq propagate ocamlBuildInputs NixOS/nixpkgs#161977 should fix it)
• unfortunately coq-dev is also broken on Docker CI since the lower bound for OCaml was bumped without coordinating with the maintainer of Docker images (https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/.3E.3D.204.2E09.20and.20opam/near/280985366) hopefully, this will be fixed soon
• reverse dependencies not ported yet
  • analysis
  • deriving
  • extructures
• other reverse dependencies are working out of the box or with an overlay (c.f. list of overlays at bottom of top PR description):
  • abel
  • addition-chains
  • autosubst
  • bigenough
  • category-theory
  • coqeal
  • coq-bits
  • coquelicot
  • finmap
  • fourcolor
  • gaia
  • graph-theory
  • interval
  • mczify
  • multinomials
  • odd-order
  • QuickChick
  • real-closed
  • reglang
  • verdi

[ejgallego]

Out of curiosity, how are compilation times affected?

[proux01]

Last figure I remember was nearly a factor two but @gares would know better.

[proux01]

So, here is the state of the CI:

• Coq master seems fine thanks to @CohenCyril 's branch (coqPackages: etc NixOS/nixpkgs#173112)
• only remaining broken reverse dependencies are:
  • analysis
  • deriving which uses universe polymorphism (c.f. https://github.com/proux01/deriving/blob/48f613b98bfe8d130431c00bac4fefa1e54576be/theories/base.v#L980-L982 ) not yet implemented in coq-elpi
  • extructures which requires deriving

[ejgallego]

Last figure I remember was nearly a factor two but @gares would know better.

A 2x increase in compilation time seems a bit surprising (and maybe worrying) . In particular, the amount of time spent in HB code should be just a small fraction of the compilation time.

Isn't that suspicious? What is the main bottleneck here.

I think that Coq really needs something like HB, but if users are gonna get a 2x slowdown from it I'm not sure it is ready until it is more optimized.

[gares]

The difference is that structures are more regular than before, and less manual tweaks. The time spent in HB commands is negligible, or close to so. The code generated is more likely to trigger bad behavior in conversion heuristics. But so far every time I did investigate a little change here or there would change the cost of a few lines of 100x, so I'm not scared, it is just about spending time on it.
And for now the (little) energy is in cover the whole ssrnum (not far, but not there yet).

[proux01]

@CohenCyril you can now delete yout hb-ssrnum branch as it is integrated here

As a consequence, we had to drop support for Coq 8.13 and 8.14, this now only works with:

• Coq 8.15 with HB master branch
• Coq 8.16+rc1 with HB master branch
• Coq master with HB coq-master branch

[gares]

Manual merge in master in progress