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

Assia will send a poll to find a new slot for the calls.
Yves provides some feedback about PR #346, after his discussion with Karl. They propose to ultimately merge the code proposed by Georges, after having improved documentation. This is a milestone for release 1.12.
There is discussion about nix+opam, but not about the documentation by Cyril, because he is not connected. Feedback on nix-shell mostly from Reynald, Enrico, Erik. Packaging with nix is documented on coq-community but mostly from a CI perspective. Information is hard to find for setting up one's own package. Opam works reasonably well on packages for main branches (with a few issues though). But nix is nice (> opam) for working with experimental branches and/or with libs depending on other coq libs (e.g. mathcomp-analysis, hierarchy-builder, apery). Enrico says the dream would be to factor the generation of meta-data + PRs between opam and nix, but we are not there. Related experiments include an opam to nix metadata converter by F. Bobot. This would be more relevant as a topic for a Coq Call: let's discuss this again in an MC call, so that we make sure there is followup.
Reynald draws the attention on PR #504. Assia suggests to merge and open issue(s) in repositories where similar refactoring would be relevant. Reynald mentions that issue #436 contains the specification in English of what it is about (as far as I can tell it is not referenced in the PR #504 discussion thread?). Conclusion : merge (milestone for 1.11) and advertise (by release managers), e.g. on zulip, and call for volunteer to propagate the refactoring.