agda: rework builder

7 files changed, 110 insertions, 113 deletions

diff --git a/pkgs/build-support/agda/default.nix b/pkgs/build-support/agda/default.nix
index 0d054eaa546..205aff55573 100644
--- a/pkgs/build-support/agda/default.nix
+++ b/pkgs/build-support/agda/default.nix
@@ -1,90 +1,71 @@
-# Builder for Agda packages. Mostly inspired by the cabal builder.
+# Builder for Agda packages.
 
-{ stdenv, Agda, glibcLocales
-, writeShellScriptBin
-, extension ? (self: super: {})
-}:
+{ stdenv, lib, self, Agda, runCommandNoCC, makeWrapper, writeText, mkShell, ghcWithPackages }:
 
-with stdenv.lib.strings;
+with lib.strings;
 
 let
-  defaults = self : {
-    # There is no Hackage for Agda so we require src.
-    inherit (self) src name;
-
-    isAgdaPackage = true;
-
-    buildInputs = [ Agda ] ++ self.buildDepends;
-    buildDepends = [];
-
-    buildDependsAgda = stdenv.lib.filter
-      (dep: dep ? isAgdaPackage && dep.isAgdaPackage)
-      self.buildDepends;
-    buildDependsAgdaShareAgda = map (x: x + "/share/agda") self.buildDependsAgda;
-
-    # Not much choice here ;)
-    LANG = "en_US.UTF-8";
-    LOCALE_ARCHIVE = stdenv.lib.optionalString
-      stdenv.isLinux
-      "${glibcLocales}/lib/locale/locale-archive";
-
-    everythingFile = "Everything.agda";
-
-    propagatedBuildInputs = self.buildDependsAgda;
-    propagatedUserEnvPkgs = self.buildDependsAgda;
-
-    # Immediate source directories under which modules can be found.
-    sourceDirectories = [ ];
-
-    # This is used if we have a top-level element that only serves
-    # as the container for the source and we only care about its
-    # contents. The directories put here will have their
-    # *contents* copied over as opposed to sourceDirectories which
-    # would make a direct copy of the whole thing.
-    topSourceDirectories = [ "src" ];
-
-    # FIXME: `dirOf self.everythingFile` is what we really want, not hardcoded "./"
-    includeDirs = self.buildDependsAgdaShareAgda
-                  ++ self.sourceDirectories ++ self.topSourceDirectories
-                  ++ [ "." ];
-    buildFlags = stdenv.lib.concatMap (x: ["-i" x]) self.includeDirs;
-
-    agdaWithArgs = "${Agda}/bin/agda ${toString self.buildFlags}";
-
-    buildPhase = ''
-      runHook preBuild
-      ${self.agdaWithArgs} ${self.everythingFile}
-      runHook postBuild
+  withPackages' = {
+    pkgs,
+    ghc ? ghcWithPackages (p: with p; [ ieee ])
+  }: let
+    pkgs' = if builtins.isList pkgs then pkgs else pkgs self;
+    library-file = writeText "libraries" ''
+      ${(concatMapStringsSep "\n" (p: "${p}/${p.libraryFile}") pkgs')}
     '';
-
-    installPhase = let
-      srcFiles = self.sourceDirectories
-                 ++ map (x: x + "/*") self.topSourceDirectories;
-    in ''
-      runHook preInstall
-      mkdir -p $out/share/agda
-      cp -pR ${concatStringsSep " " srcFiles} $out/share/agda
-      runHook postInstall
-    '';
-
-    passthru = {
-      env = stdenv.mkDerivation {
-        name = "interactive-${self.name}";
-        inherit (self) LANG LOCALE_ARCHIVE;
-        AGDA_PACKAGE_PATH = concatMapStrings (x: x + ":") self.buildDependsAgdaShareAgda;
-        buildInputs = let
-          # Makes a wrapper available to the user. Very useful in
-          # nix-shell where all dependencies are -i'd.
-          agdaWrapper = writeShellScriptBin "agda" ''
-            exec ${self.agdaWithArgs} "$@"
-          '';
-        in [agdaWrapper] ++ self.buildDepends;
+    pname = "agdaWithPackages";
+    version = Agda.version;
+  in runCommandNoCC "${pname}-${version}" {
+    inherit pname version;
+    nativeBuildInputs = [ makeWrapper ];
+    passthru.unwrapped = Agda;
+  } ''
+    mkdir -p $out/bin
+    makeWrapper ${Agda}/bin/agda $out/bin/agda \
+      --add-flags "--with-compiler=${ghc}/bin/ghc" \
+      --add-flags "--library-file=${library-file}" \
+      --add-flags "--local-interfaces"
+    makeWrapper ${Agda}/bin/agda-mode $out/bin/agda-mode
+    ''; # Local interfaces has been added for now: See https://github.com/agda/agda/issues/4526
+
+  withPackages = arg: if builtins.isAttrs arg then withPackages' arg else withPackages' { pkgs = arg; };
+
+
+  defaults =
+    { pname
+    , buildInputs ? []
+    , everythingFile ? "./Everything.agda"
+    , libraryName ? pname
+    , libraryFile ? "${libraryName}.agda-lib"
+    , buildPhase ? null
+    , installPhase ? null
+    , ...
+    }: let
+      agdaWithArgs = withPackages (builtins.filter (p: p ? isAgdaDerivation) buildInputs);
+    in
+      {
+        inherit libraryName libraryFile;
+
+        isAgdaDerivation = true;
+
+        buildInputs = buildInputs ++ [ agdaWithArgs ];
+
+        buildPhase = if buildPhase != null then buildPhase else ''
+          runHook preBuild
+          agda -i ${dirOf everythingFile} ${everythingFile}
+          runHook postBuild
+        '';
+
+        installPhase = if installPhase != null then installPhase else ''
+          runHook preInstall
+          mkdir -p $out
+          find \( -name '*.agda' -or -name '*.agdai' -or -name '*.agda-lib' \) -exec cp -p --parents -t "$out" {} +
+          runHook postInstall
+        '';
       };
-    };
-  };
 in
-{ mkDerivation = args: let
-      super = defaults self // args self;
-      self  = super // extension self super;
-    in stdenv.mkDerivation self;
+{
+  mkDerivation = args: stdenv.mkDerivation (args // defaults args);
+
+  inherit withPackages withPackages';
 }
diff --git a/pkgs/development/libraries/agda/agda-prelude/default.nix b/pkgs/development/libraries/agda/agda-prelude/default.nix
index 86f21ad9b19..1709ce314d9 100644
--- a/pkgs/development/libraries/agda/agda-prelude/default.nix
+++ b/pkgs/development/libraries/agda/agda-prelude/default.nix
@@ -1,16 +1,16 @@
-{ stdenv, agda, fetchgit }:
+{ stdenv, mkDerivation, fetchFromGitHub }:
 
-agda.mkDerivation (self: rec {
+mkDerivation rec {
   version = "eacc961c2c312b7443109a7872f99d55557df317";
-  name = "agda-prelude-${version}";
+  pname = "agda-prelude";
 
-  src = fetchgit {
-    url = "https://github.com/UlfNorell/agda-prelude.git";
+  src = fetchFromGitHub {
+    owner = "UlfNorell";
+    repo = "agda-prelude";
     rev = version;
     sha256 = "0iql67hb1q0fn8dwkcx07brkdkxqfqrsbwjy71ndir0k7qzw7qv2";
   };
 
-  topSourceDirectories = [ "src" ];
   everythingFile = "src/Prelude.agda";
 
   meta = with stdenv.lib; {
@@ -18,6 +18,6 @@ agda.mkDerivation (self: rec {
     description = "Programming library for Agda";
     license = stdenv.lib.licenses.mit;
     platforms = stdenv.lib.platforms.unix;
-    maintainers = with maintainers; [ mudri ];
+    maintainers = with maintainers; [ mudri alexarice ];
   };
-})
+}
diff --git a/pkgs/development/libraries/agda/agda-iowa-stdlib/default.nix b/pkgs/development/libraries/agda/iowa-stdlib/default.nix
index 23013bfbc32..9cda6ceec13 100644
--- a/pkgs/development/libraries/agda/agda-iowa-stdlib/default.nix
+++ b/pkgs/development/libraries/agda/iowa-stdlib/default.nix
@@ -1,8 +1,8 @@
-{ stdenv, agda, fetchFromGitHub }:
+{ stdenv, mkDerivation, fetchFromGitHub }:
 
-agda.mkDerivation (self: rec {
+mkDerivation (rec {
   version = "1.5.0";
-  name = "agda-iowa-stdlib-${version}";
+  pname = "iowa-stdlib";
 
   src = fetchFromGitHub {
     owner = "cedille";
@@ -11,7 +11,9 @@ agda.mkDerivation (self: rec {
     sha256 = "0dlis6v6nzbscf713cmwlx8h9n2gxghci8y21qak3hp18gkxdp0g";
   };
 
-  sourceDirectories = [ "./." ];
+  libraryFile = "";
+  libraryName = "IAL-1.3";
+
   buildPhase = ''
     patchShebangs find-deps.sh
     make
@@ -22,6 +24,6 @@ agda.mkDerivation (self: rec {
     description = "Agda standard library developed at Iowa";
     license = stdenv.lib.licenses.free;
     platforms = stdenv.lib.platforms.unix;
-    maintainers = with stdenv.lib.maintainers; [ ];
+    maintainers = with stdenv.lib.maintainers; [ alexarice ];
   };
 })
diff --git a/pkgs/development/libraries/agda/agda-stdlib/default.nix b/pkgs/development/libraries/agda/standard-library/default.nix
index 6647677f71c..6d85d560a9b 100644
--- a/pkgs/development/libraries/agda/agda-stdlib/default.nix
+++ b/pkgs/development/libraries/agda/standard-library/default.nix
@@ -1,8 +1,8 @@
-{ stdenv, agda, fetchFromGitHub, ghcWithPackages }:
+{ stdenv, mkDerivation, fetchFromGitHub, ghcWithPackages }:
 
-agda.mkDerivation (self: rec {
+mkDerivation rec {
+  pname = "standard-library";
   version = "1.1";
-  name = "agda-stdlib-${version}";
 
   src = fetchFromGitHub {
     repo = "agda-stdlib";
@@ -16,13 +16,11 @@ agda.mkDerivation (self: rec {
     runhaskell GenerateEverything.hs
   '';
 
-  topSourceDirectories = [ "src" ];
-
   meta = with stdenv.lib; {
     homepage = "https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary";
     description = "A standard library for use with the Agda compiler";
     license = stdenv.lib.licenses.mit;
     platforms = stdenv.lib.platforms.unix;
-    maintainers = with maintainers; [ jwiegley mudri ];
+    maintainers = with maintainers; [ jwiegley mudri alexarice ];
   };
-})
+}
diff --git a/pkgs/top-level/agda-packages.nix b/pkgs/top-level/agda-packages.nix
new file mode 100644
index 00000000000..5bd57b5dec8
--- /dev/null
+++ b/pkgs/top-level/agda-packages.nix
@@ -0,0 +1,24 @@
+{ pkgs, lib, callPackage, newScope, Agda }:
+
+let
+  mkAgdaPackages = Agda: lib.makeScope newScope (mkAgdaPackages' Agda);
+  mkAgdaPackages' = Agda: self: let
+    callPackage = self.callPackage;
+    inherit (callPackage ../build-support/agda {
+      inherit Agda self;
+      inherit (pkgs.haskellPackages) ghcWithPackages;
+    }) withPackages mkDerivation;
+  in {
+    inherit mkDerivation;
+
+    agda = withPackages [] // { inherit 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 { };
+  };
+in mkAgdaPackages Agda
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index ea1a0791762..8c1414803ee 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -15128,19 +15128,10 @@ in
 
   ### DEVELOPMENT / LIBRARIES / AGDA
 
-  agda = callPackage ../build-support/agda {
-    glibcLocales = if pkgs.stdenv.isLinux then pkgs.glibcLocales else null;
-    extension = self : super : { };
+  agdaPackages = callPackage ./agda-packages.nix {
     inherit (haskellPackages) Agda;
   };
-
-  agdaIowaStdlib = callPackage ../development/libraries/agda/agda-iowa-stdlib { };
-
-  agdaPrelude = callPackage ../development/libraries/agda/agda-prelude { };
-
-  AgdaStdlib = callPackage ../development/libraries/agda/agda-stdlib {
-    inherit (haskellPackages) ghcWithPackages;
-  };
+  agda = agdaPackages.agda;
 
   ### DEVELOPMENT / LIBRARIES / JAVA
 
diff --git a/pkgs/top-level/release.nix b/pkgs/top-level/release.nix
index e0723523f4e..60a4a679f16 100644
--- a/pkgs/top-level/release.nix
+++ b/pkgs/top-level/release.nix
@@ -181,6 +181,7 @@ let
       haskell.compiler = packagePlatforms pkgs.haskell.compiler;
       haskellPackages = packagePlatforms pkgs.haskellPackages;
       idrisPackages = packagePlatforms pkgs.idrisPackages;
+      agdaPackages = packagePlatforms pkgs.agdaPackages;
 
       tests = packagePlatforms pkgs.tests;