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

Louis Gesbert louis.gesbert at ocamlpro.com
Tue Nov 4 06:48:10 GMT 2014

Le lundi 27 octobre 2014, 10:24:12 Guillaume Claret a écrit :
> 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.

Knowing that OPAM is successful also for managing Coq packages will make me very happy. Please share on your experience and possible improvements !

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

Sounds like a neat idea, and I don't see how that could become a problem. It'll just be slightly heavier for handling Coq packages I guess.

On the compilers-as-packages: what that would allow you to do is define, on the coq-eggs repo, "compiler" definitions which are just a reference to a given OCaml package and a given Coq package. This'll give you more stability (Coq won't change version or be recompiled) and make the coq dependency implicit in all packages.

The usage would be a bit different in this case: coq-eggs would become a self-contained repo rather than stack over the default OPAM repo for OCaml, and you could even rely on an external OCaml compiler and just specify Coq as "compiler". For this you might actually want a specific OPAM instance and opam root, e.g. ~/.coq-opam, that may coexist alongside an OCaml's ~/.opam.

Not sure how that would be an improvement on the current repo though, I'd be happy to know what you think. 


More information about the opam-devel mailing list