Minutes September 06 2023
Participants: Reynald, Pierre, Julien, Cyril, Enrico, Yves
Topics for 2023/09/06:
-
FYI: MathComp master (2) is back in Coq's CI: https://github.com/coq/coq/pull/17722
-
FYI: 8.18 now in MC and Analysis CI
-
follow up on MC2 performance:
-
math-comp#1059
- a proof was cut in two with a Qed to reduce the memory consumption
from almost 3GB to about 0.5GB
- Enrico: Is it the
HB.pack? - Cyril: try to inline to code generated by
HB.packto know - Pierre: this is really the final Qed that takes time
- Enrico: Is it the
- leave a comment to remember that a script was cut in two, merge the PR as such
- communicate the probleme to Coq developers
- a proof was cut in two with a Qed to reduce the memory consumption
from almost 3GB to about 0.5GB
-
hierarchy-builder#380
- Enrico: would have merged but the CI is too broken
- Enrico: are we still supporting 8.15?
- Cyril: keep 8.16, 8.17. 8.18 so that we can enjoy reverse coercions
- this will also improve performance (factor 2 observed with category theory)
- Pierre: the infer parameter is then not needed anymore (?)
- 30/40% more memory with MathComp, less than x3 in time
-
math-comp#1059
-
ring coercions: #1051
-
as discussed last time need to remove algebraic instances on
nat,intandrat- put instead on aliases
nat^r,int^randrat^r - and also accessible through notations
x +_int y
- put instead on aliases
-
then coercion work pretty well: https://github.com/math-comp/math-comp/pull/1051/files#diff-3322ad2eded178077c93aa3889bb9ce26a9afd8eb42d3f3ebbd705f0b48a63f7
-
for display, idea from Cyril: alway display the coercions
%:Rexcept on variables -
demo by Pierre:
-
%:Rdisplayed for expression (e.g., (n + 1)%:R) but not when applied to variables (nrather thann%:R) -
x = nbutn%:R = x - requires
8.18 - pending problem:
n + xdoes not type-check as intended if there is a structure of n-module onnat - yet, we would like to keep the structures on
natandint - Cyril: Lean solved the problem (using type-classes and back-tracking (?))
- Cyril: "unification modulo"?
- Enrico: use a syntactic trick to call an auxiliary elaborator,
but it should be about the whole expression but not locally
- requires fall-back (Coq 8.18 or Coq 8.19)
- Move coercions to contexts: https://inria.hal.science/hal-04177913/
-
-
-
deprecating the qualify mechanism? only used to display
\is,\is aand\is aninstead of\in, makes declaration of predicate instances more complicated and tricky (introduces a coercion from qualified to{pred _})- Cyril: this mechanism can be redone on top of
\inbecause it is an instance of displays - Cyril:
\is a,\is anhave been added after\in, there is room for uniformization - Cyril: there is also a plan to replace
\inso it might be worth waiting for this alternative
- Cyril: this mechanism can be redone on top of
-
Overdue milestones: https://github.com/math-comp/math-comp/milestones
- Yves: had problem to replace
[eqType of _]with MathComp 2 because the message is mentioning a solution usingclone- Pierre:
??? : eqTypeshould suffice - Cyril: it should be possible to do a PR to Coq to tell the user that a structure canonique is lacking
- Pierre: need a "canonical structure Debug" like for type classes
- Cyril: need a difference trace if we are designing a hierarchy or if we are lacking an instance
- Cyril: Shouldn't information be displayed with mouse hovering with a mode "show more" like in Lean?
- Enrico: at least, we would like to display more information than
HB.about - TODO: discuss the issue with Romain
- Enrico: automatization of the release of coq-elpi
- Cyril: we should check the documentation when PRing
- Pierre:
- discussion about regular releases (every 6 month ?): inconclusive
- not much release-manager volunteers, Reynald and Pierre to release a 2.1.0 at some point in October
- Yves: had problem to replace
-
pending PRs