Skip to content

Split released OPAM packages

The following discussion from !257 (merged) should be addressed:

Pierre (@proux):

If we merge this I should update the OPAM packages on https://coq.inria.fr/opam/extra-dev. The one on https://coq.inria.fr/opam/released should be "updated" only for the next release.

Note that the name of the packages is opened to discussion, we could for instance have:

  • coq-prosa-core
  • coq-prosa-poet (dependeing on coq-prosa-core)
  • potentially coq-prosa as a virtual package depending on all other

or any other combination

Björn:

Ok, that means we’ll have to update the POET instructions when making the next stable Prosa release.

Pierre:

Actually, there is no obligation to split the package on the repo.

But I tend to think it's nice to offer more flexibility to users who may be not be interested in the refinements part and don't want to install all of mathcomp and coqeal.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information