Could the Agda library be published to Nix Packages under agdaPackages?

[cyberglot]

I use Nix and I'm playing around with agda2hs, but it's been hard to do all the wiring necessary for this to work. I do not know how much work would that entail, but I am happy to help with that.

[jespercockx]

I'm not a Nix user myself but I'd be happy with any PRs to improve Nix support for agda2hs.

[liesnikov]

This would be great! There's a few things we can improve with the current nix setup, perhaps it would make sense to do a sprint and file within one PR? My wishlist would be:

1. As you say, having agda2hs-lib available in agdaPackages. I think this one would be the least amount of work - just about adding a derivation here and here.
2. We have a custom agda2hs derivation that is almost a copy of the upstream agda derivation. Would love to drop that.
3. We ship agda2hs-executable without agda2hs-lib linked since then one can add other libraries on top (--library-file flags that the derivation uses don't stack, afaik). It would be much nicer to have both agda2hs with the library and have the ability to add new libraries. Perhaps something like this can be done by always adding agda2hs-lib to withPackages list?
4. It would be good to have a builder that takes agda2hs library and produces an haskell derivation.
5. Devise some sensible naming scheme for all the derivations we expose in lib and packages now.

The first one is least intrusive against nixpkgs, the others will probably require some patches, e.g. so that we can re-use upstream agda derivation.

[liesnikov]

I added the lib in my fork, but haven't filed a PR against nixpkgs because I'm a bit confused about maintainers etiquette in nixpkgs.

[thelissimus]

@liesnikov Quick note: before making a PR be sure to move the contents of preBuild to buildPhase. Explanation: NixOS/nixpkgs#365340 (comment)

[liesnikov]

@thelissimus I think it's a slightly different setup, what I do is a carbon copy of how other libraries are set up, which do use preBuild.

That is, unless I misunderstood your link and the maintainers want to do that everywhere.

[thelissimus]

@liesnikov To my understanding, cubical-mini does the exact same thing, but with a Haskell script Everything.hs. As I understand it, Everything.agda should be generated during buildPhase according to this document too: agda.section.md.

Anyways, if you're uncertain you can just clarify things during the PR review. If they require changes you can just amend the commit and force push until the maintainers are satisfied, no big deal.

[cyberglot]

(apologies for radio silence! 2025 started strong 😭)

From @liesnikov's option, I am happy to have at least the first one. Personally, it's a terrible user experience to use /.agda/libraries when Nix could take care of it.