Open herbelin opened 8 years ago
Hi,
Does the presence of categories and keywords on most packages, as listed on https://coq.inria.fr/opam/www/ , solves your issue? Or would you like to specifically distinguish between these three categories?
Categories and tags provide the right infrastructure. However, the absence of any review of the tags and categories that packages add has made the thing completely useless and unusable. Someone should try to rationalize this thing. And the categories (or tags) "library", "plugin", "theorem" / "achievement" would still make sense to have, I think.
Does the presence of categories and keywords on most packages solves your issue?
I would rather think like @Zimmi48.
For the historical record, the categories used to be limited to a relatively restricted list: https://web.archive.org/web/20140813011527/http://coq.inria.fr/pylons/contribs/new But now that they are added manually in the opam file and not checked to belong to a restricted set, the number of categories has grown out of control. We could also try to take advantage of the slashes in category names to display them in a more condensed way, for instance using foldable lists.
I feel it would be useful to add tags such as
Libraries (e.g. corn, mathcomp-algebra, ...) Plugins (e.g. aac-tactics, mathcomp-ssreflect, ...) End result (e.g. godel, mathcomp-odd_order, ...)
Anyone interested in adding such an improvement?