Naming scheme for Coq namespaces used by released packages

[palmskog]

As noted in coq-community/manifesto#98, some legacy projects use very generic Coq namespaces (logical path names, logpath in OPAM), such as Graph, Algebra, etc. Moreover, as new packages are added to the released repository, the available names for other packages shrink - namespaces for two different packages must be different, or they will clash in Coq's user-contrib directory.

To avoid issues with namespaces and directories in the longer term, I believe we need to come up with some guidelines or rules (possibly eventually enforced in CI) for package namespacing and organization. For example, @herbelin suggests in coq-community/manifesto#98 that Coq packages could be organized according to some existing classification such as that of ACM or MathSciNet.

[ejgallego]

Another idea that we would like to support in Dune Coq Language 2.0 is to actually don't install packages in the same directory user-contrib , but in their individual directories; this is a bit orthogonal but would help with such clashes as the would only add the packages to the include path if they appear in theories.

Ideas are most welcome regarding what model we would like; we can indeed add interesting rules IMO.

[gares]

Maybe we could try to impose ORG.PKG a bit lik java but shorter, or like vscose extensions. Eg lpcic.elpi, ejgallego.jscoq, math-comp.fingroup, MPI.iris. In this way you would get user-contrib.Algebra.

[herbelin]

My observation is that there are different needs:

• installation in the filesystem
• view in the logical namespace
• valorization as a library among the rest of libraries
• library search

Regarding the installation in the filesystem, the installation name does not really matter and it could continue to be on a first come first served basis, or on a org.pkg basis (as actually coq-contribs names were before this structure was flattened to comply with opam, using a city name as organization), or even just a number.

Regarding the valorization as a library among the rest of libraries, by which I typically mean a web page collecting the packages in a structured way, I believe we should eventually consider the structure to be a dag since a same package can be viewed from different perspectives. For instances, a library on reals is also relevant as a library on fields or a library on list is relevant as a library of finite sets, etc. A library from math-comp on fingroup is then relevant as much as a package on groups, as a package on finite structures, as a package developed by the math-comp organization, etc. This is where I was suggesting that ACM or MathSciNet can give hints on how to organize the logical namespace, like the categories, e.g. Computer Science/Formal Languages Theory and Automata, actually already do on the coq.inria.fr/opam/www page.

Regarding the logical name within Coq, an org.pkg structure (if not adopted also in the file system) might indeed be enough and relatively intuitive. After all, this is comparable to the authors.title description one can make of a book. For graph-basics, that could be ENSL.GraphBasics, or Duprat.GraphBasics; for graphs, that could be Dyade.Graphs. For GraphTheory, maybe could that be CoVeCe.GraphTheory if the authors like it, as the project was apparently supported by a grant of this name, or maybe something like GraphTeam.GraphTheory to insist on the ambition of the library.

An organization may evolve, get more partners, move, but then, new versions of the package can have different names reflecting this evolution. And conflicts on names in a given organization are then expected to be resolved at the level of this organization.

Incidentally, should coq-contribs and coq-community be considered as organizations? For at least coq-contribs, I would say no though.

Regarding search, the question is however different, where all kinds of information, contents, metadata are relevant.

So, in particular, if a logical level of indirection is available on top of the filesystem view, and that this logical level becomes the way everyone sees the packages, there would be no need to change the current first come first serve opam naming of packages.

And if not, we don't escape anyway to have to make a pass on the current names to set a new scheme.

[gares]

Incidentally, should coq-contribs and coq-community be considered as organizations? For at least coq-contribs, I would say no though.

Practically the only requirements for an ORG is that no two PKG exists with the same name in that ORG. Indeed an organization will rule the naming inside its space. In github an organization cannot have two repos with the same name, so problem solved there.

I think that coq-community and coq-contribs should get a shorted "name" for their ORG component (that is what goes after From), eg Community and Contribs, so that on can From Community Require Algebra and avoid a possible conflict with Contribs.Algebra.

[Zimmi48]

It would indeed make sense to encourage package authors / maintainers to put their package under a team namespace. As long as you don't force people to use their username as namespace (like in the VSCode example that you cited and that I dislike very much). Once this encouragement is written down, you can indeed introduce a CI check of the top-level logname (checking that the declared top-level logname is indeed the only one used in the installed package) and have reviewers check that the logname is not too generic / out of the package authors / maintainers' control.

[Zimmi48]

In particular, while some packages in coq-community might want to use the Community top-level logname, it should be possible for other packages to migrate to coq-community without having to change the top-level logname in use.

[herbelin]

It would indeed make sense to encourage package authors / maintainers to put their package under a team namespace.

What meaning do you give to "encourage"?

That any new version of an opam package is asked to use a two-level hierarchy, say, as in user-contrib/Community/ZornsLemma, or user-contrib/mathcomp/fingroup, or user-contrib/Dyade/GraphCycleDetection (ex-graphs)?

Or that we do it just for the next versions of community and contrib packages, and leave it as a mere recommendation for other packages?

Do we also change the opam package name so that it reflects an org.pkg structure?

[Zimmi48]

What meaning do you give to "encourage"?

"encourage" as opposed to "impose"

I would not want to enforce it to all coq-community packages in particular. And this is the kind of change that should be introduced smoothly over a long time, not suddenly on all new package versions, as this is going to be a breaking change (in some cases, it would even be hard to write a backward compatible fix for users of these packages).

Do we also change the opam package name so that it reflects an org.pkg structure?

In fact, I'm not sure we can do this for existing packages (or it should be limited to some very specific cases) as this would break the opam upgrade workflow.

In any case, this is the kind of change of high enough importance to deserve a well-discussed (with users) CEP.

[Zimmi48]

BTW, if new opam package names should adopt a org.pkg structure, it would be better to make this coq-{org}-{pkg} to be in-line with the preexisting example of math-comp packages.

[gares]

Packages are called coq-something or CoqPackages.something, this is one thing.
But I was more interested about the logpath being org.pkg. This we can standardise, since it is Coq specific. For opam in particular I'm not so sure, since (1) we have a logpath attribute, orthogonal to the package name, and (2) packages may not correspond to a logpath, or can populate many, just imagine a package pulling in all metacoq or all mathcomp packages

[gares]

But yes, if the package happens to contain exactly one org.pkg, then what you suggest makes sense to me.

[ejgallego]

I'm not sure I like the org thing so much, at least in some senses. IMHO logical names should work better, a property that we want to have is stability by forking / relocation, etc...

[Zimmi48]

I'm not a fan either, and I agree with your concern about relocation. That's why I was saying it can be encouraged but should not be forced. In particular that can make sense in cases similar to Math-Comp where there's some consistency within the namespace. It is probably less so with an organization like coq-community.

[gares]

Hum, then we are back at avoiding conflicts, that is were we started.

[palmskog]

Can we at least agree that we need a separate namespace for the contribs quite urgently? Simply changing them all to (say) use the scheme Contrib.Name would free up a ton of high-quality top-level names. If a contrib project is moved elsewhere, it can assume a "proper" selected namespace.

[gares]

Fine to me.

What I wanted to point out in an early message is that all contribs used to be in a "site" directory, eg Saclay/SSReflect, Bordeaux/Groups. I've just recovered that list, it's here: https://pastebin.com/4v1Q5Jbu
This is another way to get a first level name that is possibly more informative than Contrib.

[ejgallego]

Can we at least agree that we need a separate namespace for the contribs quite urgently? Simply changing them all to (say) use the scheme Contrib.Name would free up a ton of high-quality top-level names.

Umm, I'm not sure I do agree we want to do a hotfix here; that is going to be double pain IMO as users will require to migrate twice.

First thing I'd do here is look at what other systems with large libraries are doing in order to organize the packages, and which component takes care which part; namespaces can be managed by the build system, the compiler itself, etc...

[Zimmi48]

Regarding contribs specifically, it would be good to come up with a list of contribs that are using very generic names, and whether these contribs are worth preserving with the same or a changed name, or should be archived in favor of a newer replacement.

[herbelin]

First thing I'd do here is look at what other systems with large libraries are doing in order to organize the packages, and which component takes care which part; namespaces can be managed by the build system, the compiler itself, etc...

Regarding proof assistants, Isabelle's AFP seems to have a flat namespace (https://www.isa-afp.org/topics.html) and Mizar's FM seems to have a 8.3 flat namespace (http://fm.mizar.org/fm.bib).

Independently of the question of what component manages the name space, the question remains, I believe, of whether we keep a flat name space or adopt a structured one (at least at some of the levels of abstraction).