Minutes April 21 2021 - math-comp/math-comp GitHub Wiki

Participants: Assia Mahboubi, Christian Doczkal, Cyril Cohen, Enrico Tassi, Kazuhiko Sakaguchi, Pierre Roux, Reynald Affeldt, Takafumi Saikawa, Yves Bertot.

1. Extract concrete actions from pad
   • starting point of the conversion: having a CODEOWNER file, a solution for which problem?
   • we did a pad to better understand the situation
   • which problems did we identify?
     • the process of putting stuff into MathComp is not documented enough
       • there exists several way to use git and github
     • lack of communication about the technicals of MathComp?
       • many things are not technical (naming, etc.), not everybody touches the hierarchy
     • no separation implementation/interface
       • no mechanism (modules do not fill the same role as in OCaml)
       • that's the role of the headers (= exactly the def API)
       • Local is unfaithful approximation
     • see also the end of the pad
   • solutions:
     • document the contribution workflow that we expect for MathComp
     • more tutorials to communicate about details?
     • improve coqdoc to distinguish API from internal?
     • we also want attributes for the Search command
     • clear separation public/private interface
   • TODO:
     1. feature request for Coq explaining what we need to implement the previous solutions natively in Coq
     2. document the current practice of MathComp to circumvent that
   • clarify the link between header and API
   3. postpone to the next meeting the problem of not enough workforce (not enough contributors and reviewers, meeting time not optimized)
2. Make a precise list of support tasks to give to an engineer... (e.g. linting with detailed rules)
   • wait for the extraction of solutions from the pad
   • there are possibilities for hiring such an engineer (using in-progress grants, teams of Inria engineers)
     • OCaml skills might not be that easy to find
3. Demo/Tutorial: how to setup a working environment for creating or reviewing a PR, under 3min, using nix
   • videos are available but can be improved (need more time, as general as possible audience)
   • see https://github.com/math-comp/math-comp/wiki/Creating-and-editing-PRs
   • so postponed
4. List the main theorems in MathComp
   • purpose of such a list? for the newcomer mathematician who expects to find result they know
   • how to maintain such a list?
     • related to the earlier discussion on searchable items using tags
     • when to add things? how to make sure they are correctly linked to the code?
   • main results marked as Theorem (not consistenly used)
   • some theorems appear as several variations
   • Lagrange Feit_Thompson
   • human procedure for this might be enough
   • Farkas' lemma, pumping lemma are not "theorems"
   • making a list first and then do the tool might be a waste of time
   • a few hundred elements could end up in the list
   • potential result: https://en.wikipedia.org/wiki/List_of_theorems, https://en.wikipedia.org/wiki/List_of_lemmas
   • need a natural language explanation, a reference in the litterature, mention the area of mathematics
   • ref: https://leanprover-community.github.io/theories/topology.html, https://leanprover-community.github.io/undergrad.html
   • TODO:
     1. Long-term action: what should we ask on the coqdev side
     2. Short-term action: a bash-generated list from special syntax in comments
   • natural language name
   • natural language description
   • reference
   • maths topic
5. Status report of the porting of MathComp to HB?
   • major remaining points:
     1. interaction normedZmodule and normedDomain
     2. unification slowdowns here and there
   • due to the change in packaging
   3. still instances built in the middle of proofs
   • minor remaining points:
     1. removing unnecessary alias and tweak HB to stay as close as possible to the previous version of MathComp
     2. optimize some algorithms in HB like some sorting algorithms and structure instantiations
   • anticipating difficulties with the odd-order theorem
     • only one structure in odd-order though minSimpleOddGroupType is a telescope
   • how to we release it (MathComp 2)?
     • might need to release the master branch as MathComp 1.13.0 before MathComp 2,
     • we should keep maintaining MathComp 1 after MathComp 2 for some time introducing no breaking changes in the legacy version
6. Porting finmap to HB
   • finmap.v is ported, set.v relies on things that are not available in HB
   • subobject (e.g., subgroup, subfields, subrings and so on) are not yet supported by HB
     • see Zulip topic on porting dioid
     • they present other problems than structures and morphisms