Minutes June 15 2022 - math-comp/math-comp GitHub Wiki
Participants: Kazuhiko, Laurent, Pierre, Reynald
- release a 1.15.0? (1.14.0 doesn't compile with Coq 8.16)
- need a RM
- we now have Coq 8.16+rc1 in Nix CI
- go through 1.15.0 milestone
- create 1.16.0 milestone (might be renamed 2.0 later on)
- postponing Modular lattice of linear subspaces #613 and [WIP] Make linear subspaces canonically a tbLatticeType #653
- postponing #660, #94 and #311 about
Arguments
andsimpl never
- Remove hint-without-locality warnings #891
test#[export]
in CI and go for it if it doesn't break too much (Pierre will do) - Removing dffun in favor of ffun #701
linked to PR #745 let's postpone - Add notations for patterns in [seq ... | ... ] notations #790
- was waiting fo Coq 8.13 to become the minimum, now the case
- keep it and postpone later if we don't hear back from Jason
- [build] Support for building with Dune #316
postponing - Checking exports in ssralg.v #440
Pierre will do the check - Reducing the number of displayed warnings #529
- mark "ident" vs "name" warning as fixed by #856
- and postpone the remaining
- remove big_uncond #590
Reynald will open a PR - Add predicates and lemmas for subchain, prefix and suffix on seq.v #779
- looks ready but unattended, will merge if no further comments
- chack that "changes request" were indeed handled
- WIP galmx : gal_of -> matrix #800
pinging Cyril - WIP matrix of a function and base change matrices #801
postponing (involves more design choices) - [CI] First attempt to document Nix CI #810
- postponing
- maybe ask Marie and Assia for a review once updated
- Adding vm_compute rewrite rule #813
ask for a test case - Improving ssrnum.v #818
about complex numbers, asking Cyril to rebase - Add [in A] notation #863
asking Georges to rebase, looks ready and thoroughly reviewed, should be merged - port from mathcomp-analysis #859
no further comments, maybe could be merged? - Extensionality functions - f, f * g, f \min g and f \max g #887
- approved
- Kazuhiko notice that
\min
and\max
should go in order.v (Pierre will update the PR) - are
\min
and\max
used? useful in bigops, Pierre would use them in dioid
- #893
- should credit Reynald as coauthor
- question about balancing of multirewrite rules for performance (e.g., https://github.com/math-comp/math-comp/blame/7ce300ad48f8747c48a340b84d94c7d2bda2ce72/mathcomp/ssreflect/ssrnat.v#L1849) open an issue to ask if someone remembers more details, not a blocking issue
- depending on #889
- Reynald assigning
- #892
postponing (until we require Coq 8.14)