Reintroduce coq-bits as coq-community project

[anton-trunov]

No description provided.

[palmskog]

@anton-trunov allowing dev packages as dependencies for a released package feels a bit shaky for the long term. I guess I'm fine with it for now, but if we saw a lot of these I feel we could build up a future maintenance burden.

[anton-trunov]

@palmskog Right. Thanks for merging.

[ejgallego]

I'm surprised to see this library has been added to coq-community; IMHO it is not suitable for use, also the code is using some ssr anti-patterns that makes maintenance very hard.

[anton-trunov]

@ejgallego I only discovered ssrbit after I had ported coq-bits to the recent Coq versions. Basically, the main purpose was to preserve this project because it's a paper artifact. https://github.com/artart78/coq-bitset builds on top of coq-bits, but I didn't have time to port that one too.

[ejgallego]

As you may know I had some discussions with the authors of these libraries; I guess it is subjective but IMHO I'd recommend people not to use these libraries due to some issues, so I'm not sure they belong to a set of curated packages [IMHO using them will cause quite a bit of pain]

Unfortunately we didn't finish srrbits yet, so I dunno what the best approach would be here.

[anton-trunov]

I used coq-bits in a small unpublished project to verify safe arithmetic operations and it worked but indeed I agree with you that it was painful. I had an intern trying to port the project to ssrbits, but he reported that some stuff were missing so he couldn't do the port (and he didn't have enough time to add the missing features).

I hope to contribute to ssrbits and when it's feature-equivalent we can redirect people from coq-bits to ssrbits. Do you think this would work?

[ejgallego]

I hope to contribute to ssrbits and when it's feature-equivalent we can redirect people from coq-bits to ssrbits. Do you think this would work?

I think it would work, but there is a blocker in terms of that actually it is not clear what one would want from such a "bits" libraries; indeed doing a library is not so different from just using standard math-comp's modular arithmetic.

I think other people was interested in this kind of library, so indeed if we could all agree on what kind of interface such a library should offer, then I'd guess we would be able to complete it pretty quickly.

[palmskog]

@ejgallego to my knowledge the (sole) goal of coq-community has never been to curate a collection of projects suitable/recommended for "general use". This goal makes much more sense for the Coq platform.

To me, a nontrivial artifact for a research paper is for sure over the threshold for inclusion in coq-community - but please open a coq-community manifesto issue if this needs further discussion. Projects can of course come with disclaimers about usability and practical relevance in the README.

[ejgallego]

@palmskog I see, thanks for the clarification; on the other hand keeping a project on Coq community keeps the project maintained, which gives the impression that the project is still developed and may be used.

Seems surprising to me that coq-community would have as a goal preservation of research artifacts, IMHO there is no point in updating quite a few of these artifacts [for example experiments such as coq-bits that are not suitable for further use] versus just keeping them in a VM / Docker image.

[anton-trunov]

@ejgallego Would it work for you if I put something like the following in README.md?

There is a work-in-progress library that aims to supersede the Bits library:
https://github.com/ejgallego/ssrbit

If it's not precise enough, I'm fine with anything you might suggest.

[ejgallego]

I dunno what to write, ssrbits has their own problems, so I'm not sure pointing out to that library is the right choice.

"This library should not be used unless you know what you are doing" would fit better what I think, however we cannot just write that. I dunno.

[ejgallego]

Best option to me still seems its removal.

[palmskog]

I opened a coq-community issue for any further discussion, so let's not continue here: coq-community/manifesto#93