TL;DR: We will meet from Tuesday April 6th to Friday April 9th to do the port. Please make sure you can read this mail in detail and complete the "homework" before that.
In the current state of the mathcomp library, we reached a critical point where it is hard to add a structure on top of the hierarchy and even harder (and non-backward compatible) to add intermediate structures. Hierarchy Builder was designed to solve precisely these issues and we (Enrico, Kazuhiko and me) started porting mathcomp to HB, in order to use structures generated declaratively by hierarchy builder, and the results look promising so far.
In order to unlock the situation as fast as possible, the goal of the current document is to organize a collective effort to continue the port of mathcomp.
Cf https://github.com/math-comp/math-comp/tree/hierarchy-builder
See the visual summary of the port.
A little less than half the structures have been ported: all of
fingroup.v, presentation.v, morphism.v, ssralg.v, bigop.v,
ssrfun.v, seq.v, choice.v, binomial.v, ssreflect.v, div.v,
fintype.v, ssrbool.v, ssrnat.v, eqtype.v, tuple.v,
fingraph.v, prime.v, path.v, finset.v, ssrnotations.v,
finfun.v, ssrmatching.v have been ported, including 36 structures.
A third of order.v has been ported so far, and generic_quotient.v,
ssrAC.v and perm.v are waiting to be ported: they are the files
that make fails on and are blocking for all the files that are not
mentioned above. There may be missing features in HB to address them
properly but no way to identify these missing features precisely
without doing the porting. Moreover since multiple failures occur in
parallel their is a potential for multiple groups to work at the same
time. Hence we suggest to have a porting sprint.
Let us have a full week sprint (see date choice below) where at least Enrico, Kazuhiko and me are all available (I'd say at least 80% of the time) and with as many people as possible to perform the port. During the event we could form three groups of 2/3 people (each group including Enrico, Kazuhiko or me) working in parallel so that whenever there is a bug or missing feature, it could be immediately escalated to people knowledgeable about the code of HB (written in elpi/coq-elpi).
I suggest the following schedule.
- In order to focus all our effort simultaneously in the mathcomp library, I think it is necessary that everyone involved gets familiar with the basic behaviour of hierarchy builder, by watching the two following talks:
-
Then, I would like everyone to install HB (1.0.0) on their system (using opam or nix, as described in HB's readme) and implement a small hierarchy from scratch (e.g. additive commutative monoid, ring, and additive abelian group) and ask questions on Zulip HB stream if you encounter any difficulty.
The documentation and demos in HB repository are all up to date. The syntax and behaviour from the talks and the paper are still valid (they form a subset of nowadays HB).
We should improve HB's documentation by March 5th.
-
If you have the opportunity, please attend March 5th meeting 10:00 - 12:00 Paris time about the internals of HB. It is not mandatory but it can only help.
-
Watch this video where I port the first structures of
order.v
-
On the first day we will have a common session 9:00 - 10:30, to make sure everyone has a development version of HB and the mathcomp branch for the port.
-
From 10:30 - 11:00 we will dispatch tasks between teams, each team works in autonomy on their file. Is there is a bug or missing feature in HB, it should be signaled to everyone, in order to check whether the need is specific or shared. Each issue should be opened on github and either worked around or fixed on the spot, depending on the severity of the bug/missing feature.
-
We meet again on day 2, at 10:00 and go through the issues, and so on, we iterate until all the tasks listed below are achieved (or at least 1. and 2.)
-
port all of mathcomp, working around missing features whenever possible, and giving priority to the shortest path towards
galois.v(this is were we might encounter severe slowdowns, which should be detected and fixed ASAP). The port must not add a new structure. The exceptions to that rule are:- structures that were encoded via telescopes and transition to packed classes via HB, e.g. substructures.
- structures that would make the join non unique (HB has a builtin safeguard for that).
-
document the new version of mathcomp and add the most urgent missing features to HB (the ones where the workaround were the ugliest).
-
extend HB to support morphisms
{morphism _ -> _},{rmorphism _ -> _}etc and port mathcomp. -
extend HB to support predicate hierarchies
rpred*lemmas and port mathcomp. -
extend HB to support
{group _}and{aspace _}in an automated way and port mathcomp. -
extend mathcomp with more structures or test alternative encodings.
There is a risk that a bug, missing feature or performance problem in HB prevents us from advancing in the mathcomp port. In that case here is what would happen:
-
if the problem occurs only in a delimited part of the library, we split in two groups: one group to continue the port, avoiding the problematic parts of the library, the other group, with Enrico, working on a solution.
-
if the problem occurs in the totality of what remains to port at the time the problem is discovered, then we all stop and discuss possible solutions and whether the week is enough to implement them and finish the port. If it is not the case, we may reschedule another week if the remaining work is substantial.
The part where a problem is most likely to occur is in galois.v or
above, where there could be performance problems involving slowdowns
of several minutes. If that's the case, there will be no structure
left to port at that stage, only a few canonical declarations to
replace with HB.instance, and it is likely it would not require
another group session once the problem is solved.
Moreover, if no additional structure is added to the hierarchy (as
stipulated by Task 1.), it is unlikely problems show up before
galois.
Cyril