[install_rules] Allow for stanzas to install files in different packages

[ejgallego]

In some cases, it is convenient for stanzas to produce objects that
will be installed under different packages.

For example, in Coq we may want to install the costly native files in
a foo-native package, or distributions such as Debian like to split
packages in -doc, -dev, and -dbg variants.

This PR modifies the code so this is possible.

This code is cherry-picked from #4750 (which would be the first user
of the feature), but I am submitting separately as I think the change
deserves more discussion.

For example, this implies that Dune_file.stanza_package stanza is not
canonical anymore. Likely, a better modelling would be to introduce
the notion of "sub-package" or "variant".

The code changes themselves don't make me super-happy, consider them a
draft. If you folks are OK with the idea, I can improve it so the
common case of one stanza installing files only for one package is
better optimized.

Signed-off-by: Emilio Jesus Gallego Arias e+git@x80.org

[bobot]

For example, this implies that Dune_file.stanza_package stanza is not canonical anymore.

How does that would compose with -p? Half of the stanza is disabled?

Distributions such as Debian like to split packages in -doc, -dev, and -dbg variants.

I don't understand the debian argument, as I understand: Debian uses one source package, compile it once, install it using $DESTDIR in a directory, split the files into different package. I don't see how we can help them.

For opam I don't understand what happen at the end. If something depends on coq and coq-native, coq is compiled twice?

[ejgallego]

How does that would compose with -p? Half of the stanza is disabled?

That's simpler, this does just remap files to a different .install file; rules are the same.

I don't understand the debian argument, as I understand: Debian uses one source package, compile it once, install it using $DESTDIR in a directory, split the files into different package. I don't see how we can help them.

That would help Debian as to avoid having to manually split the files into the different packages, which is fragile w.r.t. updates. As of today, you need to do a hack on the .install file; IMHO it would be much better to have dune generate .install files that can be mapped to debian install files 1:1

Anyways it was only an example of how this can be useful. Another example is for example putting the bytecode files in a different .install file, the build setup is the same, you just have two .install files.

For opam I don't understand what happen at the end. If something depends on coq and coq-native, coq is compiled twice?

That would be for example be coq-why3 and coq-why3-native, then, coq-why3 will produce the .vo files, coq-why3-native calls coqnative foo.vo and produces the .cmxs files.

So users only pay the native compilation cost when they install the *-native packages.

So indeed, this use case is mostly geared to cases when a stanza produces artifacts that are independent.

We could of course introduce a new stanza:

(coq.native
    (package coq-why3-native)
    (theory coq-why3))

but that seems a bit uglier, I dunno.

[bobot]

That's simpler, this does just remap files to a different .install file; rules are the same.

So the stanza would be activated for the -p of both package? It should work for binaries but I don't know how we can generalize that. Compiling/Installing part of the dune-project is already complicated so I'm quite nervous of such changes. The main difficulty is to know when to use the local version and when to use the installed version that was already installed. The stanza <-> package relationship helps to deactivate the stanzas and so the installed version of the deactivated library stanza are used.

In your case with a

(coq
    (package coq-why3-native for native)
    (package coq-why3 for byte)
    (theory coq-why3))

The behavior of the stanza is not only activated/deactivated but partially deactivated since the .vo shouldn't be produced but lookup in the installation directories. So it means that coq-why3 should be at the same time installed (byte part) and not installed (native part). So resolution of the location of the library is not uniq which add complications. Do you see my worries?

[rgrinberg]

If you want to make it work this way for coq stanzas, I see no problem with it. Unless there's a concrete reason we need it for other stanzas, I would refrain.

Feel free to re-open once you have a PR that uses this feature for coq and I'll be happy to review.

[ejgallego]

Yes let's close this for now.

This was indeed used in #4750 to place some objects of the theory stanza in a different package. Code in that PR was working well, however I didn't have the cycles to address François comments yet, and I won't likely have time for more native work in the near future.

But I leave this comment to anyone else interested in making the two packages setup happen.

[ejgallego]

So the stanza would be activated for the -p of both package?

It seems to me that the stanza would indeed belong to more than one package, I don't see a lot of harm in adding all the rules even if only a subset of packages is specified, we could optimize that by having the stanza rule function take a package set argument.

But this is really about install setup.

It should work for binaries but I don't know how we can generalize that. Compiling/Installing part of the dune-project is already complicated so I'm quite nervous of such changes. The main difficulty is to know when to use the local version and when to use the installed version that was already installed. The stanza <-> package relationship helps to deactivate the stanzas and so the installed version of the deactivated library stanza are used.

What is the part of the code that determines this "use local vs use installed" thing? I'm unsure I know what particular part of Dune you are talking about.

In your case with a

(coq
(package coq-why3-native for native)
(package coq-why3 for byte)
(theory coq-why3))
The behavior of the stanza is not only activated/deactivated but partially deactivated since the .vo shouldn't be produced but lookup in the installation directories. So it means that coq-why3 should be at the same time installed (byte part) and not installed (native part). So resolution of the location of the library is not uniq which add complications. Do you see my worries?

I'm unsure about what's your concrete worry here, I can agree that this is a very delicate area.

In the above example, is your worry is that if I pass -p coq-why3-native then the compilation should fail because the object files for the coq-why3-native package should not be made available ?

[bobot]

What is the part of the code that determines this "use local vs use installed" thing? I'm unsure I know what particular part of Dune you are talking about.

Each kind of notion (binary, library, package) has its own database that precise where they can be found something like name -> path.

I'm unsure about what's your concrete worry here, I can agree that this is a very delicate area.

It seems that we now have something like name -> path list, since one library can be local or installed. I believe that this change modify the granularity of the database, for example from library to library x compilation_mode.