This should say it all:
$ opam install coq-mathcomp-zify
The following actions will be performed:
↘ downgrade coq-mathcomp-ssreflect 2.0.0 to 1.17.0 [required by coq-mathcomp-zify]
∗ install coq-mathcomp-fingroup 1.17.0 [required by coq-mathcomp-algebra]
∗ install coq-mathcomp-algebra 1.17.0 [required by coq-mathcomp-zify]
∗ install coq-mathcomp-zify 1.3.0+1.12+8.13
It is also strange for two reasons, first I imagined that zify is dependency for mathcomp, but never mind that.
The second strange thing is according to this line, opam shouldnot be complaining about unsupported version.
MCzify is not yet released for MC 2.0, the process is still in progress: https://github.com/math-comp/mczify/pull/39
would there be a way help (as non mathcomp expert) ?
Well, as you can see, the port is done, it's mostly a matter of doing a release and the opam packages. So I'm not sure there is much more to do than waiting a bit to let the maintainers do their job. But thanks for the offer.
Last updated: Oct 13 2024 at 01:02 UTC