Minutes April 20 2022 - math-comp/math-comp GitHub Wiki

Participants: Reynald, Cyril, Enrico, Kazuhiko, Pierre, Laurent

what should we do with very old issues (> 5 years old)
- #3
  - this code is not in MathComp anymore
  - let's retarget it to Coq
- #4, #5
  - move to Coq
- #28
  - within sections it is impossible to know in advance what would be generalized
  - Proof using [some set of hypotheses] mitigated this issue
  - the issue is about a kind of parallelism that maybe isn't wip anymore
  - update the reference to the manual and update the title
- #29
  - feature request for writing convenience
  - maybe the scope annotation is a bit too far away
- #30
  - bug report
  - there was a follow-up on the SSR ML with a shorter example
  - TODO: somebody will check
- #35
  - closed (the error message has been improved since)
- #45
  - problem with an uninformative error message
  - TODO: ping Enrico
planning another MathComp 2.0 pass?
- ssrnum blocker
  - Cyril may have a solution that involves reviving an old branch of HB that didn't work https://github.com/math-comp/math-comp/blob/5e84326f5a6759b1d227f066088988e39e8538ff/mathcomp/algebra/ssrnum.v#L141-L149
- use hiearchy-builder also for functions
  - indeed that would be nice
  - first we need to rebase
    - Pierre to try by next week
- planning for reversible coercions? (following https://github.com/coq/coq/pull/15693)
  - at the same time?
  - will be available in the next version of Coq
  - it will simplify the things that HB generate
  - it will only introduce simplifications and thus we can allow for temporary complicated detours in the meantime
  - when we drop support for Coq 8.15
  - schedule to be decided on the next meeting
settle the topic of eqLHS, etc. notations (https://github.com/math-comp/math-comp/pull/869)?
- Laurent
  - prefers consistency (eqbLHS instead of eqLHS)
  - problems with leq vs. le
  - would like to introduce ltnLHS, etc.
  - TODO: introduce the variants for natural numbers, use eqbLHS instead of eqLHS
- experiment using custom entry in progress
  - one special rule for each infix
- Cyril is not fond of the generic notation because it introduces problems