Home

Jump to bottom

affeldt-aist edited this page Jun 26, 2024 · 412 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: 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)
News: MathComp-Analysis 1.2.0 released 3 weeks ago (https://github.com/math-comp/analysis/releases/tag/1.2.0)
take a decision about https://github.com/math-comp/analysis/pull/1191 (topology without pointed types)
questions raised recently:
- is it ok for us (users of the standard Coq library) to extend the core Hint database?
- generalization of {mfun _ >-> _}? (as in PR 672)
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
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