From b9343ad4c63f7fb9b72690c018c1ff4a3650d2a4 Mon Sep 17 00:00:00 2001
From: ibbem <ibbem@ibbem.net>
Date: Thu, 29 Feb 2024 18:03:06 +0100
Subject: [PATCH] agda: Don't be too picky about `everythingFile`

The `-path` test of `find` does string comparison, not path comparison.
Hence, the format of `everythingFile` needed to be very specific. Now,
it can be denormalized (e.g. it can contain `/./`) and an error is
emitted if the everything file or its interface file can't be removed.
---
 pkgs/build-support/agda/default.nix | 3 ++-
 pkgs/build-support/agda/lib.nix     | 8 +++++---
 2 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/pkgs/build-support/agda/default.nix b/pkgs/build-support/agda/default.nix
index 397e6d89b933..681d1ea681bb 100644
--- a/pkgs/build-support/agda/default.nix
+++ b/pkgs/build-support/agda/default.nix
@@ -75,13 +75,14 @@ let
         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 -not \( -path ${everythingFile} -or -path ${lib.interfaceFile Agda.version everythingFile} \) -and \( ${concatMapStringsSep " -or " (p: "-name '*.${p}'") (extensions ++ extraExtensions)} \) -exec cp -p --parents -t "$out" {} +
+          find \( ${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
index 9346b569dcda..63fa6ccddba6 100644
--- a/pkgs/build-support/agda/lib.nix
+++ b/pkgs/build-support/agda/lib.nix
@@ -2,11 +2,13 @@
 {
   /* Returns the Agda interface file to a given Agda file.
   *
+  * The resulting path may not be normalized.
+  *
   * Examples:
-  * interfaceFile pkgs.agda.version "./Everything.agda" == "./_build/2.6.4.3/agda/Everything.agdai"
-  * interfaceFile pkgs.agda.version "./src/Everything.lagda.tex" == "./_build/2.6.4.3/agda/src/Everything.agdai"
+  * interfaceFile pkgs.agda.version "./Everything.agda" == "_build/2.6.4.3/agda/./Everything.agdai"
+  * interfaceFile pkgs.agda.version "src/Everything.lagda.tex" == "_build/2.6.4.3/agda/src/Everything.agdai"
   */
-  interfaceFile = agdaVersion: agdaFile: "./_build/" + agdaVersion + "/agda/" + lib.head (builtins.match ''./(.*\.)l?agda(\.(md|org|rst|tex|typ))?'' agdaFile) + "agdai";
+  interfaceFile = agdaVersion: agdaFile: "_build/" + agdaVersion + "/agda/" + lib.head (builtins.match ''(.*\.)l?agda(\.(md|org|rst|tex|typ))?'' agdaFile) + "agdai";
 
   /* Takes an arbitrary derivation and says whether it is an agda library package
   *  that is not marked as broken.