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.
This commit is contained in:
ibbem 2024-02-29 18:03:06 +01:00
parent 1642654453
commit b9343ad4c6
2 changed files with 7 additions and 4 deletions

View File

@ -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
'';

View File

@ -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.