Minutes April 19 2023 - math-comp/math-comp GitHub Wiki

Participants: Pierre, Reynald, Thomas, Yves

short presentation of what we expect to do in upcoming doc sprint

skipped

PR triaging

934 "renamings of long suffixes (fixes #933)"

  • it looks ready according to the discussions we had last time
  • let's merge

980 "Add notations \top and \bot and deprecate 0 and 1"

  • looks ready (we agreed to drop 8.13 and 8.14 last time)
  • found a comment with 0 and 1 that was not updated and a use of 0%O
  • should count_lt_le_mem be there? yes

987 "Adding recommendations about mathcomp 2 to the pull request template"

  • looks ready
  • TODO(rei): rm the last commit and rebase

994 fixing a warning in recent master

  • consequence of this PR https://github.com/coq/coq/pull/17205
    • NB: Georges initially disagreed because it conflicts with a pattern used often in MathComp
  • replacing Let with Local Lemma might not be a good idea because we have to restore the hints and the lemmas now appear in Search
  • use XYZ_subproof?
  • for the time being, maybe disable the warning globally

959 "Building finite fields using polynomial and irreducible polynomial"

  • what's the status?
  • TODO(rei): ping Laurent