Participants: Reynald Affeldt, Cyril Cohen (chair), Georges Gonthier, Pierre Roux (secretary)

issue already discussed in a previous meeting https://github.com/math-comp/math-comp/wiki/Minutes-November-08-2023#scope-issues-with-constant-literals-in-ssrint which pointed at issue #1088

• HB should simplify the instances it automatically adds (for instance semiring when manually declaring a commutative ring)
• we could also further simplify HB by separing Type and Prop fields
• also possible improvement: don't box mixins with a single field (maybe not the most urgent optim)

Coq 8.19+rc1 will be out soon, last releases (2.1 and 1.18) are not compatible with it (master is), so a release (at least a 2.2 but likely also a 1.19) will be in order, need release manager(s)

• needed "urgently" due to last release not compiling with 8.19
• would be nice for release managers to turn (Reynald and Pierre did the last four releases last year)
• Pierre volunteer to coRM with a new volunteer
• more midterm: would be nice to automate release process
• side note about performance: on Intel Xeon E-2236 3.4GHz, 32GB,
  • MathComp-Analysis 1.0 with Coq 8.18.0 HB 1.5.0 -> 38m33
  • MathComp-Analysis 1.0 with Coq 8.18.0 HB 1.6.0 -> 20m2 on Intel i7 i7-1265U
  • MathComp-Analysis 0.6.7 with Coq 8.17.1 HB 1.5.0 -> 7min51

making _%:R a coercion: https://github.com/math-comp/math-comp/pull/1051#issuecomment-1877159942 offer to add directionality hints to Coq

• we don't want the directionality thing (exponential)
• hook in the pretyper that could call elpi code
• find coercions
• call trocq
• Pierre will try to implement the hook
• question about what to read about trocq?
• Wouldn't the already existing coercion hook be enough? no, it's too deep in the pretyper

• https://github.com/math-comp/hierarchy-builder/pull/195 ? old, test if bug (test case in the PR) still applies, if yes rebase, if no close

• https://github.com/math-comp/math-comp/pull/1123 ** nothing happened, merging ** extra space in "semi rings"

cf https://github.com/affeldt-aist/monae/pull/122

• wanted to do a git bisect between HB 1.5 and 1.6 but gave up due to many things to recompile every time -> still applies
• carrier bug should be solved by https://github.com/math-comp/hierarchy-builder/pull/195
• constraint bug? ** could be related to the use of equations: test by inputing the term produced by equation by hand (rather than letting equation's OCaml code do it, maybe with a bug related to primitive projections?)

• missing things: product, containers
• solution for ~~ P && Q, then ~~ P will likely be finite only because base type is finite so trying to prove Q finite rather
• questions about too many reverse coercions, nat_of_bool shouldn't be a reversible coercion ** all agree, Pierre should look
• question about HB: does it automatically construct things that don't need more mixins? ** we have "empty" factories for that but they need to be manually called
• implement card and co on finset and use coercion from finpred to finset ** now feasible since the removal of the UIC condition on coercion enable a coercion from seq to pred