Coq releases opam

[clarus]

Instructions to install Coq with OPAM on the download page.

[herbelin]

Short remark in passing. When I do

opam info coq

I get:

version: hott
description: HoTT/Coq stable branch

How to do so that we have a more appropriate info about coq? Is this the responsability of the coq.hott package maintainer (no maintainer field actually)? Is this our responsability? Other?

Incidentally, the coq.hott packages is missing many important fields (ocaml, campl5, labgltk constraints, maintainer, authors, ideally homepage, ...).

[clarus]

I think you can do opam info coq.8.4.6 to get the information about another version. By the way, the hott version of Coq is not available in the standard repository.

[herbelin]

Hi Clarus and thanks for your comment. I think that my questions were two.

The first one was about the unclear output of "opam info" and I filled a feature request about it.

The second one is about the policy about submissions of coq packages. Who should we consider is responsible of ensuring the presence of enough fields in the "opam" file of a package? Who should we consider is responsible of the naming of the version of a package so that a package is considered at its due place in the preorder of version numbers?

[clarus]

Thanks for your feature request!

For now, the "mandatory" fields (like license or homepage) are verified by the lint.rb program.

No one is officially responsible of naming of versions, but I think we can expect people to be reasonable, at least for the beginning. For the coq.hott issue, we can maybe remove Coq versions which are not corresponding to tags or branches in the main Git repository.