Agenda of December 11th 2019 meeting 13:00 to 14:00 - math-comp/math-comp GitHub Wiki

  • Big Operators over Setoids (issue #407)
  • PR #270
  • Organization of fortnightly mathcomp (= who does what when)
  • Is there a doc for installing CI? (might be out of place)

Minutes

  • Yves is volunteering to participate to the next 2 release to polish the documentation of the release process. We need to find a second person for each of them.
  • Big Operators over Setoids:
    • it could be an external library since the definitions of bigop are the same
    • replacing bigop lemmas with it could cause either compatibility issues (if there is a problem with setoid rewrite) or performance issues (if setoid rewrite does not notice that it could use substitution of Leibniz equality instead). However it is not clear there is a problem. We should make sure whether there is one or not.
    • it could be integrated by code duplication, and we could use the module to disambiguate between the leibniz and setoid versions.
    • we should make tests
  • PR #270
    • Decision to merge it. And fix potential bugs or improve later.