summary refs log tree commit diff
path: root/pkgs/top-level/agda-packages.nix
blob: 1e0e6e0a2d5863a204b0de03ed7980af8153b002 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
{ 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 { };

    _1lab = callPackage ../development/libraries/agda/1lab { };
  };
in mkAgdaPackages Agda