Add containers-lib to nix flake packages

[HeinrichApfelmus]

This pull request adds an attribute containers-lib to the packages output in flake.nix. In this way, users can provision the containers-lib using Nix.

This is an addendum to #406 to make containers.agda-lib useable with Nix.

Note: This pull request also changes the version of the base-lib attribute to match the version 4.18 of the base package on Hackage.

[HeinrichApfelmus]

@jespercockx Thanks! Could you merge the pull request? — I don't have any permissions on this repository. 😅

[HeinrichApfelmus]

Actually, I think that there is something wrong when Nix typechecks the containers.agda-lib library: It tries to write local interface files for base.agda-lib into the nix store.

Somehow, transitive dependencies do not compose just yet (containers depends on base), not sure what to do here.

[liesnikov]

do you mean these lines? https://github.com/agda/agda2hs/actions/runs/14793443918/job/41535343556#step:5:204 (and till 304 or so)
Because it seems like that was just a dependency build, so a separate derivation, as it should be. And then when containers it typechecked I don't see any re-checking of base.

[HeinrichApfelmus]

do you mean these lines? https://github.com/agda/agda2hs/actions/runs/14793443918/job/41535343556#step:5:204 (and till 304 or so)

Yes and no.

And then when containers it typechecked I don't see any re-checking of base.

Yes. However, the problem is that agdaPackages.mkDerivation produces a result that is incompatible with agda2hs when used. I.e. agdaPackages produces self-consistent results in the nix store, but those results are not useable when trying to compile with adga2hs.

We need an equivalent agda2hs.mkDerivation. I have some code here:

https://github.com/HeinrichApfelmus/bags/blob/main/nix/lib.nix

but haven't managed to backport it yet.

[liesnikov]

Hmm, I'm not sure I understand exactly. What do you consider to be a "built derivation" for agda2hs?

If it's agda+agdai files and agda2hs then doesn't behave the same way agda proper does, I think I see the problem. I'd be surprised if agda2hs behaved very differently here, but it can be.
Or is it agda, agdai, and hs files, i.e. a self-contained compiled unit for all usages of agda2hs?

[HeinrichApfelmus]

If it's agda+agdai files and agda2hs then doesn't behave the same way agda proper does, I think I see the problem. I'd be surprised if agda2hs behaved very differently here, but it can be.

Yep, that's indeed the case and the problem.

• Agda puts .agdai files in a directory _build/2.7.0
• The nixified agda2hs uses --local-interfaces (here:

  agda2hs/nix/agda2hs.nix

  Line 26 in 256e604

  --add-flags "--local-interfaces"

  ) and expects the .agdai files to be colocated with the .agda files.

Consequently, when compiling a downstream file with agda2hs, the --local-interfaces options causes agda2hs to attempt to write an .agdai file to the nix store.

[liesnikov]

Ah, indeed.
That file should probably stay in sync with nixpkgs' source for agda, which by now dropped --local-interfaces, afaik
I just couldn't find a way to (ab)use the upstream in a way that would work reliably, so I copied the file. It doesn't mean that there is no way to derive it programmatically though

[HeinrichApfelmus]

@liesnikov I have added a custom definition of mkDerivation and used it for the base-lib and containers-lib derivations.

This works, in downstream code, I can now do

        agda2hs-custom = agda2hs.lib.${system}.withPackages ([
          agda2hs.packages.${system}.base-lib
          agda2hs.packages.${system}.containers-lib
        ]);

and get a variant of agda2hs that knows about these two libraries.

[jespercockx]

@liesnikov @HeinrichApfelmus what's the current status of this PR? What's needed for it to get into a mergeable state?

[HeinrichApfelmus]

@liesnikov @HeinrichApfelmus what's the current status of this PR? What's needed for it to get into a mergeable state?

The changes are complete as far as I am concerned. The CI had failed for spurious reasons, I'll try to restart it.

[HeinrichApfelmus]

CI passes. @jespercockx do you want me to merge?