Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

opam package categories, logpath and dates are treated as regular tags #7

Open
palmskog opened this issue Dec 25, 2024 · 0 comments
Open

opam package categories, logpath and dates are treated as regular tags #7

palmskog opened this issue Dec 25, 2024 · 0 comments
Labels
packages About the Rocq Opam Packages

Comments

@palmskog
Copy link
Contributor

As per CEP 3, the Coq opam archive has the following special fields under tags:

  • logpath that states the Coq logical path prefix, e.g., mathcomp.ssreflect
  • category that has a limited number of possible values, e.g., Miscellaneous/Coq Use Examples
  • date that has the release date like 2024-12-25

However, all of these are treated like regular tags on the website (which they clearly are not) and we get links like https://rocq-prover.org/packages/search?q=tag%3A%22logpath%3Amathcomp.ssreflect%22

I also think the keyword part should be stripped from tag links, i.e., the keyword entries are our actual tags.
@palmskog palmskog added the packages About the Rocq Opam Packages label Dec 25, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
packages About the Rocq Opam Packages
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@palmskog