From 226299e1a2e8dbc9ee8b10042182d8a1f47d7f16 Mon Sep 17 00:00:00 2001
From: Alexander Ben Nasrallah <me@abn.sh>
Date: Mon, 18 Jan 2021 20:01:31 +0100
Subject: [PATCH 1/2] agdaPackages.mkDerivation: don't install Everything
 module

The Everthing module is not part of a library and should therefore
not be copied to the nix store.

This is particularly bad, if the Everything module is defined in
an agda library included directory, e.g. consider an agda-lib with

    include: .

and Everything.agda in the project root (.), in which case the
Everything module would become part of the library.
If multiple such projects are in the dependency tree, the Everything
module becomes ambiguous and the build would fail.
---
 nixos/tests/agda.nix                |  7 +++++++
 pkgs/build-support/agda/default.nix |  2 +-
 pkgs/build-support/agda/lib.nix     | 10 ++++++++++
 pkgs/top-level/agda-packages.nix    |  2 ++
 4 files changed, 20 insertions(+), 1 deletion(-)
 create mode 100644 pkgs/build-support/agda/lib.nix

diff --git a/nixos/tests/agda.nix b/nixos/tests/agda.nix
index bbdeb7395aa7..61d99fe50500 100644
--- a/nixos/tests/agda.nix
+++ b/nixos/tests/agda.nix
@@ -23,6 +23,13 @@ in
   };
 
   testScript = ''
+    assert (
+        "${pkgs.agdaPackages.lib.interfaceFile "Everything.agda"}" == "Everything.agdai"
+    ), "wrong interface file for Everything.agda"
+    assert (
+        "${pkgs.agdaPackages.lib.interfaceFile "tmp/Everything.agda.md"}" == "tmp/Everything.agdai"
+    ), "wrong interface file for tmp/Everything.agda.md"
+
     # Minimal script that typechecks
     machine.succeed("touch TestEmpty.agda")
     machine.succeed("agda TestEmpty.agda")
diff --git a/pkgs/build-support/agda/default.nix b/pkgs/build-support/agda/default.nix
index 3c973e8cc0ac..01855bf2614c 100644
--- a/pkgs/build-support/agda/default.nix
+++ b/pkgs/build-support/agda/default.nix
@@ -70,7 +70,7 @@ let
         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" {} +
+          find -not \( -path ${everythingFile} -or -path ${lib.interfaceFile everythingFile} \) -and \( ${concatMapStringsSep " -or " (p: "-name '*.${p}'") (extensions ++ extraExtensions)} \) -exec cp -p --parents -t "$out" {} +
           runHook postInstall
         '';
       };
diff --git a/pkgs/build-support/agda/lib.nix b/pkgs/build-support/agda/lib.nix
new file mode 100644
index 000000000000..976151a8283c
--- /dev/null
+++ b/pkgs/build-support/agda/lib.nix
@@ -0,0 +1,10 @@
+{ lib }:
+{
+  /* Returns the Agda interface file to a given Agda file.
+  *
+  * Examples:
+  * interfaceFile "Everything.agda" == "Everything.agdai"
+  * interfaceFile "src/Everything.lagda.tex" == "src/Everything.agdai"
+  */
+  interfaceFile = agdaFile: lib.head (builtins.match ''(.*\.)l?agda(\.(md|org|rst|tex))?'' agdaFile) + "agdai";
+}
diff --git a/pkgs/top-level/agda-packages.nix b/pkgs/top-level/agda-packages.nix
index 601ab6d42b9d..7434134d28f2 100644
--- a/pkgs/top-level/agda-packages.nix
+++ b/pkgs/top-level/agda-packages.nix
@@ -11,6 +11,8 @@ let
   in {
     inherit mkDerivation;
 
+    lib = lib.extend (final: prev: import ../build-support/agda/lib.nix { lib = prev; });
+
     agda = withPackages [] // { inherit withPackages; };
 
     standard-library = callPackage ../development/libraries/agda/standard-library {

From 688ebdc77dcc73163da651ad1bfc7509266df67e Mon Sep 17 00:00:00 2001
From: Alexander Ben Nasrallah <me@abn.sh>
Date: Fri, 22 Jan 2021 15:16:53 +0100
Subject: [PATCH 2/2] agdaPackages.standard-library: don't install Everything
 files

---
 pkgs/development/libraries/agda/standard-library/default.nix | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/pkgs/development/libraries/agda/standard-library/default.nix b/pkgs/development/libraries/agda/standard-library/default.nix
index 1d8dc03bbde9..39e30b3c3711 100644
--- a/pkgs/development/libraries/agda/standard-library/default.nix
+++ b/pkgs/development/libraries/agda/standard-library/default.nix
@@ -14,6 +14,9 @@ mkDerivation rec {
   nativeBuildInputs = [ (ghcWithPackages (self : [ self.filemanip ])) ];
   preConfigure = ''
     runhaskell GenerateEverything.hs
+    # We will only build/consider Everything.agda, in particular we don't want Everything*.agda
+    # do be copied to the store.
+    rm EverythingSafe.agda EverythingSafeGuardedness.agda EverythingSafeSizedTypes.agda
   '';
 
   meta = with lib; {