diff options
author | Alex Rice <alexrice999@hotmail.co.uk> | 2019-12-29 12:14:16 +0000 |
---|---|---|
committer | Alex Rice <alexrice999@hotmail.co.uk> | 2020-05-14 20:54:11 +0100 |
commit | d30e2468e0c7875d3d4d47404f52647ccea76fcf (patch) | |
tree | 988b1d96ad8fe33e6c287049ae5b013311111d28 /pkgs | |
parent | 6cbaa256fab7df0d213be5caa14a6a29c9a47ed0 (diff) |
agda: rework builder
Diffstat (limited to 'pkgs')
-rw-r--r-- | pkgs/build-support/agda/default.nix | 145 | ||||
-rw-r--r-- | pkgs/development/libraries/agda/agda-prelude/default.nix | 16 | ||||
-rw-r--r-- | pkgs/development/libraries/agda/iowa-stdlib/default.nix (renamed from pkgs/development/libraries/agda/agda-iowa-stdlib/default.nix) | 12 | ||||
-rw-r--r-- | pkgs/development/libraries/agda/standard-library/default.nix (renamed from pkgs/development/libraries/agda/agda-stdlib/default.nix) | 12 | ||||
-rw-r--r-- | pkgs/top-level/agda-packages.nix | 24 | ||||
-rw-r--r-- | pkgs/top-level/all-packages.nix | 13 | ||||
-rw-r--r-- | pkgs/top-level/release.nix | 1 |
7 files changed, 110 insertions, 113 deletions
diff --git a/pkgs/build-support/agda/default.nix b/pkgs/build-support/agda/default.nix index 0d054eaa54690..205aff5557307 100644 --- a/pkgs/build-support/agda/default.nix +++ b/pkgs/build-support/agda/default.nix @@ -1,90 +1,71 @@ -# Builder for Agda packages. Mostly inspired by the cabal builder. +# Builder for Agda packages. -{ stdenv, Agda, glibcLocales -, writeShellScriptBin -, extension ? (self: super: {}) -}: +{ stdenv, lib, self, Agda, runCommandNoCC, makeWrapper, writeText, mkShell, ghcWithPackages }: -with stdenv.lib.strings; +with lib.strings; let - defaults = self : { - # There is no Hackage for Agda so we require src. - inherit (self) src name; - - isAgdaPackage = true; - - buildInputs = [ Agda ] ++ self.buildDepends; - buildDepends = []; - - buildDependsAgda = stdenv.lib.filter - (dep: dep ? isAgdaPackage && dep.isAgdaPackage) - self.buildDepends; - buildDependsAgdaShareAgda = map (x: x + "/share/agda") self.buildDependsAgda; - - # Not much choice here ;) - LANG = "en_US.UTF-8"; - LOCALE_ARCHIVE = stdenv.lib.optionalString - stdenv.isLinux - "${glibcLocales}/lib/locale/locale-archive"; - - everythingFile = "Everything.agda"; - - propagatedBuildInputs = self.buildDependsAgda; - propagatedUserEnvPkgs = self.buildDependsAgda; - - # Immediate source directories under which modules can be found. - sourceDirectories = [ ]; - - # This is used if we have a top-level element that only serves - # as the container for the source and we only care about its - # contents. The directories put here will have their - # *contents* copied over as opposed to sourceDirectories which - # would make a direct copy of the whole thing. - topSourceDirectories = [ "src" ]; - - # FIXME: `dirOf self.everythingFile` is what we really want, not hardcoded "./" - includeDirs = self.buildDependsAgdaShareAgda - ++ self.sourceDirectories ++ self.topSourceDirectories - ++ [ "." ]; - buildFlags = stdenv.lib.concatMap (x: ["-i" x]) self.includeDirs; - - agdaWithArgs = "${Agda}/bin/agda ${toString self.buildFlags}"; - - buildPhase = '' - runHook preBuild - ${self.agdaWithArgs} ${self.everythingFile} - runHook postBuild + withPackages' = { + pkgs, + ghc ? ghcWithPackages (p: with p; [ ieee ]) + }: let + pkgs' = if builtins.isList pkgs then pkgs else pkgs self; + library-file = writeText "libraries" '' + ${(concatMapStringsSep "\n" (p: "${p}/${p.libraryFile}") pkgs')} ''; - - installPhase = let - srcFiles = self.sourceDirectories - ++ map (x: x + "/*") self.topSourceDirectories; - in '' - runHook preInstall - mkdir -p $out/share/agda - cp -pR ${concatStringsSep " " srcFiles} $out/share/agda - runHook postInstall - ''; - - passthru = { - env = stdenv.mkDerivation { - name = "interactive-${self.name}"; - inherit (self) LANG LOCALE_ARCHIVE; - AGDA_PACKAGE_PATH = concatMapStrings (x: x + ":") self.buildDependsAgdaShareAgda; - buildInputs = let - # Makes a wrapper available to the user. Very useful in - # nix-shell where all dependencies are -i'd. - agdaWrapper = writeShellScriptBin "agda" '' - exec ${self.agdaWithArgs} "$@" - ''; - in [agdaWrapper] ++ self.buildDepends; + pname = "agdaWithPackages"; + version = Agda.version; + in runCommandNoCC "${pname}-${version}" { + inherit pname version; + nativeBuildInputs = [ makeWrapper ]; + passthru.unwrapped = Agda; + } '' + 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" + makeWrapper ${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; }; + + + defaults = + { pname + , buildInputs ? [] + , everythingFile ? "./Everything.agda" + , libraryName ? pname + , libraryFile ? "${libraryName}.agda-lib" + , buildPhase ? null + , installPhase ? null + , ... + }: let + agdaWithArgs = withPackages (builtins.filter (p: p ? isAgdaDerivation) buildInputs); + in + { + inherit libraryName libraryFile; + + isAgdaDerivation = true; + + buildInputs = buildInputs ++ [ agdaWithArgs ]; + + buildPhase = if buildPhase != null then buildPhase else '' + runHook preBuild + agda -i ${dirOf everythingFile} ${everythingFile} + runHook postBuild + ''; + + installPhase = if installPhase != null then installPhase else '' + runHook preInstall + mkdir -p $out + find \( -name '*.agda' -or -name '*.agdai' -or -name '*.agda-lib' \) -exec cp -p --parents -t "$out" {} + + runHook postInstall + ''; }; - }; - }; in -{ mkDerivation = args: let - super = defaults self // args self; - self = super // extension self super; - in stdenv.mkDerivation self; +{ + mkDerivation = args: stdenv.mkDerivation (args // defaults args); + + inherit withPackages withPackages'; } diff --git a/pkgs/development/libraries/agda/agda-prelude/default.nix b/pkgs/development/libraries/agda/agda-prelude/default.nix index 86f21ad9b19c4..1709ce314d96f 100644 --- a/pkgs/development/libraries/agda/agda-prelude/default.nix +++ b/pkgs/development/libraries/agda/agda-prelude/default.nix @@ -1,16 +1,16 @@ -{ stdenv, agda, fetchgit }: +{ stdenv, mkDerivation, fetchFromGitHub }: -agda.mkDerivation (self: rec { +mkDerivation rec { version = "eacc961c2c312b7443109a7872f99d55557df317"; - name = "agda-prelude-${version}"; + pname = "agda-prelude"; - src = fetchgit { - url = "https://github.com/UlfNorell/agda-prelude.git"; + src = fetchFromGitHub { + owner = "UlfNorell"; + repo = "agda-prelude"; rev = version; sha256 = "0iql67hb1q0fn8dwkcx07brkdkxqfqrsbwjy71ndir0k7qzw7qv2"; }; - topSourceDirectories = [ "src" ]; everythingFile = "src/Prelude.agda"; meta = with stdenv.lib; { @@ -18,6 +18,6 @@ agda.mkDerivation (self: rec { description = "Programming library for Agda"; license = stdenv.lib.licenses.mit; platforms = stdenv.lib.platforms.unix; - maintainers = with maintainers; [ mudri ]; + maintainers = with maintainers; [ mudri alexarice ]; }; -}) +} diff --git a/pkgs/development/libraries/agda/agda-iowa-stdlib/default.nix b/pkgs/development/libraries/agda/iowa-stdlib/default.nix index 23013bfbc3245..9cda6ceec1332 100644 --- a/pkgs/development/libraries/agda/agda-iowa-stdlib/default.nix +++ b/pkgs/development/libraries/agda/iowa-stdlib/default.nix @@ -1,8 +1,8 @@ -{ stdenv, agda, fetchFromGitHub }: +{ stdenv, mkDerivation, fetchFromGitHub }: -agda.mkDerivation (self: rec { +mkDerivation (rec { version = "1.5.0"; - name = "agda-iowa-stdlib-${version}"; + pname = "iowa-stdlib"; src = fetchFromGitHub { owner = "cedille"; @@ -11,7 +11,9 @@ agda.mkDerivation (self: rec { sha256 = "0dlis6v6nzbscf713cmwlx8h9n2gxghci8y21qak3hp18gkxdp0g"; }; - sourceDirectories = [ "./." ]; + libraryFile = ""; + libraryName = "IAL-1.3"; + buildPhase = '' patchShebangs find-deps.sh make @@ -22,6 +24,6 @@ agda.mkDerivation (self: rec { description = "Agda standard library developed at Iowa"; license = stdenv.lib.licenses.free; platforms = stdenv.lib.platforms.unix; - maintainers = with stdenv.lib.maintainers; [ ]; + maintainers = with stdenv.lib.maintainers; [ alexarice ]; }; }) diff --git a/pkgs/development/libraries/agda/agda-stdlib/default.nix b/pkgs/development/libraries/agda/standard-library/default.nix index 6647677f71c08..6d85d560a9bd7 100644 --- a/pkgs/development/libraries/agda/agda-stdlib/default.nix +++ b/pkgs/development/libraries/agda/standard-library/default.nix @@ -1,8 +1,8 @@ -{ stdenv, agda, fetchFromGitHub, ghcWithPackages }: +{ stdenv, mkDerivation, fetchFromGitHub, ghcWithPackages }: -agda.mkDerivation (self: rec { +mkDerivation rec { + pname = "standard-library"; version = "1.1"; - name = "agda-stdlib-${version}"; src = fetchFromGitHub { repo = "agda-stdlib"; @@ -16,13 +16,11 @@ agda.mkDerivation (self: rec { runhaskell GenerateEverything.hs ''; - topSourceDirectories = [ "src" ]; - meta = with stdenv.lib; { homepage = "https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary"; description = "A standard library for use with the Agda compiler"; license = stdenv.lib.licenses.mit; platforms = stdenv.lib.platforms.unix; - maintainers = with maintainers; [ jwiegley mudri ]; + maintainers = with maintainers; [ jwiegley mudri alexarice ]; }; -}) +} diff --git a/pkgs/top-level/agda-packages.nix b/pkgs/top-level/agda-packages.nix new file mode 100644 index 0000000000000..5bd57b5dec893 --- /dev/null +++ b/pkgs/top-level/agda-packages.nix @@ -0,0 +1,24 @@ +{ pkgs, lib, callPackage, newScope, Agda }: + +let + mkAgdaPackages = Agda: lib.makeScope newScope (mkAgdaPackages' Agda); + mkAgdaPackages' = Agda: self: let + callPackage = self.callPackage; + inherit (callPackage ../build-support/agda { + inherit Agda self; + inherit (pkgs.haskellPackages) ghcWithPackages; + }) withPackages mkDerivation; + in { + inherit mkDerivation; + + agda = withPackages [] // { inherit withPackages; }; + + standard-library = callPackage ../development/libraries/agda/standard-library { + inherit (pkgs.haskellPackages) ghcWithPackages; + }; + + iowa-stdlib = callPackage ../development/libraries/agda/iowa-stdlib { }; + + agda-prelude = callPackage ../development/libraries/agda/agda-prelude { }; + }; +in mkAgdaPackages Agda diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index ea1a07917621f..8c1414803eeb1 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -15128,19 +15128,10 @@ in ### DEVELOPMENT / LIBRARIES / AGDA - agda = callPackage ../build-support/agda { - glibcLocales = if pkgs.stdenv.isLinux then pkgs.glibcLocales else null; - extension = self : super : { }; + agdaPackages = callPackage ./agda-packages.nix { inherit (haskellPackages) Agda; }; - - agdaIowaStdlib = callPackage ../development/libraries/agda/agda-iowa-stdlib { }; - - agdaPrelude = callPackage ../development/libraries/agda/agda-prelude { }; - - AgdaStdlib = callPackage ../development/libraries/agda/agda-stdlib { - inherit (haskellPackages) ghcWithPackages; - }; + agda = agdaPackages.agda; ### DEVELOPMENT / LIBRARIES / JAVA diff --git a/pkgs/top-level/release.nix b/pkgs/top-level/release.nix index e0723523f4e51..60a4a679f1611 100644 --- a/pkgs/top-level/release.nix +++ b/pkgs/top-level/release.nix @@ -181,6 +181,7 @@ let haskell.compiler = packagePlatforms pkgs.haskell.compiler; haskellPackages = packagePlatforms pkgs.haskellPackages; idrisPackages = packagePlatforms pkgs.idrisPackages; + agdaPackages = packagePlatforms pkgs.agdaPackages; tests = packagePlatforms pkgs.tests; |