Minutes May 05 2022 - math-comp/math-comp GitHub Wiki

Participants: Reynald, Enrico, Cyril, Kazuhiko, Pierre

  • conclusion about PR https://github.com/math-comp/math-comp/pull/869
    • ok to merge
    • TODO: remember the custom entry proposal by Laurent as a feature request
  • report about rebase of HB port
    • see https://github.com/math-comp/math-comp/tree/hierarchy-builder-rebased
    • took half a day, without surprises, had to port a few instances (such as bounded sequences, done by looking at tuples)
    • Pierre does not have the rights to merge
    • Enrico gave the right for a temporary force-push
    • about the ssrnum problem:
      • Cyril and Enrico found a way to fix hb so that the current mathcomp hierarchy goes through
      • it should be possible to port mathcomp-analysis afterwards