[opam-devel] Using OPAM as the Coq packages manager

[Anil Madhavapeddy]

On 27 Oct 2014, at 09:24, Guillaume Claret <guillaume at claret.me> wrote:
> 
> Hi,
> 
>  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

Nice!

>  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.

-anil