-
Notifications
You must be signed in to change notification settings - Fork 129
Minutes 2025 03 19
Pierre Roux edited this page Mar 19, 2025
·
1 revision
- attending: Alessandro, Cyril, Kazuhiko, Quentin, Pierre, Reynald
- any MathComp-related paper spotted at POPL/CPP/CoqPL 2025? (this is to report on the website)
left from last time - release
RM: Allessandro with help from Cyril
then, there will be a MC Analysis release at the end of the month - droping 8.19? #1354
do we have "emergencies"?
introduction of sesquilinear screwed up some notations - Using deprecated.use directive to make good use of vscode quickfixes
using it in 8.20 is an error, so we need to wait until MC requires 9.0
could be backported to some 8.20.2 but not worth it - and merge long standing large PRs #1256 #1169 #1125 (one structure ops, preorders, semi-modules)
something to decide about addr_closed? is it "closed for addition" or "closed for 0 and addition"
deprecate GRing.addr_closed in favor of Algebra.nmod_closed with a new "Algebra" namespace?
what should be the extent of that new namespace? (many structures are not algebraic)
should we have HB handle namespaces?
no namespace for "canonical" structures? don't remove modules, would be hard to come back if it appears to be an error
we don't remember exactly what was the original reason for GRing (protect internal subdefinitions?)
conclusion: for now, just rename GRing to Algebra in monoid and commutative monoid
conflict between semi-modules and one-op?
conclusion: first release, then semi-mod #1125 to be merged first, then #1256 and #1169 rebased on top of it - naming of closure predicates (e.g. addr_closed vs. nmod_closed)
agreement that addr_closed should be stability by add and nmod_closed with 0 and add - basic lemmas about trunc/floor/ceil #1359
do we want to define |.|+ : int -> nat := "max(0, .) as a nat"
currently floor and ceil defined out of trunc, should this be changed?
conclusion: only review for good names and statements for now, proofs can be updated later
reopen PR on Analysis, review and merge it there, then backport once merged