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

[Guillaume Claret]

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

   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?

Thanks,
Guillaume