haskellPackages.Agda: Split outputs to reduce closure size

[phijor]

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 is an attempt to resolve #285261.

Description of changes

Things done

• Built on platform(s)
  • x86_64-linux
  • aarch64-linux
  • x86_64-darwin
  • aarch64-darwin
• For non-Linux: Is sandboxing enabled in nix.conf? (See Nix manual)
  • sandbox = relaxed
  • sandbox = true
• Tested, as applicable:
  • NixOS test(s) (look inside nixos/tests)
  • and/or package tests
  • or, for functions and "core" functionality, tests in lib/tests or pkgs/test
  • made sure NixOS tests are linked to the relevant packages
• Tested compilation of all packages that depend on this change using nix-shell -p nixpkgs-review --run "nixpkgs-review rev HEAD". Note: all changes have to be committed, also see nixpkgs-review usage
• Tested basic functionality of all binary files (usually in ./result/bin/)
• 24.05 Release Notes (or backporting 23.05 and 23.11 Release notes)
  • (Package updates) Added a release notes entry if the change is major or breaking
  • (Module updates) Added a release notes entry if the change is significant
  • (Module addition) Added a release notes entry if adding a new NixOS module
• Fits CONTRIBUTING.md.

---

Add a 👍 reaction to pull requests you find important.

[turion]

@ofborg build agda.passthru.tests.allPackages

[iblech]

I believe I very much like this, thank you for your work :-), but can probably only test on Saturday.

[turion]

CC @alexarice @neosimsim

[phijor]

All tests seem to pass; I'll mark this PR as ready for review. This is my first time working on code that a lot of packages depend on, so any feedback and comments are appreciated.

I have used this successfully locally for Agda development with Neovim + cornelis. Can anyone who uses emacsPackages.agda-mode and/or vimPackages.vim-agda confirm that I didn't break editor integration?

I believe I very much like this, thank you for your work :-), but can probably only test on Saturday.

Thank you, I'd appreciate that a lot!

[phijor]

The interaction of multiple-output packages and outputsToInstall was very surprising to me (Why does changing a meta attribute cause an evaluation error?? I believe I ran into #255947). Is removing outputsToInstall for the derived package the right thing to do here?

[ncfavier]

LGTM, haven't tested.

[iblech]

I have now tested this with my workflow -- everything works as it should. (I'm using the agda-mode for Emacs, however I'm not using emacsPackages.agda-mode.) Thank you for your work! Unfortunately I cannot comment on your question regading outputsToInstall.

I propose to handle the issue of unconditional dependency on GHC at some later point and don't hold off this pull request just for that reaon.