math-comp
Upstream integration of ALEA changes
ALEA is now a maintained project in coq-community. Please consider submitting extensions and changes to ALEA from here to that repo so that the community can benefit.
Dear @palmskog,
This is a very good news. I'm using a very small part of ALEA, since I'm only dealing with discrete probabilities. However, together with Christine Paulin, we wrote some bindings between ALEA and mathcomp rationals which might by of general interest. I only maintained this part to have my code compile. It is probably very incomplete.
@hivert since ALEA is not a widely used package, I think it would be a reasonable idea to put the MathComp bindings directly into ALEA and have ALEA as a whole depend on MathComp.
However, the tradeoff for you would be that you have to depend on the ALEA package/project in the code here. We have done a lot of work recently to have continuous integration (CI) work well with external packages via opam (and Nix), but it's still a bit of work.
Maybe you would consider becoming a co-maintainer of the ALEA project in coq-community so you can make sure the MathComp bindings always work with Coq-Combi? If so, I can help set that up (and also help with CI here).