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.
wip/yesman
Alexander Ben Nasrallah 3 years ago
parent b929be75dc
commit 226299e1a2
No known key found for this signature in database
GPG Key ID: DF6D22A22FA2D5A8
  1. 7
      nixos/tests/agda.nix
  2. 2
      pkgs/build-support/agda/default.nix
  3. 10
      pkgs/build-support/agda/lib.nix
  4. 2
      pkgs/top-level/agda-packages.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")

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

@ -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";
}

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

Loading…
Cancel
Save