From 226299e1a2e8dbc9ee8b10042182d8a1f47d7f16 Mon Sep 17 00:00:00 2001 From: Alexander Ben Nasrallah Date: Mon, 18 Jan 2021 20:01:31 +0100 Subject: [PATCH] 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. --- nixos/tests/agda.nix | 7 +++++++ pkgs/build-support/agda/default.nix | 2 +- pkgs/build-support/agda/lib.nix | 10 ++++++++++ pkgs/top-level/agda-packages.nix | 2 ++ 4 files changed, 20 insertions(+), 1 deletion(-) create mode 100644 pkgs/build-support/agda/lib.nix diff --git a/nixos/tests/agda.nix b/nixos/tests/agda.nix index bbdeb7395aa..61d99fe5050 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 3c973e8cc0a..01855bf2614 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 00000000000..976151a8283 --- /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 601ab6d42b9..7434134d28f 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 {