Skip to content

2023 12 21 Meeting

affeldt-aist edited this page Dec 21, 2023 · 1 revision

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

  • which keywords to add to opam files?
  • 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 *)
  • 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
  • documentation using coq2html:
  • PR triaging:
  • Poll for the next meeting: https://framadate.org/XMI2ZG5hAIoNdhjD