2023 12 21 Meeting - math-comp/analysis GitHub Wiki

Participants: Alessandro, Georges, Pierre, Quentin, Reynald, Takafumi

which keywords to add to opam files?
- see PR 1125
about the release of MathComp-Analysis 1.0.0
- the documentation of the HB branch needs to be updated
- main problem is topology.v
- shall we release 1.0.0 without the doc updated?
  - no
- what to do for topology.v?
  - put the list of structures first
  - then put the notations
- TODO:
  - Reynald will do a first pass (before the end of next week)
  - Takafumi will do a second pass (interested in documented filtered types)
- hard deadline for the release: mid-January 2024
release of MathComp-Analysis 0.6.7 before Christmas
TODO: issue about the funny title (* The algebraic part of the algebraic hierarchy *)
- see PR https://github.com/math-comp/math-comp/pull/1144
PR by Takafumi https://github.com/math-comp/analysis/pull/1117
- Zorn's variant:
  - localized version where the maximal element is taken over a given point
  - stated for relations in Prop
  - stronger than the original Zorn's lemma
  - no link with the Zorn lemma by Georges
    - the latter is a bit stronger because it is localized to subsets
    - only require a preorder and not a partial order
      - similar to the already present ZL_preorder in fact
  - Quentin has ported Georges' Zorn's lemma
  - there is also Zorn_bigcup
    - NB(rei): used in ex_maximal_disjoint_subcollection which is used in Vitali's lemma
- maybe derive the Prop version from the bool version
  - but this require PR #1119 first...
- Conclusion: issue postponed
PR #1119 (adding a contraposition tactic)
- quick demo by Quentin
- Georges had a work about the implementation
- Quentin has a couple of TOTHINK
  - do not use exfalso for consistency
  - 8.12 issue still need to be addressed
- MCA is adequate because it is a tactic for a Prop irrelevant setting
  - it would require more work for a MathComp version
- TODO: Quentin to complete the PR with the doc so that it can be reviewed lightly in January
making classical a standalone library
- idea by Yves for use in liberabaci among others
- coq-mathcomp-classical is already a package
- TODO: Takafumi to come up with ideas to improve the presentation of the webpage
- recorded as issue https://github.com/math-comp/analysis/issues/1126
documentation using coq2html:
- here is a PR that does minimal changes https://github.com/math-comp/analysis/pull/1108
  - TODO: pierre to double-check
- the result can be seen: https://yoshihiro503.github.io/coq2html/
- still a few bugs but it does not use sed and allows for markdown
- drop coqdoc for the next release?
  - yes
- other issue related to documentation: https://github.com/math-comp/analysis/issues/1071
- rename to rocq2html?
- TODO(rei): contact Xavier
PR triaging:
- https://github.com/math-comp/analysis/pull/1029 (adapting) -> Pierre?
  - closed (problem forgotten, not needed anymore apparently since CI is happy)
- https://github.com/math-comp/analysis/pull/1121 (lim sup)
  - TODO: review asked to Zachary
- https://github.com/math-comp/analysis/pull/1083 (radon nikodym chain rule)
  - TODO: Quentin will take a quick look (keeping in mind that we have extra notations for HB on Coq 8.14 and 8.15 and that we might need a notation for ae_eq)
  - TODO: will also ask Zachary afterwards
- https://github.com/math-comp/analysis/pull/1122 (easy fix but that raises the question of the status of forms.v)
  - try to remove mulr_rev in favor of R^C (put R^C in the canonical, cast one of the arguments to the converse ring)
  - Takafumi: is there a morphism defined from R to R^C?
    - Shouldn't be too hard
Poll for the next meeting: https://framadate.org/XMI2ZG5hAIoNdhjD