Rocq Package Metadata: Piggybacking on Findlib.

[rlepigre]

Rendered version

This could use feedback from dune devs (CC @ejgallego @Alizter @rgrinberg), to make sure this would be good enough.

Related discussions:

• https://coq.zulipchat.com/#narrow/channel/240550-Dune-devs-.26-users/topic/.5Blaodpath.5D.20Coqdep.20vs.2E.20Coqmod/near/285853410
• https://coq.zulipchat.com/#narrow/channel/240550-Dune-devs-.26-users/topic/Warning.20about.20not.20found.20libraries.20which.20are.20there

[proux01]

Alternatively, if the build systems are ported, maybe there will be no porting needed on project side.

[rlepigre]

Actually, I think that porting will be required regardless: the build systems will need to be provided with different information (basically a list of package names the project depends on). For dune, this information is already required in some form, but that might need to change. In particular, theories that are dependencies currently need to be listed as directory paths, and these would need to become package names. (Furthermore, the (plugins ...) and (theories ...) fields of the coq.theory stanza could be merged in a single (deps ...) field.)

In any case, care needs to be taken to ensure that a smooth transition is possible.

[jfehrle]

The best transition is one that allows using either the old or the new build method for a transition period. That may be difficult to achieve. Requiring immediate but very simple changes to every interesting Rocq package in opam could be a rocky transition.

[jfehrle]

Having rocq_makefile install packages may be nice as an option. However, developers modifying a package should probably still be able to build it without installing anything (instead reporting errors for missing packages).

If you're modifying a package, the code you're modifying should not be in opam or Rocq directories (good development practice). So there should be a way to build in a user specified directory (downloading source with git). Developers may want to modify a package that's a dependency of their main package, testing by running their main package. How would that work? There's also the more obscure (hypothetical?) case where you're modifying multiple packages at once--all of which should be outside of opam/Rocq directories.

One difficulty with modifying rocq_makefile is that IINM GUIs know and parse the file. (A better design would be for only Rocq to parse the file and provide an API the GUIs can call to get the details in a processed format.)

[rlepigre]

Currently, the typical workflow for maintaining packages is to create an opam switch with all dependencies installed in the appropriate version, and then building the project from its sources. For example, I know that this is how most Iris devs do things, and they even use some infrastructure for pinning the right versions of their dependencies in opam.

Alternatives exist, like using dune and it's composed builds, which lets you compile a project and its dependencies in the same workspace, without having to install said dependencies. What you are talking about above seems to be similar to that if I understand correction. In any case, a mechanism like that is very useful, but rather orthogonal to the particular installation scheme / package metadata.

I have never heard of anything like GUIs parsing rocq_makefile files. Do you have pointers to that?

[jfehrle]

orthogonal to the particular installation scheme / package metadata.

My first paragraph above responds directly to your comments about installing libraries. Also what I said about using a non-opam, non-Rocq directory for packages that you're modifying. That is directly related to the installation scheme, isn't it?

Currently, the typical workflow for maintaining packages is to create an opam switch

Perhaps, but I expect that requires considerable familiarity with opam. The procedure should be documented rather than forcing everyone to figure it out on their own. Last I checked, about 2 years ago, the opam doc was still quite incomplete. Pretty much the same with the dune documentation and its dependencies. Does this procedure let you put the code you want to modify in a non-opam directory?

I wrote this section about 2 years ago. Some of the procedures are quite awkward due to missing features.

I have never heard of anything like GUIs parsing rocq_makefile files. Do you have pointers to that?

The dependency is on _CoqProject, my mistake.

[rlepigre]

orthogonal to the particular installation scheme / package metadata.

My first paragraph above responds directly to your comments about installing libraries. Also what I said about using a non-opam, non-Rocq directory for packages that you're modifying. That is directly related to the installation scheme, isn't it?

I'm sorry, I realize now that I did not quite understand what you meant in your first paragraph, and in fact I still don't. Clearly, I'm failing to communicate what I have in mind. What kind of situation do you have in mind exactly when writing "developers modifying a package"?

In case that helps, let me try to clarify what I meant to communicate in the CEP paragraph we are discussing: I have not yet worked out how rocq_makefile can be made to work with the discussed installation scheme. That roughly means figuring out two things:

1. How does a developer communicate to rocq_makefile the theory dependencies of the project in practice? Currently there is no need to do so because everything that is installed is always available, but that will eventually need to change when we stop putting theories in user-contrib. Instead, we will need to be explicit about what packages we depend on, and -Q bindings will need to be somehow added for all transitive deps.
2. How do we make it so that rocq_makefile produces a Makefile that, when invoked with make install, has the effect of installing the theories as expected for the new installation scheme?

[jfehrle]

What kind of situation do you have in mind exactly when writing "developers modifying a package"?

Primarily the author or a maintainer of the package who needs to modify the code in the package while doing maintenance, perhaps preparing PRs, but potentially could also be a developer who wants to tweak the package locally, e.g. to work around a limitation. Is that specific enough?

[jfehrle]

When dune is enhanced, perhaps we can also make progress on these related issues:

• From within Rocq, there's currently no way to learn what packages are installed. The installation process should save the opam package name, version number, description and the associated Rocq load path names (-R -Q etc, determining the module name) so that Rocq can show this information.

• Rocq should be able to show package dependencies for installed packages. Non-developer users won't want to wade through a bunch of configuration files to get this info. If they can get readily get it from the OS command line in an understandable format, that would be reasonable provided we document how to do this.

• There is no mechanism to ensure that two packages don't use the same load path, in which case you can't use both simultaneously without modifying one of the packages. This could be addressed with a registry of package load paths for Rocq opam packages and checking that new packages have unique load paths. This would be an opam change rather than dune.

[rlepigre]

I believe that most of these things could be done by querying opam and using ocamlfind (or the underlying findlib OCaml library). In any case, a tool could be developed to easily query that information if people find that is useful.

About your the last point: I believe there should be no such mechanism. It is perfectly fine if two independent packages use the same load path, even if two files end up a the same module path. This is even sometimes desirable, for example for configuration packages not meant to be used at the same time. If two packages define the same module, then the order of dependencies should be good enough for disambiguation.

[jfehrle]

The doc section I mention above lists some useful opam commands. I'm not aware of how you get the full list of dependencies for a package. Also, there's no clean way to get the Coq load path (logical name) for an opam package. Non-developer users do need to know that will want to know the dependencies.

For load paths, there could be a way to skip the check for the case you mention.

If two packages define the same module, then the order of dependencies should be good enough for disambiguation.

Where does this order of dependencies come from? You shouldn't have to specify -R on the command line for installed packages. Also it would be strange IINM to have a subdirectory that's in the overridden package that doesn't exist in the overriding package show up in the midst of the overriding package in Print LoadPath. Don't you think that breaks the appearance of modularity? Seems like this would be confusing for users.

[proux01]

FWIW, you may want to have a look at how things are done in Nix as it is an intermediate solution between the single user-contrib dir and ocamlfind use. I have the feeling that Nix (partly) adresses some of the issues you mention (of course only at package manager level, so not with the same granularity as what would be possible with a build manager like dune).