Re: Installing headers to a separate output?

[ludo@gnu.org (Ludovic Courtès)]

Efraim Flashner <efraim@flashner.co.il> skribis:

> On Thu, 25 Feb 2016 21:32:22 +0100
> Ricardo Wurmus <rekado@elephly.net> wrote:
>
>> Hi Guix,
>> 
>> should we install headers to separate outputs as we do it in some cases
>> for really large documentation?  It seems wrong to me to download
>> substitutes for libraries when at build time only certain headers are
>> needed.
>> 
>> Other distributions have separate “*-devel” or “*-dev” packages (and I’m
>> ambivalent about this) — would it be a bad idea if we provided “devel”
>> or “dev” *outputs* so that users had more control over what ends up in
>> their store?
>> 
>> I’m not writing this because I’m annoyed by the current behaviour — I’m
>> just curious.
>> 
>> ~~ Ricardo
>
> I thought a bit about it before and I don't really think it'll save that much
> space. Most of the time the headers are a small part of the total package,
> and the fine-tuning that comes with chosing exactly which outputs from a
> build process you actually want seem like they should be left as
> encouragement for people to hack their systems.

Seconded.  We can add a separate “include” output (there’s already a
special case for that in gnu-build-system) on a case-by-case basis, like
we do for documentation, but in practice, I’ve never seen a case where
moving headers away would be a significant space saving.

IOW, it’d be a micro-optimization; there are other things we could do
before that to save space.

Ludo’.