nixpkgs/pkgs/top-level/agda-packages.nix
Naïm Favier 65e774e2a4
agda: fix passthru
The current `//` override to `agda.passthru.tests` is non-recursive so
it destroys everything else under `passthru`, and furthermore does not
go through `mkDerivation` so that we end up with different values for
`agda.tests` and `agda.passthru.tests`.

Fix it by moving the `allPackages` test to the definition of
`withPackages`.
2023-02-12 14:44:16 +01:00

37 lines
1.2 KiB
Nix

{ pkgs, lib, newScope, Agda }:
let
mkAgdaPackages = Agda: lib.makeScope newScope (mkAgdaPackages' Agda);
mkAgdaPackages' = Agda: self: let
inherit (self) callPackage;
inherit (callPackage ../build-support/agda {
inherit Agda self;
inherit (pkgs.haskellPackages) ghcWithPackages;
}) withPackages mkDerivation;
in {
inherit mkDerivation;
lib = lib.extend (final: prev: import ../build-support/agda/lib.nix { lib = prev; });
agda = withPackages [];
standard-library = callPackage ../development/libraries/agda/standard-library {
inherit (pkgs.haskellPackages) ghcWithPackages;
};
iowa-stdlib = callPackage ../development/libraries/agda/iowa-stdlib { };
agda-prelude = callPackage ../development/libraries/agda/agda-prelude { };
agda-categories = callPackage ../development/libraries/agda/agda-categories { };
cubical = callPackage ../development/libraries/agda/cubical { };
functional-linear-algebra = callPackage
../development/libraries/agda/functional-linear-algebra { };
generic = callPackage ../development/libraries/agda/generic { };
agdarsec = callPackage ../development/libraries/agda/agdarsec { };
};
in mkAgdaPackages Agda