Home

Guides

Date: 2024-10-10 (Thu.) 14:00--15:00 (Paris Time)

Check TODOs from the last meeting (https://github.com/math-comp/analysis/wiki/2026-06-26-Meeting)
about the splitting of topology.v (issue 1167)
- Zachary's plan is almost complete
- already merged:
- related pending issue 1067 (real_topology.v) (was proposed by Saikawa)
splitting of normedmodule.v
- issue 1339
- on zulip also
- NB(rei): I would advocate for an incremental split that spans at least one release like we did for topology.v because there was unexpected (minor) problems (with the CI) and because the reviews proved useful to fix and improve the doc (and also for the changelog)
splitting lebesgue_measurable.v
- issue 1315
- the Lebesgue measure appears in the middle of the file, the first half is rather about measurable functions over the real numbers or the extended real numbers
create issues for the following topics?
- changing the convention in convex.v to fit Infotheo (https://github.com/math-comp/analysis/wiki/2026-06-26-Meeting)
  - the sooner the better
  - related to issue 860
- coq-mathcomp-real package (https://github.com/math-comp/analysis/wiki/2026-06-26-Meeting)
  - it might be good to have a version of the packager of MathComp for MathComp-Analysis
issue triaging:
- issue 271 (about landau and Banach-Steinhaus)
- issue 1269 (naming of set_mem)
PR triaging:
- Reminder: PR 1256 on the {mfun _ >-> _} type for measurable functions

Documentation:
- how to prove that something is a nbhs?
  - NB: already partially addressed in FAQ
  - impacted by the port to Hierarchy-builder #915
Simplification of the filter layer
- see #300 and #282
- impacted by the port to Hierarchy-builder #915
Issue related to Landau:
- typechecking in Landau notations using derive.v