agda: Remove the --local-interfaces flag

Upstream now provides a library file for the builtin library and ensured
that the existing interface files will be used regardless of whether
--local-interfaces is in effect. Hence, Agda will not try to write to
the Nix store anymore except if the build flags are changed.
This commit is contained in:
ibbem 2024-02-26 09:13:28 +01:00
parent 10c80b9934
commit 1642654453
3 changed files with 6 additions and 14 deletions

View file

@ -25,13 +25,6 @@ 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")

View file

@ -31,10 +31,9 @@ let
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"
--add-flags "--library-file=${library-file}"
ln -s ${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; };
@ -82,7 +81,7 @@ let
installPhase = if installPhase != null then installPhase else ''
runHook preInstall
mkdir -p $out
find -not \( -path ${everythingFile} -or -path ${lib.interfaceFile everythingFile} \) -and \( ${concatMapStringsSep " -or " (p: "-name '*.${p}'") (extensions ++ extraExtensions)} \) -exec cp -p --parents -t "$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" {} +
runHook postInstall
'';

View file

@ -3,10 +3,10 @@
/* 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 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 = agdaFile: 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.