cc: @Zimmi48 ; for future version of the coq language we could indeed drop compatibility with Coq makefile, then installing the corresponding dune-package files would allow us to properly recreate a package database.

Even so, the question on whether we should allow libraries names of the form foo.bar.mow where foo is a package is still unclear, maybe we should use for Coq a form foo+bar.mow or even foo.lib+bar.mow, or maybe separate package name from the point of insertion in the module hierarchy?

I dunno, the form of namespacing as used in the OCaml world should maybe something that Coq itself should be aware of.

I think it is OK to be stricter on what we accept. A Dune package should be packed under a single namespace, and this is already what is conventionally done in Coq packages.
I don't understand what you mean by "drop compatibility with Coq makefile". It is important to be able to depend on libraries / plugins that were built and installed with coq_makefile obviously, and it seems also that it should be possible to make a Coq package installable in the same way with Dune and coq_makefile (assuming it follows some restrictions).

I don't understand what you mean by "drop compatibility with Coq makefile".

In the 2.0 version of the language we could allow fancier rules; the current rules for Coq makefile install everything under a global directory [which can be several if you use COQPATH, but that is still one for Coq].

This is a bit inconvenient, as for example there are no proper ways to compartmentalize nested libs.

Something that bothers me is that we identifiy the module namespace with the library name. IMHO these are two conceptually different things, however I am not sure under this "1.0" scheme we can do better; after all, all that Dune can query is the directory tree on lib/coq/user-contrib

So yeah, even in the version 1.0 of the language it is not clear what a library identifier should be.

For example, using this convention we cannot install two libraries that provide the module namespace Data. This is IMO very limiting.

I think that a good start for a "2.0" version of the Coq language would be to adopt a 2-level similar naming scheme as in OCaml.

Thus, a library that is declared pkg.theory would be installed under lib/pkg/theory.

In the end I dunno, it is hard to know how things are going to work out until we don't try more; we don't have a lot of experience in this Coq context I'm afraid.

How can you, in OCaml, depend on two packages that provide modules under the same namespace? I personally feel like this is a very good practice to use namespaces that are reminiscent of the package name for less ambiguity. If you want a Data namespace, it can be nested, and with the right open or Import you can talk about it as Data.

How can you, in OCaml, depend on two packages that provide modules under the same namespace? I personally feel like this is a very good practice to use namespaces that are reminiscent of the package name for less ambiguity. If you want a Data namespace, it can be nested, and with the right open or Import you can talk about it as Data.

Oh, then we can go with this proposal to identify package name with its namespace for now.

In OCaml you cannot depend on two packages that provide the same namespace, but you can have indeed have virtual modules so for example, for namespace Foo you can have libraries foo-unix and foo-windows for example that will provide Foo.

That works because they are properly installed, however in the current Coq setup we cannot do that with the global namespace that is forced. The moment we break this discipline dune-produced packages cannot be use by coq-makefile users easily.

In OCaml you cannot depend on two packages that provide the same namespace, but you can have indeed have virtual modules so for example, for namespace Foo you can have libraries foo-unix and foo-windows for example that will provide Foo.

That works because they are properly installed, however in the current Coq setup we cannot do that with the global namespace that is forced. The moment we break this discipline dune-produced packages cannot be use by coq-makefile users easily.

Good point. I now understand what you mean by breaking compatibility and how we could wish to follow this route in the future. Virtual libraries are a nice concept that I would hope to support in the future (but we are far from it as we don't have interface files yet).

Virtual libraries are a nice concept that I would hope to support in the future (but we are far from it as we don't have interface files yet).

Yeah maybe virtual libraries are not the best name, but indeed with the current compat constraints we cannot do better. It is very unfortunate we cannot allow a better install for now.

I am not very comfortable going this way, but as long as we want to support the legacy install method I guess we'll have to leave with this. So let's make the 1.0 version use module names as namespaces and see what kind of workflow does people have.

In fact, as soon as Coq itself is moved to dune we could have the 1.1 version of the language with slightly more sensible rules.

Ready to merge IMO, thanks @rgrinberg