You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
experimental-reals: Superficial dependency on "analysis". #2145
Currently, the experimental-reals package depends on the analysis package, but this dependency is only superficial. experimental-reals depends only on the classical and reals packages, so its listed dependencies can be changed accordingly.
As far as I can tell, the change in dependencies requires no code change, so this update could be backported to old versions in opam and in nixpkgs. I have tested the change in nixpkgs here: MarkusKL/nixpkgs#1
I suppose that this might break existing developments that actually depend on both experimental-reals and analysis, but only has experimental-reals listed as a direct dependency.
I found this while looking into the dependencies of SSProve. Likewise, SSProve only superficially depends on analysis, but dropping the dependency will have no consequence until a change is made to experimental-reals. Dropping analysis as a direct dependency would mean faster compile times for SSProve including dependencies, especially in opam.
I would like to know if you think that this update should be applied and to what extend the changes should be backported. I will be happy to help create the pull-requests.
I think that there is now a true dependency: for example, realsum.v is using esum.v.
There is an on-going effort by @lyonel2017 to re-implement experimental_reals by taking advantage of theories is analysis that are a bit more general.
Introducing the dependency was a first step (that helped us getting rid of infamous Admitted's). See also PRs #2049 or #2063 or #2116 .
Right, thanks for the context. I just tested nix-build -A rocqPackages_9_2.mathcomp-experimental-reals and it fails as expected with the actual dependency as of analysis 1.18.0. I will just close this then.
Activity
affeldt-aist commentedon Oct 26, 2026
I think that there is now a true dependency: for example,
realsum.vis usingesum.v.There is an on-going effort by @lyonel2017 to re-implement
experimental_realsby taking advantage of theories isanalysisthat are a bit more general.Introducing the dependency was a first step (that helped us getting rid of infamous
Admitted's). See also PRs #2049 or #2063 or #2116 .MarkusKL commentedon Oct 26, 2026
Right, thanks for the context. I just tested
nix-build -A rocqPackages_9_2.mathcomp-experimental-realsand it fails as expected with the actual dependency as of analysis 1.18.0. I will just close this then.