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: between 2024-06-26 (Paris Time)

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

Topics (please edit) ✍️

• Check TODOs from the last meeting (https://github.com/math-comp/analysis/wiki/2024-04-16-Meeting)

• take a decision about https://github.com/math-comp/analysis/pull/1191 (topology without pointed types)

• question: is it ok for us (users of the standard Coq library) to extend the core Hint database?

• work in progress about measure.v:

  • merge PR 1251?
  • setD_closed vs. setDI_closed PR 1243

• PR triaging:

  • merge the Banach-Steinhaus PR?
  • to_set vs. xsection PR 1248

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-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