Home

Guides

Date: between 2024-06-26 (Paris Time)

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)
- Alessandro's presentation at TYPES: https://alessandrobruni.name/papers/24-mca_proba.pdf
- corollary to FTC1 PR #1246
  - "poor man's FTC2"
  - under review
take a decision about https://github.com/math-comp/analysis/pull/1191 (topology without pointed types)
- Zachary cannot be here but it seems that preserving backward-compatibility is beyond our resources
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)
- move signed.v and constructive_ereal.v to classical?
- question about patch in issue 1100
  - this is done in this PR: https://github.com/math-comp/analysis/pull/1246/
- about the semi_ prefix in measure.v issue 1072
floor, ceil, etc. subsumed by MathComp:
- PR 1244
work in progress about measure.v:
- following the introduction of sigma-rings PR 1222
- merge PR 1251?
- setD_closed vs. setDI_closed PR 1243
PR triaging:
- merge the Banach-Steinhaus PR?
- to_set vs. xsection PR 1248
- easy corollary to FTC1 PR 1250
- new Zorn's PR 1198 (stalled by lack of time)
- input wanted about Lp-spaces PR 1230

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