uwplse/StructTact

generally-avialable opam package

vzaliva opened this issue · 3 comments

vzaliva commented

Currently, it requires using https://coq.inria.fr/opam/extra-dev which holds some
other experimental code I do not want to use. Would it be possible to make
it available via the default coq opam repository?

palmskog commented

Thanks for the interest. The main problem is that making releases takes additional continuous work for which there isn't any time budget right now. One workaround is to directly pin the package based on the repository URL. I aim to ensure the repository opam file always works.

When dune support for Coq stabilizes (hopefully mid-2020, but possibly earlier), we will use dune-release to automate releases.

vzaliva commented

Sorry to hear that. I was hoping that his package should be relatively low-maintenance as it includes only tactics, and already packaged in opam.

I did not know it is possible to pin a single package from a repository. I was afraid if I add extra-dev to my opam, an opam update/upgrade will install other experimental versions of packages I am using. How can I pin just one package from that repo?

palmskog commented

Here is what I meant you can do, which doesn't add any new opam repository:

opam pin add coq-struct-tact https://github.com/uwplse/StructTact.git -k git

This will use the package definition that is in the git repo on GitHub.

  • 👍1