Home

Jump to bottom

affeldt-aist edited this page Oct 10, 2024 · 413 revisions

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)
wip: splitting of topology.v (issue 1167)
- already merged:
- related pending issue 1067
TODO, on the same model:
- rearranging normedtype.v
  - see details here
- splitting lebesgue_measurable.v
  - issue 1315
create issues for the following topics?
- convex.v (https://github.com/math-comp/analysis/wiki/2026-06-26-Meeting)
  - related to issue 860
- coq-mathcomp-real package (https://github.com/math-comp/analysis/wiki/2026-06-26-Meeting)
issue triaging:
- issue 271 (about landau and Banach-Steinhaus)
- issue 1269 (naming of set_mem)

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
2023
2022
2021
2020
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