Release compatible with analysis 1.7.0

[proux01]

@4ever2 @sertel apaprently the latest 0.2.1 release of ssprove is not compatible with the latest 1.7.0 release of analaysis, any plan for a compatible release?

[4ever2]

I will look into it later this week and make a release compatible with analysis.
It looks like the analysis package split broke a few imports.

[sertel]

@4ever2, thanks for taking a look.

[proux01]

It looks like the analysis package split broke a few imports.

This should only have moved files, not renamed anything so From mathcomp Require foo should be a backward compatible solution (and is the recommended way to do any mathcomp import in any case).

[4ever2]

SSProve depends on distr.v which was moved to mathcomp-experimental-reals but SSProve doesn't depend on this new package.

[proux01]

Apparently adding the dependency is enoug to make it work: rocq-community/coq-nix-toolbox#289
Thanks!
I let you either close this or update your README/package files/whatever with the new dependencies before.

[proux01]

Hum, apparently I misread the CI result, this is not yet fixed: https://github.com/coq-community/coq-nix-toolbox/actions/runs/12007908356/job/33469475445?pr=289
Sorry

[4ever2]

The remaining issues were already fixed. Main branch compiles with mathcomp-analysis 1.7.0 after added the missing dependency.

[sertel]

@proux01 , I suppose you would need a new release version (for the according update in nixpkgs)?

[proux01]

Yes please (I can then take care of the nixpkgs update)

[sertel]

@4ever2 , would it be possible to merge my pending PR and then do the new release, please?
(I just merged in your latest changes.)

[sertel]

Thanks a lot for taking care of the nixpkgs update, @proux01.

[4ever2]

@sertel Yes, will merge it and make a new release once I'm done porting SSProve to Coq 8.20

[4ever2]

SSProve 0.2.2 is released now.
NixOS/nixpkgs#359596

We will need to add mathcomp-experimental-reals as a dependency once mathcomp-analysis 1.7.0 is on nixpkgs