Minutes June 02 2020 - math-comp/math-comp GitHub Wiki

  • About nix shell for MC.

    • Any feedback? Not for the moment.
    • Cyril plans to test this procedure in CI using GH actions

  • No Coq call, no feedback on the nix-opam bridge

  • About PR relevant for 8.11

    • #516 shall be ready by tomorrow, issue with minr/maxr that are to be deprecated, 2 missing lemmas
    • #513 is ready
    • #514 is morally a bigfix, some more lemmas are missing (Cyril will submit an issue with this list #518)
    • release by the end of the week (possibly Thursday)

  • About the wrong tag 1.11.0+beta (should be 1.11+beta). Cyril: not to be removed since tools may crash. Maybe update the Release HOWTO to avoid getting it wrong again.

  • Beta:

    • not much feedback by the external user
    • gave a impulse to Cyril to bump the dependency on many related projects. In turn this discovered a few issue he is fixing in the final.

  • CI:

    • pr odd-order #16 to enable easy GH actions based (using the usual docker images)
      • suggestion to merge without testing MC-dev on Coq < 8.10, since these images will shortly fail to build due to PR #501
    • template is taken from coq-community, very easy

  • About #501/#502