diff options
| -rw-r--r-- | doc/languages-frameworks/agda.section.md | 96 | ||||
| -rw-r--r-- | doc/languages-frameworks/index.xml | 1 | ||||
| -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 |
9 files changed, 207 insertions, 113 deletions
diff --git a/doc/languages-frameworks/agda.section.md b/doc/languages-frameworks/agda.section.md new file mode 100644 index 00000000000..7a5dc767b7c --- /dev/null +++ b/doc/languages-frameworks/agda.section.md @@ -0,0 +1,96 @@ +--- +title: Agda +author: Alex Rice (alexarice) +date: 2020-01-06 +--- +# Agda + +## How to use Agda + +Agda can be installed from `agda`: +``` +$ nix-env -iA agda +``` + +To use agda with libraries, the `agda.withPackages` function can be used. This function either takes: ++ A list of packages, ++ or a function which returns a list of packages when given the `agdaPackages` attribute set, ++ or an attribute set containing a list of packages and a GHC derivation for compilation (see below). + +For example, suppose we wanted a version of agda which has access to the standard library. This can be obtained with the expressions: + +``` +agda.withPackages [ agdaPackages.standard-library ] +``` + +or + +``` +agda.withPackages (p: [ p.standard-library ]) +``` + +or can be called as in the [Compiling Agda](#compiling-agda) section. + +If you want to use a library in your home directory (for instance if it is a development version) then typecheck it manually (using `agda.withPackages` if necessary) and then override the `src` attribute of the package to point to your local repository. + +Agda will not by default use these libraries. To tell agda to use the library we have some options: +- Call `agda` with the library flag: +``` +$ agda -l standard-library -i . MyFile.agda +``` +- Write a `my-library.agda-lib` file for the project you are working on which may look like: +``` +name: my-library +include: . +depends: standard-library +``` +- Create the file `~/.agda/defaults` and add any libraries you want to use by default. + +More information can be found in the [official Agda documentation on library management](https://agda.readthedocs.io/en/v2.6.1/tools/package-system.html). + +## Compiling Agda +Agda modules can be compiled with the `--compile` flag. A version of `ghc` with `ieee` is made available to the Agda program via the `--with-compiler` flag. +This can be overridden by a different version of `ghc` as follows: + +``` +agda.withPackages { + pkgs = [ ... ]; + ghc = haskell.compiler.ghcHEAD; +} +``` + +## Writing Agda packages +To write a nix derivation for an agda library, first check that the library has a `*.agda-lib` file. + +A derivation can then be written using `agdaPackages.mkDerivation`. This has similar arguments to `stdenv.mkDerivation` with the following additions: ++ `everythingFile` can be used to specify the location of the `Everything.agda` file, defaulting to `./Everything.agda`. If this file does not exist then either it should be patched in or the `buildPhase` should be overridden (see below). ++ `libraryName` should be the name that appears in the `*.agda-lib` file, defaulting to `pname`. ++ `libraryFile` should be the file name of the `*.agda-lib` file, defaulting to `${libraryName}.agda-lib`. + +The build phase for `agdaPackages.mkDerivation` simply runs `agda` on the `Everything.agda` file. If something else is needed to build the package (e.g. `make`) then the `buildPhase` should be overridden (or a `preBuild` or `configurePhase` can be used if there are steps that need to be done prior to checking the `Everything.agda` file). `agda` and the Agda libraries contained in `buildInputs` are made available during the build phase. The install phase simply copies all `.agda`, `.agdai` and `.agda-lib` files to the output directory. Again, this can be overridden. + +To add an agda package to `nixpkgs`, the derivation should be written to `pkgs/development/libraries/agda/${library-name}/` and an entry should be added to `pkgs/top-level/agda-packages.nix`. Here it is called in a scope with access to all other agda libraries, so the top line of the `default.nix` can look like: +``` +{ mkDerivation, standard-library, fetchFromGitHub }: +``` +and `mkDerivation` should be called instead of `agdaPackages.mkDerivation`. Here is an example skeleton derivation for iowa-stdlib: + +``` +mkDerivation { + version = "1.5.0"; + pname = "iowa-stdlib"; + + src = ... + + libraryFile = ""; + libraryName = "IAL-1.3"; + + buildPhase = '' + patchShebangs find-deps.sh + make + ''; +} +``` +This library has a file called `.agda-lib`, and so we give an empty string to `libraryFile` as nothing precedes `.agda-lib` in the filename. This file contains `name: IAL-1.3`, and so we let `libraryName = "IAL-1.3"`. This library does not use an `Everything.agda` file and instead has a Makefile, so there is no need to set `everythingFile` and we set a custom `buildPhase`. + +When writing an agda package it is essential to make sure that no `.agda-lib` file gets added to the store as a single file (for example by using `writeText`). This causes agda to think that the nix store is a agda library and it will attempt to write to it whenever it typechecks something. See [https://github.com/agda/agda/issues/4613](https://github.com/agda/agda/issues/4613). diff --git a/doc/languages-frameworks/index.xml b/doc/languages-frameworks/index.xml index 9364c764bbf..97202751f7d 100644 --- a/doc/languages-frameworks/index.xml +++ b/doc/languages-frameworks/index.xml @@ -5,6 +5,7 @@ <para> The <link linkend="chap-stdenv">standard build environment</link> makes it easy to build typical Autotools-based packages with very little code. Any other kind of package can be accomodated by overriding the appropriate phases of <literal>stdenv</literal>. However, there are specialised functions in Nixpkgs to easily build packages for other programming languages, such as Perl or Haskell. These are described in this chapter. </para> + <xi:include href="agda.section.xml" /> <xi:include href="android.section.xml" /> <xi:include href="beam.xml" /> <xi:include href="bower.xml" /> diff --git a/pkgs/build-support/agda/default.nix b/pkgs/build-support/agda/default.nix index 0d054eaa546..205aff55573 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 86f21ad9b19..1709ce314d9 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 23013bfbc32..9cda6ceec13 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 6647677f71c..6d85d560a9b 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 00000000000..5bd57b5dec8 --- /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 ea1a0791762..8c1414803ee 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 e0723523f4e..60a4a679f16 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; |