1 files changed, 122 insertions, 0 deletions
diff --git a/nixpkgs/pkgs/build-support/agda/default.nix b/nixpkgs/pkgs/build-support/agda/default.nix
new file mode 100644
index 000000000000..b5d72d9ccf19
--- /dev/null
+++ b/nixpkgs/pkgs/build-support/agda/default.nix
@@ -0,0 +1,122 @@
+# Builder for Agda packages.
+
+{ stdenv, lib, self, Agda, runCommand, makeWrapper, writeText, ghcWithPackages, nixosTests }:
+
+let
+  inherit (lib)
+    attrValues
+    elem
+    filter
+    filterAttrs
+    isAttrs
+    isList
+    platforms
+    ;
+
+  inherit (lib.strings)
+    concatMapStrings
+    concatMapStringsSep
+    optionalString
+    ;
+
+  withPackages' = {
+    pkgs,
+    ghc ? ghcWithPackages (p: with p; [ ieee754 ])
+  }: let
+    pkgs' = if isList pkgs then pkgs else pkgs self;
+    library-file = writeText "libraries" ''
+      ${(concatMapStringsSep "\n" (p: "${p}/${p.libraryFile}") pkgs')}
+    '';
+    pname = "agdaWithPackages";
+    version = Agda.version;
+  in runCommand "${pname}-${version}" {
+    inherit pname version;
+    nativeBuildInputs = [ makeWrapper ];
+    passthru = {
+      unwrapped = Agda;
+      inherit withPackages;
+      tests = {
+        inherit (nixosTests) agda;
+        allPackages = withPackages (filter self.lib.isUnbrokenAgdaPackage (attrValues self));
+      };
+    };
+    # Agda is a split package with multiple outputs; do not inherit them here.
+    meta = removeAttrs Agda.meta [ "outputsToInstall" ];
+  } ''
+    mkdir -p $out/bin
+    makeWrapper ${Agda.bin}/bin/agda $out/bin/agda \
+      --add-flags "--with-compiler=${ghc}/bin/ghc" \
+      --add-flags "--library-file=${library-file}"
+    ln -s ${Agda.bin}/bin/agda-mode $out/bin/agda-mode
+    '';
+
+  withPackages = arg: if isAttrs arg then withPackages' arg else withPackages' { pkgs = arg; };
+
+  extensions = [
+    "agda"
+    "agda-lib"
+    "agdai"
+    "lagda"
+    "lagda.md"
+    "lagda.org"
+    "lagda.rst"
+    "lagda.tex"
+    "lagda.typ"
+  ];
+
+  defaults =
+    { pname
+    , meta
+    , buildInputs ? []
+    , everythingFile ? "./Everything.agda"
+    , includePaths ? []
+    , libraryName ? pname
+    , libraryFile ? "${libraryName}.agda-lib"
+    , buildPhase ? null
+    , installPhase ? null
+    , extraExtensions ? []
+    , ...
+    }: let
+      agdaWithArgs = withPackages (filter (p: p ? isAgdaDerivation) buildInputs);
+      includePathArgs = concatMapStrings (path: "-i" + path + " ") (includePaths ++ [(dirOf everythingFile)]);
+    in
+      {
+        inherit libraryName libraryFile;
+
+        isAgdaDerivation = true;
+
+        buildInputs = buildInputs ++ [ agdaWithArgs ];
+
+        buildPhase = if buildPhase != null then buildPhase else ''
+          runHook preBuild
+          agda ${includePathArgs} ${everythingFile}
+          rm ${everythingFile} ${lib.interfaceFile Agda.version everythingFile}
+          runHook postBuild
+        '';
+
+        installPhase = if installPhase != null then installPhase else ''
+          runHook preInstall
+          mkdir -p $out
+          find \( ${concatMapStringsSep " -or " (p: "-name '*.${p}'") (extensions ++ extraExtensions)} \) -exec cp -p --parents -t "$out" {} +
+          runHook postInstall
+        '';
+
+        # As documented at https://github.com/NixOS/nixpkgs/issues/172752,
+        # we need to set LC_ALL to an UTF-8-supporting locale. However, on
+        # darwin, it seems that there is no standard such locale; luckily,
+        # the referenced issue doesn't seem to surface on darwin. Hence let's
+        # set this only on non-darwin.
+        LC_ALL = optionalString (!stdenv.isDarwin) "C.UTF-8";
+
+        meta = if meta.broken or false then meta // { hydraPlatforms = platforms.none; } else meta;
+
+        # Retrieve all packages from the finished package set that have the current package as a dependency and build them
+        passthru.tests =
+          filterAttrs (name: pkg: self.lib.isUnbrokenAgdaPackage pkg && elem pname (map (pkg: pkg.pname) pkg.buildInputs)) self;
+      };
+in
+{
+  mkDerivation = args: stdenv.mkDerivation (args // defaults args);
+
+  inherit withPackages withPackages';
+}