Please remove the copy of ssrZ (or rename it)

[MSoegtropIMC]

@strub : the change in the install path in b94f002 from CoqWord to mathcomp/word (afair it was suggested by @palmskog) has the effect that other packages which do a From mathcomp Require ssrZ now fail, because there are two ssrZ files under mathcomp:

# Error: Required library ssrZ matches several files in path (found
# /home/runner/.opam/__coq-platform.2022.09.0~dev/lib/coq/user-contrib/mathcomp/word/ssrZ.vo and
# /home/runner/.opam/__coq-platform.2022.09.0~dev/lib/coq/user-contrib/mathcomp/zify/ssrZ.vo).

This is really quite bad since ssrZ is a common thing to require.

I don't know why you copied ssrZ. If it is just for convenience / historic reasons please consider removing it and installing zify via opam. Otherwise please rename it.

In Coq Platform I am still using version 1.1 for the reason as mentioned here

[palmskog]

There is quite a lot of overlap in the content of these two files, so the ideal solution would be if both projects consolidated what they need in MathComp itself. However, since MCZify is expected to be used in more places (due to its status as "proof automation package"), maybe ssrZ in coqword could be renamed to something like ssrZutil in the meantime?

[strub]

I don't know why you copied ssrZ.

Looking at the history of both files, assuming 2017 < 2021, should invalidate this statement.

[strub]

IMO, the simplest is to remove ssrZ. It may be that we can rely on mczify only. Will investigate.

[MSoegtropIMC]

@strub : sorry, I should have properly investigated this - I am a bit under water with breakages in Coq Platform these days.

[palmskog]

@strub any update on plans to rely on ssrZ from mczify? Also, I would like to ping in @pi8027 for an opinion on how to best resolve this namespace collision - could some results from ssrZ in this repo be moved to mczify maybe?

[strub]

I managed to remove nearly all the contents of thus file. I al not sure it is worth consolidating anything then.

[palmskog]

That sounds good to me, then all that may be needed is to rename the file with the remaining code (and start to depend on coq-mathcomp-zify). Please flag up when there's a new release with this content, and we'll make sure it ends up in the next Platform release.

[pi8027]

At least I would say it would be nice to have only one source (library) of structure instances for the standard binary integer type Z. Otherwise, we may face an issue that instances provided by different libraries are not convertible. As the author of the Mczify library, I hope Mczify is the right place to provide such instances (because otherwise, Mczify has to depend on another library).

[eponier]

What is the status of this? #17 renamed ssrZ.v into word_ssrZ.v, but the proper fix in my opinion is to remove word_ssrZ.v, as mentioned here.

[strub]

The status is that we should implement this. #17 is a fix hack to solve the name clash issue.

[MSoegtropIMC]

Of course I would prefer a proper solution. If this is not possible in say 2 weeks, I would go with the hack, so that the proper solution can be done properly.

[strub]

I accepted your PR so that you can go with the hack.

[MSoegtropIMC]

Ah yes - and there is also a new tag. So all what is missing is that you confirm in #18 that this is the tag you want to see in Coq Platform. Sorry for this rather verbose protocol - it helps to avoid mistakes.