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
  • PR 1300 on topological vector spaces
    • in the current state, it leads to the addition of necessary type constraints (0:R) otherwise Coq fails to figure out the topological space, no idea why?
  • PR 912 on probabilistic programming languages
    • this PR relies on lra and the CI fails because of that, what can we do? (very soon we will start using lra in master probably

• issue triaging:

  • naming issues:
    • issue 1269 (naming of set_mem))
    • issue 1292 (about the opp prefix/suffix)
  • questions:
    • shall we close issue 759 now that relations have found a place in classical_sets.v?
    • issue 1268 (about at_point and principal_filter)
    • issue 1077 (about measure_addE)
  • issue 271 (about landau and Banach-Steinhaus)
  • issue 1320 (near message error)

• 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

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