Quinn (Oct 18 2022 at 00:42): Quinn (Oct 18 2022 at 00:42):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.
Reynald Affeldt (Oct 18 2022 at 01:01):Thanks for letting us know. Is there a result in particular you would like to see in master?
Quinn (Oct 18 2022 at 02:20):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
Quinn (Oct 18 2022 at 02:59):looking at expectation code and lol I don't feel like rolling my own.
Quinn (Oct 18 2022 at 03:01):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
Reynald Affeldt (Oct 18 2022 at 03:06):That indeed sounds like something to consider.
Reynald Affeldt (Oct 18 2022 at 03:09):(btw the next version of "mathcomp-analysis" will come as two packages, splitting can occur later as you said)
Michael Soegtrop (Oct 18 2022 at 06:44):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.
Michael Soegtrop (Oct 18 2022 at 06:48):I am also looking forward to have this added!
Pierre Roux (Oct 18 2022 at 08:31):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
Michael Soegtrop (Oct 18 2022 at 09:26):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: Apr 20 2024 at 00:02 UTC