haskellPackages.Agda: Split outputs to reduce closure size

After enabling a separate binary output for the `Agda` Haskell package,
the new `bin` output measures ~100MiB, compared to the ~4.5GiB before.
Using it in `agdaWithPackages` reduces the closure size of an Agda
installation from ~5GiB to ~3GiB.  The remaining space is taken up
mostly by the GHC backend.

With this change, derivations depending on `haskellPackages.Agda`
directly need to pick the right (binary) output.  This concerns in
particular `emacsPackages.agda2-mode`.
This commit is contained in:
Philipp Joram 2024-04-05 16:56:52 +03:00
parent 8a35fec862
commit 294245f750
3 changed files with 13 additions and 8 deletions

View File

@ -1,21 +1,23 @@
{ trivialBuild { trivialBuild
, haskellPackages , haskellPackages
}: }:
let
trivialBuild rec { Agda = haskellPackages.Agda.bin;
in
trivialBuild {
pname = "agda-mode"; pname = "agda-mode";
version = haskellPackages.Agda.version; version = Agda.version;
dontUnpack = true; dontUnpack = true;
# already byte-compiled by Agda builder # already byte-compiled by Agda builder
buildPhase = '' buildPhase = ''
agda=`${haskellPackages.Agda}/bin/agda-mode locate` agda=`${Agda}/bin/agda-mode locate`
cp `dirname $agda`/*.el* . cp `dirname $agda`/*.el* .
''; '';
meta = { meta = {
inherit (haskellPackages.Agda.meta) homepage license; inherit (Agda.meta) homepage license;
description = "Agda2-mode for Emacs extracted from Agda package"; description = "Agda2-mode for Emacs extracted from Agda package";
longDescription = '' longDescription = ''
Wrapper packages that liberates init.el from `agda-mode locate` magic. Wrapper packages that liberates init.el from `agda-mode locate` magic.

View File

@ -40,13 +40,14 @@ let
allPackages = withPackages (filter self.lib.isUnbrokenAgdaPackage (attrValues self)); allPackages = withPackages (filter self.lib.isUnbrokenAgdaPackage (attrValues self));
}; };
}; };
inherit (Agda) meta; # Agda is a split package with multiple outputs; do not inherit them here.
meta = removeAttrs Agda.meta [ "outputsToInstall" ];
} '' } ''
mkdir -p $out/bin mkdir -p $out/bin
makeWrapper ${Agda}/bin/agda $out/bin/agda \ makeWrapper ${Agda.bin}/bin/agda $out/bin/agda \
--add-flags "--with-compiler=${ghc}/bin/ghc" \ --add-flags "--with-compiler=${ghc}/bin/ghc" \
--add-flags "--library-file=${library-file}" --add-flags "--library-file=${library-file}"
ln -s ${Agda}/bin/agda-mode $out/bin/agda-mode ln -s ${Agda.bin}/bin/agda-mode $out/bin/agda-mode
''; '';
withPackages = arg: if isAttrs arg then withPackages' arg else withPackages' { pkgs = arg; }; withPackages = arg: if isAttrs arg then withPackages' arg else withPackages' { pkgs = arg; };

View File

@ -1073,6 +1073,8 @@ self: super: builtins.intersectAttrs super {
# very useful. # very useful.
# Flag added in Agda 2.6.4.1, was always enabled before # Flag added in Agda 2.6.4.1, was always enabled before
(enableCabalFlag "debug") (enableCabalFlag "debug")
# Split outputs to reduce closure size
enableSeparateBinOutput
]; ];
# ats-format uses cli-setup in Setup.hs which is quite happy to write # ats-format uses cli-setup in Setup.hs which is quite happy to write