platform Add MathComp Word to the Coq Platform

MathComp Word is a Coq library on machine words based on Mathematical Components. It is a core dependency of SSProve (a candidate to join the Platform) and other projects such as the Jasmin compiler. Machine words are a frequently formalized concept useful in many verification projects.

To allow SSProve and other projects to more easily use MathComp Word, and based on this discussion on Zulip, I propose that MathComp Word is added to the Coq Platform.

The primary maintainers of MathComp Word are @vbgl and @strub. In accordance with the Platform package inclusion process, we would like for them to comment here that they agree on including the library. In practice, this means committing to making a Git tag for every major Coq release in the GitHub repository (this tag is then ideally packaged in Coq opam repository).

cc: @spitters @gares (can this package use the coq-math-comp- prefix?)

Jul 18 '22 15:07 palmskog

Fine with me.

Jul 18 '22 20:07 strub

I agree that this library be included in the Coq Platform.

Jul 19 '22 04:07 vbgl

@vbgl @strub thanks! I think this means we can get the library into the next Platform release this fall, but @MSoegtropIMC who is currently unavailable, will have to confirm later.

In the meantime, is it OK with you if I package release 1.1 in the Coq opam archive? From what I can tell, it's compatible with 8.16 and MathComp 1.15, so I would adjust bounds accordingly.

Jul 19 '22 10:07 palmskog

is it OK with you if I package release 1.1 in the Coq opam archive?

It is OK.

Jul 19 '22 11:07 vbgl

coq-mathcomp-word.1.1 is now out on the archive and marked as compatible with 8.16 and MC 1.15, per https://github.com/coq/opam-coq-archive/pull/2239

For uniformity with other MathComp-related projects, it may be a good idea to change the logpath to something like mathcomp.word rather than the current CoqWord.

Jul 19 '22 12:07 palmskog

@strub : I would appreciate if there would be a Readme.md file in (https://github.com/jasmin-lang/coqword), so that people see what this is good for. There is no need to tag it - it is sufficient if it is available in the main branch.

Aug 08 '22 08:08 MSoegtropIMC

Ok. I added a minimal README.

Aug 08 '22 09:08 strub

Thanks - it is clear and to the point.

Aug 08 '22 13:08 MSoegtropIMC

@strub : there is a new version in opam (https://github.com/coq/opam-coq-archive/pull/2342). Since I am delayed a bit with Coq Platform 2022.09 (but about to release) I wanted to ask if I should update to this version. I need a really quick answer.

Oct 05 '22 10:10 MSoegtropIMC

Yes, you can take the last version.

Oct 05 '22 10:10 strub

@strub : thanks for the quick confirmation. I updated to 2.0.

Oct 05 '22 13:10 MSoegtropIMC

@strub: actually the new versions breaks coq-mathcomp-algebra-tactics there is a name conflict about file ssrZ with zify:

===============================================================================
/Users/runner/.opam/log/coq-mathcomp-algebra-tactics-66058-b80608.out
===============================================================================

    42	File "./theories/ring.v", line 5, characters 0-39:
    43	Error: Required library ssrZ matches several files in path (found
    44	/Users/runner/.opam/__coq-platform.2022.09.0~8.16~2022.09~beta1/lib/coq/user-contrib/mathcomp/zify/ssrZ.vo and
    45	/Users/runner/.opam/__coq-platform.2022.09.0~8.16~2022.09~beta1/lib/coq/user-contrib/mathcomp/word/ssrZ.vo).

I will revert to the previous version.

Oct 05 '22 16:10 MSoegtropIMC