Revamp Agda builder, add documentation

[langston-barrett]

The build process for Agda packages now mirrors that of Idris packages. There is an agda.withPackages attribute that works like ghcWithPackages.

This should make it easier to implement building Agda binaries, since that process can reuse agdaWithPackages.

Motivation for this change

Fixes #19434

Things done

• Tested using sandboxing (nix.useSandbox on NixOS, or option build-use-sandbox in nix.conf on non-NixOS)
• Built on platform(s)
  • NixOS
  • macOS
  • other Linux distributions
• Tested via one or more NixOS test(s) if existing and applicable for the change (look inside nixos/tests)
• Tested compilation of all pkgs that depend on this change using nix-shell -p nox --run "nox-review wip"
• Tested execution of all binary files (usually in ./result/bin/)
• Fits CONTRIBUTING.md.

---

[langston-barrett]

cc: @Fuuzetsu @copumpkin

[Fuuzetsu]

Seems it removes the interactive part which is needed for nix-based Agda with emacs for example

[langston-barrett]

@Fuuzetsu Can you point that part out to me? Is it the passthru bit? Thanks for taking a look.

[Fuuzetsu]

Yes precisely the passthru, being able to load stuff into emacs was actually the main motivation for original version of builder (not the one you're changing)

[langston-barrett]

@Fuuzetsu Can you describe the use-case in a little more detail? It seems to me like the user could use agda.withPackages, since emacs will find the wrapped agda binary.

[Fuuzetsu]

emacs needs to know where to find sources and compiled sources, it's not enough that agda binary sees it

[mpickering]

Does this break or improve the way we can package cedille? I didn't know there were any other agda binaries packaged in nixpkgs.

[alexarice]

Is there any reason the documentation and withPackages part of this can't be added without changing the agda mkderivation part? Otherwise I feel I'm missing something as I can't see how you can currently load any agda packages in emacs.

[turion]

@langston-barrett I believe this is now superseded by #76653. Shall we close?

[langston-barrett]

@turion Yes, agreed! 🎉