Skip to content

2026 06 26 Meeting

Jump to bottom
affeldt-aist edited this page Jun 27, 2024 · 1 revision

Participants: Alessandro, Marie, Pierre, Reynald, Takafumi

  • News:

  • take a decision about PR 1191 (topology without pointed types)

    • Zachary cannot be here but it seems that preserving backward-compatibility is beyond our resources
    • what about breaking backward compatibility?
      • Pierre: +1 (won't probability break that much)
      • Reynald: +1 (be pragmatic)
      • no vote against

  • questions raised recently:

    • move signed.v and constructive_ereal.v to classical?
      • Pierr: coq-mathcomp-real package?
      • would contain signed.v, constructive_ereal.v, reals.v, real_interval.v, Rstruct.v
      • TODO: pierre not available now for this, maybe later in the summer, might be done by then
    • is it ok for us (users of the standard Coq library) to extend the core Hint database?
      • Pierre: better ask that kind of questions to PMP
      • we already core in MathComp
      • In SSRreflect, by, //, etc. use core
      • it is not obvious how to deal with another database (using /0?)
      • Pierre: probably fine to add hints to core as long as by it is not slow
    • floor, ceil, etc. subsumed by MathComp PR 1244
      • TODO: do Import Num.Def rather than using a scope
      • new lemmas to avoid the is a real subgoals, e.g., floor_ge_int should be renamed real_blah in MathComp
      • iow, we need specialized versions

  • merge the Banach-Steinhaus PR?

    • Marie: yes
    • a few lemmas can be moved to topology.v
    • TODO: try to move le_closed_ball to topology.v
    • use HB.pack to avoid mylinear
    • TODO: do not forget to properly credit Theo Vignon
    • Marie might have time in August for that

  • about the semi_ prefix in measure.v issue 1072

    • compare semi_additive to additive
    • rename semi_additive to semi_finitely_additive (too long...)
    • Pierre not worried, he wouldn't do any name change just to avoid the conflict
    • TODO: try to localize the semi_ lemmas in a module?

  • work in progress about measure.v:

    • following the introduction of sigma-rings PR 1222
    • merge PR 1251?
      • better name for isAlgebraOfSetsD ?
      • TODO(takafumi): review
    • setD_closed vs. setDI_closed PR 1243
      • setD_closed -> setSD_closed of setD_proper_closed
      • TODO(takafumi): review

  • question about patch in issue 1100

    • Takafumi: where is the name patch coming from? what about windowing?
    • example of favoring \_ vs. patch: PR 1246
    • Reynald thinks patch is good because it gives a look'n'feel closer to bigop

  • generalization of {mfun _ >-> _}? (as in PR 672)

    • TODO(alessandro): to experiment next week
    • related topic: the Giry monad
    • Takafumi: lemma without interface to go to analysis and the interface to go to monae?
    • TODO(alessandro): for the time being, move the giry monad to the showcase subdir

  • easy corollary to FTC1 PR 1250

    • Takafumi is FTC1Ny useful? maybe in some cases
    • TODO(takafumi): review

  • input wanted about Lp-spaces PR 1230

    • we need to experiment whether it improves probability.v...
    • Alessandro+Reynald+Takafumi: resume thursday meeting (Paris 09:00, Tokyo 16:00) on Thursday from next week?

  • new Zorn's PR 1198 (stalled by lack of time)

    • TODO(rei): document and CHANGElog

  • to_set vs. xsection PR 1248

    • rename to: xsect? Pierre fears it augments mental charge
    • need to review to answer
    • TODO(rei): to_set is to go, do more than one pass to decide the renaming

  • Takafumi: wants change mathcomp-analysis convexity default convention

Clone this wiki locally