Don't register include directories in dune registry of packages

dune_project is eager to register include directories of upstream modules into the registry of packages. The problem with this is that include directories must be guarded with proper build and install interfaces to work well. If an unguarded include directory is added to an installable target, cmake will rightfully complain that this will not work on the installed version. A first iteration of this MR pointed at out that the right solution here is to just register the target, and delegate the include directories to whoever creates the target (we will add a helper for this later in !1355 (merged)). However, in the discussions we realized that this is also not necessary due dune_project invoking include_directories on upstream packages anyways, making this line completely superfluous in single-builds and instead obstructing super-builds.

added buildsystem label

assigned to @simon.praetorius

mentioned in merge request pdelab/dune-pdelab!624 (merged)

changed the description

mentioned in merge request !1355 (merged)

I guess, this is not meant to be merged right away, or is it? I am trying to think what this change implies or requires. When the module dependencies are processed of the whole dependency tree, the include directories are not put into the global registry anymore, but instead the module library (libraries). This would requires that 1. every module has a module library, 2. the include dirs are registered in that module target. I this correct? If yes, we should list what needs to be done before we can merge this. If my conclusion is not correct, I need a little bit help to understand the proposed change.

added 1 commit

• 05e3cca5 - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version

resolved all threads

changed title from Register module libraries instead of include directories to Do note register include directories in dune packages

changed the description

assigned to @santiago.ospina and unassigned @simon.praetorius

requested review from @simon.praetorius

changed title from Do note register include directories in dune packages to Don't register include directories in dune packages

changed title from Don't register include directories in dune packages to Don't register include directories in dune registry of packages

changed the description

resolved all threads

added 1 commit

• 8247647f - Remove outdated comment

Compare with previous version

approved this merge request

Ok, everything seems to be fine. I will merge.

merged

mentioned in commit 9142c21b

It could be that this MR caused #394 (closed). Without testing locally, it seems to me that the precompiled python libraries were passing the directories in ${module}_INCLUDE_DIRS via the registered package modules with the extractCompiler.cc target. So maybe we were too quick to merge this without properly testing in the python side. So the good news is that we don't need to back port, but the bad news is that we may need to revert this change :(

mentioned in commit c074f7a2

mentioned in merge request !1463 (closed)

mentioned in issue #394 (closed)

mentioned in merge request !1526 (closed)

mentioned in commit 1d66aba3

mentioned in merge request !1528

mentioned in commit f6ae3cf4

mentioned in commit ad45bca9