diff options
| author | Alexander Ben Nasrallah <me@abn.sh> | 2021-01-18 20:01:31 +0100 |
|---|---|---|
| committer | Alexander Ben Nasrallah <me@abn.sh> | 2021-01-24 17:30:01 +0100 |
| commit | 226299e1a2e8dbc9ee8b10042182d8a1f47d7f16 (patch) | |
| tree | 83dc1d3fb4e1bc6a5e9828fb4e649031942b0da8 | |
| parent | b929be75dcd605b4233bb69372e1c8b1d7449f47 (diff) | |
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.
| -rw-r--r-- | nixos/tests/agda.nix | 7 | ||||
| -rw-r--r-- | pkgs/build-support/agda/default.nix | 2 | ||||
| -rw-r--r-- | pkgs/build-support/agda/lib.nix | 10 | ||||
| -rw-r--r-- | pkgs/top-level/agda-packages.nix | 2 |
4 files changed, 20 insertions, 1 deletions
diff --git a/nixos/tests/agda.nix b/nixos/tests/agda.nix index bbdeb7395aa7e..61d99fe505008 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 3c973e8cc0acb..01855bf2614cd 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 0000000000000..976151a8283c6 --- /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 601ab6d42b9dc..7434134d28f29 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 { |