2021 03 26 Meeting - math-comp/analysis GitHub Wiki

Participants: Marie, Kazuhiko, Pierre-Yves, Cyril, Reynald

• about https://github.com/math-comp/analysis/pull/334
  • TODO: Marie does the dispatch and we will merged
  • dense goes to topology.v
  • floor_nat_comp should use ceiling (or trunc?) TODO: Reynald to give the pointer to Marie
  • definitions in sections should stay there with possibly a comment
  • mention as a comment that this should be generalized to vector spaces?
• about https://github.com/math-comp/analysis/pull/337
  • low priority because nobody using it at this point
  • treatment of functions as predicate is different from what is done in the library
    • should be uniformized
  • many things can be reused from the library (e.g., contra lemmas)
• about https://github.com/math-comp/analysis/pull/294
  • might be heading for a merge despite that fact that improvements shall come later
• about https://github.com/math-comp/analysis/pull/311
  • heading for a merge
    • refactoring still need though, Cyril to look at it
  • one issue is the notion of restriction it introduces which is competing with fer
  • should it use pointed types for patch?
    • so that patch does not take a default function anymore
    • but this approach is not without problems
  • we should maybe adopt this definition
    • specialize when we are on a ring, in the manner of nth which is specialized to 0
    • here, the zero would be the constant zero function
  • TODO: try to replace fer by this PR definition
• about PR https://github.com/math-comp/analysis/pull/318
  • might need to hear from the author
• status of PR https://github.com/math-comp/analysis/pull/116
  • in progress
• status of PR https://github.com/math-comp/analysis/pull/180
  • try to recompile it now that PR #205 has been merged
  • heading for a merge
• about PR https://github.com/math-comp/analysis/pull/358
  • the computational contents should not be relevant
  • a priori no reason to use Defined instead of Qed
    • test whether it is true and merge
• about issue https://github.com/math-comp/analysis/issues/348
  • agree to use bar R instead of the notation {ereal R}
• merge the PR fixing issue https://github.com/math-comp/analysis/issues/323
  • this is probably the result of a bad merge
• agree to release 0.3.7 asap
• TODO: try to schedule the next meeting at 2pm Paris Time
  • ask about https://github.com/math-comp/analysis/pull/318