Usefulness and recommended use of Coq projects in coq-community

[palmskog]

Currently, it is not a requirement for a project hosted in coq-community to be useful, or at all suitable for wider use. For example, one of several sufficient conditions is that

the initial author has stopped maintaining the project and someone else is volunteering to do so

It is recognized that some projects will be lower quality than others, and perhaps not be suited for general use, e.g.,

some editorial work will be also required to put forward the most interesting packages, be it for their usefulness as a library or plugin, because they demonstrate interesting proof techniques, or because they represent an important achievement. This work will be done by an editorial board [...]

No such editorial board is in place yet.

@ejgallego recently raised concerns about the usefulness of the Bits project, and argued that it should be removed [from coq-community]. Here are the key parts of the conversation, which should be continued here.

@ejgallego on 2020-02-04

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

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 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 on 2020-02-05

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

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

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.
Best option to me still seems its removal.

[palmskog]

Personally, I wouldn't at all mind if some coq-community projects got a badge/marking like some research artifacts do:

• reusable / recommended for reuse
• usable
• experimental / not recommended for reuse

But I'm firmly against adding a requirement for coq-community projects to be reusable/recommended.

[ejgallego]

But I'm firmly against adding a requirement for coq-community projects to be reusable/recommended.

I'm not sure I follow here; the goal of CC is "A project for a collaborative, community-driven effort for the long-term maintenance and advertisement of Coq packages."

The aforementioned package is very hard to maintain without a full rewrite and should not be advertised; thus I don't see how it does fit that criteria.

[palmskog]

@ejgallego I don't think maintainability or "fitness for advertising" for included projects can in any way be derived from the current stated goal of CC. The manifesto currently gives four in-themselves-sufficient criteria for inclusion:

1. the initial author has stopped maintaining the project and someone else is volunteering to do so;
2. the project has become a collective work (several community members are actively working on it);
3. the initial author is still maintaining the project but they want to encourage other community members to participate in the maintenance and possibly take over (and the project is indeed raising interest from the community);
4. the project is a tool of general interest and it makes sense to develop it collaboratively.

Only the fourth can in some way be said to directly relate to maintainability/advertisement ("of general interest").

As for why I don't mind hard-to-maintain projects, there are many proof engineering research tasks where such projects can still be useful, e.g., as a comparison point for better libraries, for a machine learning dataset, ...

Finally, the fact that we aim to do advertisement for packages doesn't mean we always do the same kind of advertisement for all projects (hence the badges).

[anton-trunov]

On top of everything said I can add that I don't mind having a special place (a dedicated GitHub organization or something like that) for paper artifacts or adding badges and/or disclaimers.

[ejgallego]

@palmskog I just copied what the Coq Community page says.

[ejgallego]

Anyways whatever are the semantics, we are doing users a disservice by having a repos with so many known problems here; they will see this project and try, only to lose a large amount of time.

[palmskog]

@ejgallego but how do you go (logically) from CC being "a project for maintenance" to that Coq packages "hard to maintain" should be excluded?

[palmskog]

we are doing users a disservice by having a repos with so many known problems here; they will see this project and try, only to lose a large amount of time.

I don't think we are anywhere near having significant problems with many people trying out coq-community packages and failing to use them. I'm sure we can look into this again when we have 50+ projects and many complaints, though.

[ejgallego]

Even having a single person lose a few hours due to oversight on our part is not acceptable to me.

[ejgallego]

@ejgallego but how do you go (logically) from CC being "a project for maintenance" to that Coq packages "hard to maintain" should be excluded?

Projects that have no hope of becoming usable should not be here; so far the only motivation for this project appears to be preservation of an artifact; this is IMO out of the scope for CC.

[palmskog]

Projects that have no hope of becoming usable should not be here; so far the only motivation for this project appears to be preservation of an artifact; this is IMO out of the scope for CC.

This is very much a hardliner stance to me, and I've already argued against it above. I can tell you that, independently of Anton's goals for the project, my collaborators and I are already using Bits for proof engineering research. I also doubt that most CC members would agree with such a restrictive policy, but I'm sure we can arrange to poll them at some point.

@Zimmi48 maybe you can weigh in on this topic?

[Zimmi48]

Karl's explanations about what coq-community is and what it isn't are spot on. A claim in Emilio's message is that being in coq-community implies a project is maintained. That isn't true. A project needs to get a volunteer maintainer to join, but it can stop being maintained because the maintainer steps down and no one takes their place. We won't eject such projects, although we'll properly mark them as unmaintained. Coq-community contains other examples of unsuitable projects (e.g. exact-real-arithmetic is even marked as unsafe). The debate in the case of coq-bits should not be whether it belongs to coq-community but whether it should be in the package index or not.

[anton-trunov]

I wouldn't oppose removing coq-bits from opam. I added it there just because it used to be on opam.