Stream: math-comp users

Topic: mczify for mathcomp 2.0


view this post on Zulip walker (May 15 2023 at 09:09):

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.

view this post on Zulip Pierre Roux (May 15 2023 at 09:12):

MCzify is not yet released for MC 2.0, the process is still in progress: https://github.com/math-comp/mczify/pull/39

view this post on Zulip walker (May 15 2023 at 09:15):

would there be a way help (as non mathcomp expert) ?

view this post on Zulip Pierre Roux (May 15 2023 at 09:18):

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: Jul 25 2024 at 16:02 UTC