Skip to content

2025‐04‐11 Meeting

Jump to bottom Edit New page
affeldt-aist edited this page Apr 12, 2025 · 2 revisions

Participants: Alessandro, Cyril, Kazuhiko, Marie, Pierre, Quentin, Reynald, Takafumi, Yosuke, Zachary

  • work in progress: the online documentation

    • using rocq-navi, now available on opam (see)

  • per-PR changelog, similar to https://github.com/math-comp/math-comp/pull/1328

    • should we keep the name of the author of the PR in the changelog?
      • maybe not
    • are changes reorganized for each file?
      • should be done
    • anyway, we cannot avoid curating the changelog in the end
    • tak: adding comment to lemmas to have the history of name changes and changes in statement?
    • tak: adding in separated changelog a description of the intent of the PR in addition to the number of the PR
      • maybe not needed because there is a link

  • check unstable.v

    • mathcomp_extra.v were welcoming things that were actually not backported as such
    • now mathcomp_extra.v just duplicates the information that is already backported
    • https://github.com/math-comp/analysis/blob/master/classical/unstable.v
    • check unstable.v to elect things to be backported (but not before the release, too much work the release manager)
    • when do we flush that?
      • during the meetings and the sharing day

  • add lra and interval to the dependencies? (ale)

    • CoqInterval depends on the stdlib so no (pie)
    • ale: special packet for experiments/applications of MathComp-Analysis?
      • like showcase (showcase not intended to be reused)
      • like experimental_reals (pi) ?
    • cyr: we just need to rewrite from mathcomp to the stdlib and call the interval tactic
      • pie: this is already in Rstruct.v
      • produce a table for every real function (sin, cos, +, *, etc.), they are not the same that ours but we can have theorems
    • tak: evaluation of Taylor expansion?
      • need to prove that Lebesgue and Riemann from the standard library agree
      • cyr: does the standard library handle piecewise-continuous? yes (pie)
    • TODO: is showcase the right word?
    • TODO(rei): new package for sfppl
    • TODO: sampling theorem -> might end up to analysis_stdlib

  • move separation_axioms.v into topology_theory

    • tak: why is it outside?
      • no specific reason
    • breaking change?
      • should not break external development
    • TODO: PR (list it in topology.v? -> yes! (zak))

  • splitting of normedtype.v: PR 1544

    • Marie ok with the split and the fix
    • TODO(zac): review
      • urysohn.v might end up in topology
      • put a deprecation notice before urysohn in the Export file for the transition
    • tvs.v will depend on pseudometric_normed_Zmodule.v file
      • lemmas standard_add_continuous and standard_scale_continuous are duplicates
      • TODO: try later to eliminate these duplicates
      • NB(que): take the standard_topology section outside of the file and maybe this tvs.v should not be moved to normedtyped.v

  • cumulative distribution function

    • intended to be used in actuary
    • TODO: merge
    • cdf should be an instance of Cumulative
      • cumulative is R -> R
      • cdf is R -> \bar R
    • TODO: generalize to topological order space, just add an instance of cumulative as a separate
    • generalize later (e.g., cadlag)

  • lspace master

    • Lp norm are defined with codomain \bar R but specialized everywhere to R, this should be uniformized
    • generalizing the p?
      • this has actually been generalized but need check
    • generalizing the function? e.g., l.475: Local Notation "'N_ p [ f ]" := (Lnorm mu p (EFin \o f)).
    • the goal is to uniformize to help future changes
    • functions should never by cast to reals
    • TODO(ale, rei): review all the lemmas
    • milestone: 1.11

  • PR triaging:

  • prod/pair naming issue 1514

    • TODO(cyr): review

  • Small lemmas from the formalization of the Gamma function

  • PR 1491 --- Boost derive

    • TODO: merge when CI green

  • recurring topic: flush unstable.v

    • maxr_absE, minr_absE go to ssrnum.v
    • TODO(rei): PR

  • about the naming of weak topologies: new issue

Add a custom footer
Add a custom sidebar
Clone this wiki locally