1# Builder for Agda packages.
2
3{ stdenv, lib, self, Agda, runCommand, makeWrapper, writeText, ghcWithPackages, nixosTests }:
4
5with lib.strings;
6
7let
8 withPackages' = {
9 pkgs,
10 ghc ? ghcWithPackages (p: with p; [ ieee754 ])
11 }: let
12 pkgs' = if builtins.isList pkgs then pkgs else pkgs self;
13 library-file = writeText "libraries" ''
14 ${(concatMapStringsSep "\n" (p: "${p}/${p.libraryFile}") pkgs')}
15 '';
16 pname = "agdaWithPackages";
17 version = Agda.version;
18 in runCommand "${pname}-${version}" {
19 inherit pname version;
20 nativeBuildInputs = [ makeWrapper ];
21 passthru = {
22 unwrapped = Agda;
23 inherit withPackages;
24 tests = {
25 inherit (nixosTests) agda;
26 allPackages = withPackages (lib.filter self.lib.isUnbrokenAgdaPackage (lib.attrValues self));
27 };
28 };
29 inherit (Agda) meta;
30 } ''
31 mkdir -p $out/bin
32 makeWrapper ${Agda}/bin/agda $out/bin/agda \
33 --add-flags "--with-compiler=${ghc}/bin/ghc" \
34 --add-flags "--library-file=${library-file}" \
35 --add-flags "--local-interfaces"
36 ln -s ${Agda}/bin/agda-mode $out/bin/agda-mode
37 ''; # Local interfaces has been added for now: See https://github.com/agda/agda/issues/4526
38
39 withPackages = arg: if builtins.isAttrs arg then withPackages' arg else withPackages' { pkgs = arg; };
40
41 extensions = [
42 "agda"
43 "agda-lib"
44 "agdai"
45 "lagda"
46 "lagda.md"
47 "lagda.org"
48 "lagda.rst"
49 "lagda.tex"
50 ];
51
52 defaults =
53 { pname
54 , meta
55 , buildInputs ? []
56 , everythingFile ? "./Everything.agda"
57 , includePaths ? []
58 , libraryName ? pname
59 , libraryFile ? "${libraryName}.agda-lib"
60 , buildPhase ? null
61 , installPhase ? null
62 , extraExtensions ? []
63 , ...
64 }: let
65 agdaWithArgs = withPackages (builtins.filter (p: p ? isAgdaDerivation) buildInputs);
66 includePathArgs = concatMapStrings (path: "-i" + path + " ") (includePaths ++ [(dirOf everythingFile)]);
67 in
68 {
69 inherit libraryName libraryFile;
70
71 isAgdaDerivation = true;
72
73 buildInputs = buildInputs ++ [ agdaWithArgs ];
74
75 buildPhase = if buildPhase != null then buildPhase else ''
76 runHook preBuild
77 agda ${includePathArgs} ${everythingFile}
78 runHook postBuild
79 '';
80
81 installPhase = if installPhase != null then installPhase else ''
82 runHook preInstall
83 mkdir -p $out
84 find -not \( -path ${everythingFile} -or -path ${lib.interfaceFile everythingFile} \) -and \( ${concatMapStringsSep " -or " (p: "-name '*.${p}'") (extensions ++ extraExtensions)} \) -exec cp -p --parents -t "$out" {} +
85 runHook postInstall
86 '';
87
88 # As documented at https://github.com/NixOS/nixpkgs/issues/172752,
89 # we need to set LC_ALL to an UTF-8-supporting locale. However, on
90 # darwin, it seems that there is no standard such locale; luckily,
91 # the referenced issue doesn't seem to surface on darwin. Hence let's
92 # set this only on non-darwin.
93 LC_ALL = lib.optionalString (!stdenv.isDarwin) "C.UTF-8";
94
95 meta = if meta.broken or false then meta // { hydraPlatforms = lib.platforms.none; } else meta;
96
97 # Retrieve all packages from the finished package set that have the current package as a dependency and build them
98 passthru.tests = with builtins;
99 lib.filterAttrs (name: pkg: self.lib.isUnbrokenAgdaPackage pkg && elem pname (map (pkg: pkg.pname) pkg.buildInputs)) self;
100 };
101in
102{
103 mkDerivation = args: stdenv.mkDerivation (args // defaults args);
104
105 inherit withPackages withPackages';
106}