Minutes December 1 2021 - math-comp/math-comp GitHub Wiki
Participants: Christian, Cyril, Enrico, Kazuhiko, Laurent, Reynald, Yves
- https://github.com/math-comp/math-comp/pull/808 made me think that
we may (or may not) want to ad a Number Notation in rat, to be able
to write numerical constants as 42 or 3.14 in rat_scope (Pierre (but
I won't be available on December 1st))
- Cyril:
- desirable indeed, and also for ring
- Reynald: isn't it the role of
%:R
? - Cyril:
- this could alleviate inefficiencies (due to hnf, due to discrimiante) in rat
- TODO: experiment with a number notation in rat (and also in ring)
- Pierre: will do a draft PR (note added after the meeting)
- Kazuhiko: the good thing with
_%:~R
(for int) is that it is an additive function (or a ring morphism if the codomain is a ring). I think we should rather include GRing.natmul in the interface of zmodType - Cyril: MathComp relies a lot on
1%:R
is 1 and putting natmul in the interface would break this property
- Cyril:
- status of https://github.com/math-comp/docker-mathcomp/issues/12
- because of stdlib-shims, coq-elpi requires at least OCaml 4.07 https://github.com/coq/opam-coq-archive/pull/1826
- not fixable on Enrico's side
- we are left with the option of upgrading the docker image with OCaml > 4.05
- TODO: ping Erik
- NB: during the last release Cyril add to fix the following file https://github.com/math-comp/docker-mathcomp/blob/master/images.yml whose fix is not yet reflected in the documentation
- other refererences:
- HB and OOthm
- Enrico:
- odd-order-theorem compiles with the HB-version of MathComp but is not fast (half an hour)
- Cyril:
- why does it not work with Coq 8.13?
- see the CI ouput here https://github.com/math-comp/hierarchy-builder/actions/runs/1523253447
- NB: mathcomp becomes twice as slow (+ 10 minutes), odd-order was 12 minutes
- why does it not work with Coq 8.13?
- Reynald:
- minor fix following to the port of finmap to hierarchy-builder
- Cyril:
- discussing the remaining issue related to ssrnum with HB
- further discussions on the performances of the CI
- Enrico: how does Coquelicot use MathComp?
- Enrico: