Dev agda shellfor

doc/languages-frameworks/agda.section.md

@@ -158,6 +158,26 @@ This can be overridden.
 
 By default, Agda sources are files ending on `.agda`, or literate Agda files ending on `.lagda`, `.lagda.tex`, `.lagda.org`, `.lagda.md`, `.lagda.rst`. The list of recognised Agda source extensions can be extended by setting the `extraExtensions` config variable.
 
+## Creating a development environment {#creating-a-development-environment}
+
+You can create a `nix-shell` containing `agda` with all dependency libraries with the function `agdaPackages.shellFor`.
+Assuming that you have already created an agda package `mypkg` using `agdaPackages.mkDerivation`,
+create a file `shell.nix` containing:
+
+```nix
+{ nixpkgs ? import <nixpkgs> {} }:
+(nixpkgs.pkgs.agdaPackages.shellFor (import ./mypkg.nix))
+```
+
+For convenience, you can also arrive at the same result by accessing the `env` attribute of an Agda derivation:
+
+```nix
+(import ./mypkg.nix).env
+```
+
+This will bring `agda` in scope with all dependencies of your package,
+but not build your package itself (which is useful if you are developing it currently).
+
 ## Adding Agda packages to Nixpkgs {#adding-agda-packages-to-nixpkgs}
 
 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:

pkgs/build-support/agda/default.nix

@@ -44,6 +44,13 @@ let
     "lagda.tex"
   ];
 
+  filterAgdaBuildInputs = builtins.filter (p: p ? isAgdaDerivation);
+
+  shellFor = agdaDrv: mkShell {
+    buildInputs = [ (withPackages (filterAgdaBuildInputs agdaDrv.buildInputs)) ];
+    inputsFrom = agdaDrv.buildInputs ++ agdaDrv.nativeBuildInputs;
+  };
+
   defaults =
     { pname
     , meta
@@ -56,7 +63,7 @@ let
     , extraExtensions ? []
     , ...
     }: let
-      agdaWithArgs = withPackages (builtins.filter (p: p ? isAgdaDerivation) buildInputs);
+      agdaWithArgs = withPackages (filterAgdaBuildInputs buildInputs);
     in
       {
         inherit libraryName libraryFile;
@@ -81,7 +88,7 @@ let
       };
 in
 {
-  mkDerivation = args: stdenv.mkDerivation (args // defaults args);
+  mkDerivation = args: (lib.extends (self: super: super // { env = shellFor super; }) stdenv.mkDerivation (args // defaults args));
 
-  inherit withPackages withPackages';
+  inherit withPackages withPackages' shellFor;
 }

pkgs/top-level/agda-packages.nix

@@ -7,9 +7,9 @@ let
     inherit (callPackage ../build-support/agda {
       inherit Agda self;
       inherit (pkgs.haskellPackages) ghcWithPackages;
-    }) withPackages mkDerivation;
+    }) withPackages mkDerivation shellFor;
   in {
-    inherit mkDerivation;
+    inherit mkDerivation shellFor;
 
     lib = lib.extend (final: prev: import ../build-support/agda/lib.nix { lib = prev; });