Minutes March 12 - math-comp/math-comp GitHub Wiki

About the beta:

• Cyril: if you use numDomain or up, you get breakage
• Yves is OK with it
• Dates:
  • beta: work starts around 20 march, released end march
  • final: may?
    • no major changes in master in between
• we need to make a docker image for the beta, and an opam package as well
  • docker is now part of the release process
    • it went smooth last time
  • we are reaching the limit number of images that we can automatically build on docker hub (25 according to this page)
    • we may need to remove images for MC 1.7
• Georges has a huge change about predicates on a finite support, but it is not for this release

Erik on CI:

• a few PR are stuck and should be merged: PR #455 and PR #465
  • Cyril looks at them
• cleanup the GitLab temporary images:
  • repository to be moved in gitlab.com/math-comp
  • containing a script that can be run by GitLab CI
  • GitLab (bot) user will run the script on a regular basis
• CI is currently broken (coq.dev + MC.dev + finmap.dev)
  • Kazuhiko is working on a fix
  • lemma overloading was removed from CI since it is broken by Coq, not MC

Doc:

• GH let's you add a page named sidebar that is always rendered as a sidebar
• Cyril looking into it

The history of MC disappeared from the forge:

• Enrico: I think it is still there but not linked, I'll look into it

Next meeting: 27 March at 11AM