65e774e2a4
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`.
38 lines
1.2 KiB
Nix
38 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
|