Minutes April 20 2020 - math-comp/math-comp GitHub Wiki

Enrico has the lock

• what about mc_1_9 mc_1_10: a bit more than aliases, they can contain lemmas with different types.

  • it does not print a warning
  • but requires explicit opt-in by the user
  • Enrico thinks their lifetime should be the same of deprecation aliases
  • open an issue for 1.12, leave them there for 1.11
  • they also seem to be unused on github

• we get the list of postponed to 1.12 in the topics for the next meeting

• Cyril announces a Zulip instance for MC and Coq (and you name it) will be available in the future: https://coq.zulipchat.com

  • ETA: end of April
  • data from gitter will be imported

• Setting up CI for Apery (it has some deps), how to?

  • it includes some extra for MC, orthogonal to CI
  • Erik: you should also add Apery to MC ci
  • the difficult thing is that Apery depends on some deps, and adding it to MC ci would require to have them in the loop as well
  • Erik has a much more complicated setup, will chat with Assia offline
  • Christian put his graph library in CoqCommunity using their default CI, and he thinks it would me more important to test against multiple MC versions, disregarding which Coq version (pick the latest)

• Christian on beta testing the latest release

  • there is an opam option to disable dependency checking and let you install what you want
  • should we upper bound deps on MC

• Cyril has some doc for MC with nix, planning to release it soon. Nix should solve some of the problems we have with opam