[opam-devel] Using OPAM as the Coq packages manager
anil at recoil.org
Mon Oct 27 11:20:19 GMT 2014
On 27 Oct 2014, at 09:24, Guillaume Claret <guillaume at claret.me> wrote:
> The Coq theorem prover is facing the same challenges as OCaml to distribute and share its contributions. OPAM is a successful initiative for OCaml, so we would be pleased to use it as well. Thanks for this software.
> Things are still in development and not publicly released, but here are what we have for Coq:
> * a website: http://clarus.github.io/coq-eggs-test/
> * a bench system: http://coq-bench.github.io/
> * four repositories:
> * stable packages: https://github.com/coq/repo-stable.git
> * beta packages: https://github.com/coq/repo-testing.git
> * development packages: https://github.com/coq/repo-unstable.git
> * development versions of Coq: https://github.com/coq/repo-coqs.git
> Something we wonder is how to prevent name collisions with the OCaml packages. Some kind of namespace would be the solution. As a convention, we propose to use the ":" separator, like in Docker. So a package on the Coq repository would be of name: "coq:ssreflect" instead of just "ssreflect". We could go even further and use the "coq:big-project-name:small-part-of-it" scheme for big projects.
Sounds sensible to me. I'd probably keep the : convention unambiguous though. You can also use the 'tags' field mark Coq packages specifically. This will let you merge remotes with OCaml and still filter to Coq-only packages.
> Do you think it is a good practice and will the ":" symbol remain handled in names by OPAM? Could we reserve the "coq:" prefix on the OCaml repo to make sure no one is allowed to publish a package with this prefix?
Sure; by 'reserve', the repository mergers will flag up any Coq packages to you before taking any action. Is there a mailing list for the Coq/OPAM effort? You're welcome to continue to use this one from my perspective...
What sort of automated testing would be useful for you? We have a growing amount of infrastructure that does automatic building, but triaging errors is the current bottleneck.
Louis had some prototype code for compilers-as-packages that may help improve this integration in the future. For now though, OPAM 1.2 looks good for your needs with some careful metadata management, I think.
More information about the opam-devel