Criteria for inclusion in the released repo - mark/exclude experimental packages?

[palmskog]

We currently use only the following criteria for inclusion of a package in the released OPAM repo/index (and some are not always fully enforced):

• Includes a Changelog that lists the main changes between any two versions part of this archive
• The License must allow free redistribution (even if it is not a free software license)
• No Admitted proofs
• All Axioms used are documented
• ML code is reviewed by a Coq developer
• Documentation should be available (see the doc: field in the Opam metadata)

However, @ejgallego has recently raised the general issue (and for the coq-bits package specifically) that some projects should be discouraged from general use due to, e..g., usability problems. Hence, they could either be excluded from the released repo or marked in some way, say, with keyword:experimental or even keyword:EXPERIMENTAL.

Personally, I don't mind enforcing an "experimental" tag like this, but I'm against excluding packages due to usability and similar issues, i.e., that we out of concern for potential users do not allow packages in released that otherwise conform to the above criteria.

Can other archive maintainers (@gares @clarus) give their opinions perhaps?

[Zimmi48]

This is theory. It seems to me that most of these criteria are never checked. In particular, "ML code is reviewed by a Coq developer" is wishful thinking. It would be good to focus on a smaller set of criteria that would be actually enforceable.

I would start with the two rules "All axioms used are documented" and "No Admitted proofs". We recently discussed these two rules with @ybertot and @Casteran. An idea was to have a standard format for expressing this. This is also related to coq/coq#10617: axioms could be separated into standard axioms and non-standard ones.

The changelog thing could be strongly encouraged and become actually enforced later on.

FTR I'm also against excluding packages out of usability concerns (because these are too hard to judge).

Excluded packages because they have Admitted proofs for instance have their place in extra-dev (whose existence is unfortunately poorly documented -- i.e. only in this repo's README).

[palmskog]

@Zimmi48 I completely agree about most criteria being theoretical. However, the only practical way to enforce the axioms-related rules I see is to find a way to check and flag up axioms in CI. Is it realistic to have coqchk with the right options do this currently (I assume your discussion with Yves and Pierre touched on this)? At least, we could begin by checking for "closed under context" or not.

[gares]

The page says "We advise package authors to make sure that the following conditions are met:" and "In any case the Coq development team keeps the right to refuse the integration of a package or remove any package at any time." So to me these are guidelines, and good excuses for removing packages. Not really things we have to enforce.

Anyway, the central question is about the quality of the packages part of the archive. It was discussed quite a few times in the past and the truth is that we lack knowledgeable manpower for doing it seriously. Evaluating the quality of a library is hard, much harder that looking at an opam file, and less consensual.
Who decides which package deserves the experimental flag? Is having more that 10 lines of ltac1 a sufficient condition? (I'm pushing it now, I hope my point is clear, we don't have golden standards for .v files).

Something that works fine in similar contexts and that is sort of addressing the issue without requiring a council of experts is a popularity meter, eg the number of downloads or +1/-1 clicks. If I had time (and fluency in web tech) I would have done it already.

[clarus]

I like the idea of having a very liberal approach with a minimal set of rules, like the opam lint + opam install work + license informations, to encourage people submitting. I think even admitted proofs can be fine as long as the authors judge this is useful enough to be published.

The page says "We advise package authors to make sure that the following conditions are met:" and "In any case the Coq development team keeps the right to refuse the integration of a package or remove any package at any time." So to me these are guidelines, and good excuses for removing packages. Not really things we have to enforce.

Good point to say we can always remove things in the worst case.

Something that works fine in similar contexts and that is sort of addressing the issue without requiring a council of experts is a popularity meter, eg the number of downloads or +1/-1 clicks. If I had time (and fluency in web tech) I would have done it already.

I agree with the popularity meters. I would say that the GitHub stars / commit activity can already give some insights for free. As an example, here is what it says on the npm page:

To me it is enough to let people find these informations given our time bandwidth.

[gares]

That is fine as a storage, but it should be more "integrated" with the package index I believe. This is the web tech thing I was talking about.