In what version can I expect `math-comp`

to have `probability`

? I've been looking at 516 and 769 (latter being targeted at the 516 branch), and it'd be cool to use them on a current project.

Thanks for letting us know. Is there a result in particular you would like to see in master?

I was gonna say random variables but looking at it again I'm kinda willing to just `From mathcomp.analysis Require Import measure.`

and roll my own from there

looking at expectation code and lol I don't feel like rolling my own.

related, though: are you sure `probability`

should be in the analysis package? it seems more likely that `mathcomp-probability`

as a package that depends on `mathcomp-analysis`

may be better.... but I guess it'd be easy to refactor into such a thing in the future

That indeed sounds like something to consider.

(btw the next version of "mathcomp-analysis" will come as two packages, splitting can occur later as you said)

One point to consider is that new features added to mathcomp-analysis should have a reasonably stable interface since it is in Coq Platform "full" level. If some parts are from an interface point of view still in motion, this should either be clearly mentioned in the release notes, or it should indeed be released as a separate package, which then can be aded to Coq Platform "extended". I can't tell in how far this applies to the measure theory / probability additions and don't want to imply it does. This is just a point to consider when deciding what to put into separate packages.

I am also looking forward to have this added!

Analysis is becoming quite big and we can see use cases where a user would only need a part of it. That's why `mathcomp-classical`

will be a separate package in next release, containing parts of analysis about classical logic (with axioms). Similarly, there are other parts of the library that should either be integrated into mathcomp or put in separate packages in the future (classical real numbers or extended reals for instance). So yes, this is still likely to move a bit in the future. I guess there is a reason why Analysis is still version 0.sth

Another advantage of splitting up large packages is that for users it is more obvious what is there. But of course one should keep the (typical) nice side of single large packages: keep the design aligned.

Last updated: Jun 22 2024 at 15:01 UTC