Minutes November 08 2023
Participants: Cyril Cohen, Pierre Roux (chair), Quentin Vermande, Reynald Affeldt, Yves Bertot (secretary), Kazuhiko Sakaguchi, Enrico Tassi
see coq#17576 Let with Qed: produce really-Qed side definition This has been taken care of by Pierre Roux. No action is needed anymore.
see #1086
Do we want a parser, what should be constructed?
e la réunion mathcomp doit être discuté entre nous deux Kazuhiko thinks it should be always be towards the same time. It is better not to have this possibility for a generic ring.
There are performance issues, it would be better to have integer constants.
Cyril thinks one is losing generality and would prefer to see a better analysis of performance issue.
Pierre thinks it is possible to specify scopes to choose between alternatives.
A problem found by Laurent is mentioned, issue #1088
https://github.com/math-comp/math-comp/issues/1088
So fixing the issue found by Laurent may help for this issue.
The conclusion for this PR: we need to understand better the cause of the performance issue.
see #1110 to adapt to removal of recovery mechanism in Coq coq#17876 (even if first a warning) Cyril thinks the question should be sent to the Coq level because many other libraries will be impacted and be able to maintain compatibility with only one version of Coq.
looking for voluntieers to maintain multinomials. Pierre thinks the situation should be clarified. Expertise is not much of a problem. Cyril thinks this is related to the topic of the upcoming coding sprint on integrating finmap into math-comp.
there is a huge rewrite of multinomials, mpoly is the historic approach, as used in the Lindemann theorem, and there is another approach called monalg, which is more modular and algebraic, and allows multinomials to have an arbitrary set of variables. This monalg development is stalled but shows good promises. It would be better if we could finish this evolution of multinomials. This makes the maintainer question more relevant, but the person working on this would have to be more expert than just being a maintainer.
Kazuhiko is willing to co-maintain. Still calling for volunteers. Being the officially maintainer removes a psychological barrier. Somebody needs to check with Pierre-Yves Strub. Cyril will write a mail to P.-Y. Kazuhiko sends information about willingness to transfer maintainer status to Cyril.
the tentative schedule for the coding sprint is from 2023-12-11 to 2023-12-15
There is a plan to have a push of all functionalities of finmap into mathcomp, so that finite sets can be used in any choice type. Georges will be present, it is an initiative of Reynald. There is a discussion about advertising, more effort should be made on this by using a regular mail (instead of a zulip thing). Multinomials is a specific case that will be using both finsets and finmaps.
Finding a chair and secretary to replace Reynald who has been doing it for a very long time. The chair should definitely be distinct from the secretary. Pierre Roux will update the wiki page and he will chair for the next meeting. At each meeting we should decide of a new chair for the next meeting. The secretary can be decided at the beginning of the meeting.
Yves will contact Cyril to make progress on this.
This is sensible. Pierre will open a PR, Yves wants to be pinged on editions in this PR, if possible.
-
recurring topic from the previous meeting: there are several "mathcomp complements" files and directories in the mathcomp hierarchy, e.g.:
- Coq-Combi: https://github.com/math-comp/Coq-Combi/tree/master/theories/SSRcomplements
- cad: https://github.com/math-comp/cad/blob/master/extra_ssr.v
- newtonsums: https://github.com/math-comp/newtonsums/blob/master/auxresults.v
- multinomials: https://github.com/math-comp/multinomials/blob/master/src/ssrcomplements.v
- CoqEAL: https://github.com/coq-community/coqeal/blob/master/theory/ssrcomplements.v
it would be nice to collect useful things from them but how to do that efficiently?
-
PR triaging:
- Abel backports (https://github.com/math-comp/math-comp/pull/944)