search

jasmin-lang / coqword

Yet Another Coq Library on Machine Words.
MIT License
9 stars 7 forks source link

Please remove the copy of ssrZ (or rename it) #15

Open MSoegtropIMC opened 1 year ago

MSoegtropIMC commented 1 year ago

@strub : the change in the install path in b94f0020377791cb3e1dbdc37731327f02b1355c 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 commented 1 year ago

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 commented 1 year ago

I don't know why you copied ssrZ.

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

strub commented 1 year ago

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

MSoegtropIMC commented 1 year ago

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

palmskog commented 1 year ago

@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 commented 1 year ago

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

palmskog commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

What is the status of this? https://github.com/jasmin-lang/coqword/pull/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 commented 1 year ago

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

MSoegtropIMC commented 1 year ago

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 commented 1 year ago

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

MSoegtropIMC commented 1 year ago

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.