[install] Tweaks to library handling in dune install

[ejgallego]

When creating the install rules of Coq packages, we'd like to separate lib_root from lib, as for example to support having custom library dirs:

$prefix/lib/ocaml/$ocaml_version/$lib_name
$prefix/lib/coq/$coq_version/$lib_name

Nix builds uses --libdir to map the lib directory to the right path in the first case however this also remaps libroot so that doesn't work so well for the intended Coq layout.

How should we handle this? Is that a desired thing to do? Should we add an extra parameter to dune install for setting the OCaml lib?

c.f. coq/coq#9689

[ghost]

I'm not sure dune install is the right place for such a setting to go. I would expect such a choice to be made by whoever controls the OCaml installation. i.e., you would configure where OCaml libraries go when calling the ./configure script of OCaml.

One other issue is that this doesn't fit well with existing opam .install files. Though we can always produce paths of the form ../ocaml/4.08/mylib in .install files.

[ejgallego]

I am not sure I fully follow what you mean @diml , I think the current setup works fine for OCaml libs, it is for other kind of data that should go in lib where things are a bit more constrained.

I guess my description was a bit confusing, indeed the install files for OCaml should not change, we assume the compiler was correctly configured for whatevev lib/blah/ocaml path we use; however the problem I refer to is that now Coq libraries will be forced to live under that path.

[rgrinberg]

@ejgallego I think I might also be misinterpreting. So if you could clarify from the beginning that would be useful. I'm not understand the issue with nix for example (probably because I don't use nix)

The way I understand it is that you don't necessarily want coq libraries to be installed along with OCaml libraries. That seems to make sense, but it also seems to be conflicting with .install files work.

@diml why isn't $ dune install the right place for such settings? We already have similar settings like --libdir, --prefix.

[ghost]

@diml why isn't $ dune install the right place for such settings? We already have similar settings like --libdir, --prefix.

Well, we should indeed allow to override these settings for special purposes or package managers. However, it doesn't feel right that the users would be required to pass these parameters everytime they manually install a package. If the decision as to where packages should go has already been made when installing the master package, that's the location that should be used by default.

[ejgallego]

The way I understand it is that you don't necessarily want coq libraries to be installed along with OCaml libraries.

Indeed, that's what I need; sorry if my description was confusing. OCaml libraries are installed properly, however Coq libraries are bound to the OCaml library path and IMHO it would make sense for them to live in a different "path space".

That seems to make sense, but it also seems to be conflicting with .install files work.

I guess you are right and lib / libroot are bound together almost by spec. Allowing to override lib and libroot separately could make sense on the other hand you could claim it is a bit of a hack.

If the decision as to where packages should go has already been made when installing the master package, that's the location that should be used by default.

The thing is that the install format seems too OPAM-specific to me; as of today installing dune-built Coq with OPAM works perfectly well as in this case OCaml's lib == general lib.

But in most distros general lib will be /usr/lib and OCaml's lib will be /usr/lib/ocaml/$version so that's where the format seems to lack a bit of flexibility.

p.s: Note that the .install format forbids using .. in install paths.

[ghost]

It seems to me that packages should be allowed to define "sites" where other packages are allowed to install files. For instance, Coq could define a "Coq library site". Then this site would become a valid installation section.

p.s: Note that the .install format forbids using .. in install paths.

Are you sure about that? We generate a lot of them when cross-compiling.

[ejgallego]

It seems to me that packages should be allowed to define "sites" where other packages are allowed to install files. For instance, Coq could define a "Coq library site". Then this site would become a valid installation section.

Yup, that would work fine. Note that if the package files are architecture independent then there is no problem as share works pretty well; it is only for true binaries that the problem exists.

Handling libroot separately would also work tho provided the install rules add the package-specific suffix.

Are you sure about that? We generate a lot of them when cross-compiling.

That's what's written in the manual https://opam.ocaml.org/doc/Manual.html#lt-pkgname-gt-install

[and IMHO makes sense]

[ghost]

Ah, well this is definitely not enforced then. I agree that it makes sense though

[rgrinberg]

How should we proceed then? Does it make sense for $ dune install to provide extra functionality on top of .install files to facilitate this? @ejgallego if coq is planning on using opam for package management, seems like you need to wait for proper upstream support.

[ejgallego]

How should we proceed then? Does it make sense for $ dune install to provide extra functionality on top of .install files to facilitate this?

It is indeed not clear to me how to proceed. Extending install files is not something very lightweight unfortunately.

@ejgallego if coq is planning on using opam for package management, seems like you need to wait for proper upstream support.

Actually Coq works well with OPAM already, as OPAM makes the assumption "OCaml lib == system lib", the problem is with other setups such as Nix or Debian.

[ejgallego]

Actually Coq works well with OPAM already, as OPAM makes the assumption "OCaml lib == system lib", the problem is with other setups such as Nix or Debian.

And indeed this makes the case for extending OPAM install format weaker :(

[rgrinberg]

Perhaps it makes sense to do what we did with META files. Have a dune specific format for installation that $ dune install will understand. For opam installation, we can simply convert from this dune format to .install files (possibly at the cost of precision).

[ghost]

That seems reasonable to me

[ejgallego]

Indeed that seems reasonable, I could have a stab at it once I get back to the Coq PR and it would be a good use case. Indeed if we have a qualified lib declaration, such as lib "coq", etc..., there is a mapping to regular install files by prefixing the qualified part to the install path, this is what's done in Coq for example.

[ejgallego]

Related to #3104

[rgrinberg]

@bobot do you have any input on this?