Home

Guides

• FAQ

• Documentation (link inside the README)

  • What's where?

• How to contribute

• How to document

• How to release

• How to bump

Meetings

Next meeting

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

• poll: https://framadate.org/z74878uodlbotQjW
• visio: https://jitsi.riot.im/mathcomp_analysis

Topics (please edit) ✍️

• 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:
    • https://github.com/math-comp/analysis/pull/1166
    • https://github.com/math-comp/analysis/pull/1324
    • https://github.com/math-comp/analysis/pull/1338
  • 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

• PR triaging:

  • PR 1340 on continuous functions
  • PRs for which reviews have more or less started (feel free to jump in):
    • PR 1256 on the {mfun _ >-> _} type for measurable functions
    • PR 1331 on completely regular spaces

• issue triaging:

  • naming issues:
    • issue 1269 (naming of set_mem))
    • issue 1292 (about the opp prefix/suffix)
  • issue 271 (about landau and Banach-Steinhaus)
  • issue 1320 (near message error)

Long-standing issues

• 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

Minutes

• 2024
  • 2024-06-26
  • 2024-04-16
  • 2024-02-09
• 2023
  • 2023-12-21
  • 2023-10-16
  • 2023-07-27
  • 2023-06-21
  • 2023-04-20
  • 2023-02-06
• 2022
  • 2022-11-22
  • 2022-09-22
  • 2022-07-27
  • 2022-04-12
  • 2022-02-24
  • 2022-01-20
• 2021
  • 2021-12-16
  • 2021-09-28
  • 2021-07-22
  • 2021-06-22
  • 2021-05-27
  • 2021-03-26
  • 2021-01-26
• 2020
  • 2020-12-17
  • 2020-11-05
  • 2020-09-28
  • 2020-09-04
  • 2020-07-24
  • 2020-06-17
  • 2020-05-25
  • 2020-05-07
• 2019
  • 2019-12-16
  • 2019-09-26
  • 2019-07-18
  • 2019-06-28
  • 2019-06-27
  • 2019-06-07
  • 2019-05-27
  • 2019-05-14
  • 2019-05-09
  • 2019-03-26
  • 2019-02-27 (minutes lost?)
• 2018
  • 2018-12-12
  • 2018-11-08