From 34e8eea942e02a5562c2391e62fd1e5cfc154dda Mon Sep 17 00:00:00 2001
From: Shea Levy <shea@shealevy.com>
Date: Fri, 27 Nov 2015 07:56:11 -0500
Subject: [PATCH 1/8] Add with-packages wrapper for idris

---
 .../idris-modules/with-packages-wrapper.nix   | 38 +++++++++++++++++++
 1 file changed, 38 insertions(+)
 create mode 100644 pkgs/development/idris-modules/with-packages-wrapper.nix

diff --git a/pkgs/development/idris-modules/with-packages-wrapper.nix b/pkgs/development/idris-modules/with-packages-wrapper.nix
new file mode 100644
index 00000000000..e55fd2c3324
--- /dev/null
+++ b/pkgs/development/idris-modules/with-packages-wrapper.nix
@@ -0,0 +1,38 @@
+{ stdenv, idris, packages }: stdenv.mkDerivation {
+  inherit (idris) name;
+
+  inherit packages;
+
+  unpackPhase = ''
+    cat >idris.c <<EOF
+    #include <stdlib.h>
+    #include <unistd.h>
+    #include <stdio.h>
+
+    int main (int argc, char ** argv) {
+      /* idris currently only supports a single library path, so respect it if the user set it */
+      setenv("IDRIS_LIBRARY_PATH", "$out/lib/${idris.name}", 0);
+      execv("${idris}/bin/idris", argv);
+      perror("executing ${idris}/bin/idris");
+      return 127;
+    }
+    EOF
+  '';
+
+  buildPhase = ''
+    gcc -O3 -o idris idris.c
+  '';
+
+  installPhase = ''
+    mkdir -p $out/lib/${idris.name}
+    for package in $packages
+    do
+      ln -sv $package/lib/${idris.name}/* $out/lib/${idris.name}
+    done
+
+    mkdir -p $out/bin
+    mv idris $out/bin
+  '';
+
+  stripAllList = [ "bin" ];
+}

From 5898c2060433d803865df3a9af4408d0443de8b8 Mon Sep 17 00:00:00 2001
From: Shea Levy <shea@shealevy.com>
Date: Fri, 27 Nov 2015 08:19:50 -0500
Subject: [PATCH 2/8] Add idrisPackages to all-packages.nix

---
 pkgs/development/idris-modules/default.nix | 18 ++++++++++++++++++
 pkgs/top-level/all-packages.nix            |  2 ++
 2 files changed, 20 insertions(+)
 create mode 100644 pkgs/development/idris-modules/default.nix

diff --git a/pkgs/development/idris-modules/default.nix b/pkgs/development/idris-modules/default.nix
new file mode 100644
index 00000000000..d07619724fe
--- /dev/null
+++ b/pkgs/development/idris-modules/default.nix
@@ -0,0 +1,18 @@
+{ pkgs, idris, overrides ? (self: super: {}) }: let
+  inherit (pkgs.lib) callPackageWith fix' extends;
+
+  /* Taken from haskell-modules/default.nix, should probably abstract this away */
+  callPackageWithScope = scope: drv: args: (callPackageWith scope drv args) // {
+    overrideScope = f: callPackageWithScope (mkScope (fix' (extends f scope.__unfix__))) drv args;
+  };
+
+  mkScope = scope : pkgs // pkgs.xorg // pkgs.gnome // scope;
+
+  idrisPackages = self: let
+    defaultScope = mkScope self;
+
+    callPackage = callPackageWithScope defaultScope;
+  in {
+    withPackages = packages: callPackage ./with-packages-wrapper.nix { inherit packages idris; };
+  };
+in fix' (extends overrides idrisPackages)
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 760f3309be3..f482a74881c 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -4121,6 +4121,8 @@ let
 
   icedtea_web = icedtea8_web;
 
+  idrisPackages = callPackage ../development/idris-modules { inherit (haskellPackages) idris; };
+
   ikarus = callPackage ../development/compilers/ikarus { };
 
   intercal = callPackage ../development/compilers/intercal { };

From efbee054fd2dca2b14c729cf73aca7246c56d9f2 Mon Sep 17 00:00:00 2001
From: Shea Levy <shea@shealevy.com>
Date: Fri, 27 Nov 2015 09:35:59 -0500
Subject: [PATCH 3/8] Add builtin idris packages to idrisPackages

---
 .../idris-modules/build-builtin-package.nix   | 12 +++++++
 .../idris-modules/build-idris-package.nix     | 34 +++++++++++++++++++
 pkgs/development/idris-modules/default.nix    | 24 +++++++++++--
 .../idris-modules/with-packages-wrapper.nix   | 22 +++++++-----
 4 files changed, 82 insertions(+), 10 deletions(-)
 create mode 100644 pkgs/development/idris-modules/build-builtin-package.nix
 create mode 100644 pkgs/development/idris-modules/build-idris-package.nix

diff --git a/pkgs/development/idris-modules/build-builtin-package.nix b/pkgs/development/idris-modules/build-builtin-package.nix
new file mode 100644
index 00000000000..9a6b99d1523
--- /dev/null
+++ b/pkgs/development/idris-modules/build-builtin-package.nix
@@ -0,0 +1,12 @@
+{ idris, buildIdrisPackage }: name: deps: buildIdrisPackage (args: {
+  inherit name;
+
+  propagatedBuildInputs = deps;
+
+  inherit (idris) src;
+
+  postUnpack = ''
+    mv $sourceRoot/libs/${name} $IDRIS_LIBRARY_PATH
+    sourceRoot=$IDRIS_LIBRARY_PATH/${name}
+  '';
+})
diff --git a/pkgs/development/idris-modules/build-idris-package.nix b/pkgs/development/idris-modules/build-idris-package.nix
new file mode 100644
index 00000000000..eecd7d585cf
--- /dev/null
+++ b/pkgs/development/idris-modules/build-idris-package.nix
@@ -0,0 +1,34 @@
+{ stdenv, idris }: argf: let args = {
+  preHook = ''
+    mkdir idris-libs
+    export IDRIS_LIBRARY_PATH=$PWD/idris-libs
+
+    addIdrisLibs () {
+      if [ -d $1/lib/${idris.name} ]; then
+        ln -sv $1/lib/${idris.name}/* $IDRIS_LIBRARY_PATH
+      fi
+    }
+
+    envHooks+=(addIdrisLibs)
+  '';
+
+  configurePhase = ''
+    export TARGET=$out/lib/${idris.name}
+  '';
+
+  buildPhase = ''
+    ${idris}/bin/idris --build *.ipkg
+  '';
+
+  doCheck = true;
+
+  checkPhase = ''
+    if grep -q test *.ipkg; then
+      ${idris}/bin/idris --testpkg *.ipkg
+    fi
+  '';
+
+  installPhase = ''
+    ${idris}/bin/idris --install *.ipkg
+  '';
+}; in stdenv.mkDerivation (args // (argf args))
diff --git a/pkgs/development/idris-modules/default.nix b/pkgs/development/idris-modules/default.nix
index d07619724fe..96e8b5b8ad9 100644
--- a/pkgs/development/idris-modules/default.nix
+++ b/pkgs/development/idris-modules/default.nix
@@ -12,7 +12,27 @@
     defaultScope = mkScope self;
 
     callPackage = callPackageWithScope defaultScope;
+
+    buildBuiltinPackage = callPackage ./build-builtin-package.nix {};
+
+    builtins = pkgs.lib.mapAttrs buildBuiltinPackage {
+      prelude = [];
+
+      base = [ self.prelude ];
+
+      contrib = [ self.prelude self.base ];
+
+      effects = [ self.prelude self.base ];
+
+      pruviloj = [ self.prelude self.base ];
+    };
   in {
-    withPackages = packages: callPackage ./with-packages-wrapper.nix { inherit packages idris; };
-  };
+    inherit idris;
+
+    withPackages = callPackage ./with-packages-wrapper.nix {};
+
+    buildIdrisPackage = callPackage ./build-idris-package.nix {};
+
+    builtins = pkgs.lib.mapAttrsToList (name: value: value) builtins;
+  } // builtins;
 in fix' (extends overrides idrisPackages)
diff --git a/pkgs/development/idris-modules/with-packages-wrapper.nix b/pkgs/development/idris-modules/with-packages-wrapper.nix
index e55fd2c3324..f8abe09fe87 100644
--- a/pkgs/development/idris-modules/with-packages-wrapper.nix
+++ b/pkgs/development/idris-modules/with-packages-wrapper.nix
@@ -1,7 +1,19 @@
-{ stdenv, idris, packages }: stdenv.mkDerivation {
+{ stdenv, idris }: buildInputs: stdenv.mkDerivation {
   inherit (idris) name;
 
-  inherit packages;
+  inherit buildInputs;
+
+  preHook = ''
+    mkdir -p $out/lib/${idris.name}
+
+    installIdrisLib () {
+      if [ -d $1/lib/${idris.name} ]; then
+        ln -sv $1/lib/${idris.name}/* $out/lib/${idris.name}
+      fi
+    }
+
+    envHooks+=(installIdrisLib)
+  '';
 
   unpackPhase = ''
     cat >idris.c <<EOF
@@ -24,12 +36,6 @@
   '';
 
   installPhase = ''
-    mkdir -p $out/lib/${idris.name}
-    for package in $packages
-    do
-      ln -sv $package/lib/${idris.name}/* $out/lib/${idris.name}
-    done
-
     mkdir -p $out/bin
     mv idris $out/bin
   '';

From a5ca796f557f74e23328c8892447b0606d333f8d Mon Sep 17 00:00:00 2001
From: Shea Levy <shea@shealevy.com>
Date: Fri, 27 Nov 2015 09:55:22 -0500
Subject: [PATCH 4/8] idris-modules: Read the filesystem to populate package
 list

---
 .../idris-modules/build-builtin-package.nix    |  2 +-
 pkgs/development/idris-modules/default.nix     | 18 ++++++++----------
 ...-packages-wrapper.nix => with-packages.nix} |  0
 3 files changed, 9 insertions(+), 11 deletions(-)
 rename pkgs/development/idris-modules/{with-packages-wrapper.nix => with-packages.nix} (100%)

diff --git a/pkgs/development/idris-modules/build-builtin-package.nix b/pkgs/development/idris-modules/build-builtin-package.nix
index 9a6b99d1523..7445e95e27c 100644
--- a/pkgs/development/idris-modules/build-builtin-package.nix
+++ b/pkgs/development/idris-modules/build-builtin-package.nix
@@ -1,4 +1,4 @@
-{ idris, buildIdrisPackage }: name: deps: buildIdrisPackage (args: {
+{ idris, build-idris-package }: name: deps: build-idris-package (args: {
   inherit name;
 
   propagatedBuildInputs = deps;
diff --git a/pkgs/development/idris-modules/default.nix b/pkgs/development/idris-modules/default.nix
index 96e8b5b8ad9..8388eb96bbf 100644
--- a/pkgs/development/idris-modules/default.nix
+++ b/pkgs/development/idris-modules/default.nix
@@ -13,9 +13,7 @@
 
     callPackage = callPackageWithScope defaultScope;
 
-    buildBuiltinPackage = callPackage ./build-builtin-package.nix {};
-
-    builtins = pkgs.lib.mapAttrs buildBuiltinPackage {
+    builtins_ = pkgs.lib.mapAttrs self.build-builtin-package {
       prelude = [];
 
       base = [ self.prelude ];
@@ -26,13 +24,13 @@
 
       pruviloj = [ self.prelude self.base ];
     };
-  in {
-    inherit idris;
 
-    withPackages = callPackage ./with-packages-wrapper.nix {};
+    files = builtins.filter (n: n != null) (pkgs.lib.mapAttrsToList (name: type: let
+      m = builtins.match "(.*)\.nix" name;
+    in if m == null then null else builtins.head m) (builtins.readDir ./.));
+  in (builtins.listToAttrs (map (name: { inherit name; value = callPackage (./. + "/${name}.nix") {}; }) files)) // {
+    inherit idris callPackage;
 
-    buildIdrisPackage = callPackage ./build-idris-package.nix {};
-
-    builtins = pkgs.lib.mapAttrsToList (name: value: value) builtins;
-  } // builtins;
+    builtins = pkgs.lib.mapAttrsToList (name: value: value) builtins_;
+  } // builtins_;
 in fix' (extends overrides idrisPackages)
diff --git a/pkgs/development/idris-modules/with-packages-wrapper.nix b/pkgs/development/idris-modules/with-packages.nix
similarity index 100%
rename from pkgs/development/idris-modules/with-packages-wrapper.nix
rename to pkgs/development/idris-modules/with-packages.nix

From a01c7b5a1525d333c29a05e61bcb249c934ccbf6 Mon Sep 17 00:00:00 2001
From: Shea Levy <shea@shealevy.com>
Date: Fri, 27 Nov 2015 09:57:49 -0500
Subject: [PATCH 5/8] idris-modules: Filter out default.nix

---
 pkgs/development/idris-modules/default.nix | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/pkgs/development/idris-modules/default.nix b/pkgs/development/idris-modules/default.nix
index 8388eb96bbf..da879fa6cf4 100644
--- a/pkgs/development/idris-modules/default.nix
+++ b/pkgs/development/idris-modules/default.nix
@@ -25,9 +25,9 @@
       pruviloj = [ self.prelude self.base ];
     };
 
-    files = builtins.filter (n: n != null) (pkgs.lib.mapAttrsToList (name: type: let
+    files = builtins.filter (n: n != "default") (pkgs.lib.mapAttrsToList (name: type: let
       m = builtins.match "(.*)\.nix" name;
-    in if m == null then null else builtins.head m) (builtins.readDir ./.));
+    in if m == null then "default" else builtins.head m) (builtins.readDir ./.));
   in (builtins.listToAttrs (map (name: { inherit name; value = callPackage (./. + "/${name}.nix") {}; }) files)) // {
     inherit idris callPackage;
 

From 0dce60b34d8fefa02904debc9e6d427a6cb7d459 Mon Sep 17 00:00:00 2001
From: Shea Levy <shea@shealevy.com>
Date: Fri, 27 Nov 2015 11:03:04 -0500
Subject: [PATCH 6/8] Add wl-pprint Idris package.

---
 .../development/idris-modules/build-idris-package.nix |  4 +++-
 pkgs/development/idris-modules/wl-pprint.nix          | 11 +++++++++++
 2 files changed, 14 insertions(+), 1 deletion(-)
 create mode 100644 pkgs/development/idris-modules/wl-pprint.nix

diff --git a/pkgs/development/idris-modules/build-idris-package.nix b/pkgs/development/idris-modules/build-idris-package.nix
index eecd7d585cf..d3686b2a293 100644
--- a/pkgs/development/idris-modules/build-idris-package.nix
+++ b/pkgs/development/idris-modules/build-idris-package.nix
@@ -1,4 +1,4 @@
-{ stdenv, idris }: argf: let args = {
+{ stdenv, idris, gmp }: argf: let args = {
   preHook = ''
     mkdir idris-libs
     export IDRIS_LIBRARY_PATH=$PWD/idris-libs
@@ -31,4 +31,6 @@
   installPhase = ''
     ${idris}/bin/idris --install *.ipkg
   '';
+
+  buildInputs = [ gmp ];
 }; in stdenv.mkDerivation (args // (argf args))
diff --git a/pkgs/development/idris-modules/wl-pprint.nix b/pkgs/development/idris-modules/wl-pprint.nix
new file mode 100644
index 00000000000..dfde08fceab
--- /dev/null
+++ b/pkgs/development/idris-modules/wl-pprint.nix
@@ -0,0 +1,11 @@
+{ build-idris-package, fetchgit, prelude, base }: build-idris-package (args : {
+  name = "wl-pprint";
+
+  src = fetchgit {
+    url = "git://github.com/shayan-najd/wl-pprint.git";
+    rev = "120f654b0b9838b57e10b163d3562d959439fb07";
+    sha256 = "b5d02a9191973dd8915279e84a9b4df430eb252f429327f45eb8a047d8bb954d";
+  };
+
+  propagatedBuildInputs = [ prelude base ];
+})

From 0f90c9dbc1a42430883ab31853ba25e9d9ec26a5 Mon Sep 17 00:00:00 2001
From: Shea Levy <shea@shealevy.com>
Date: Fri, 27 Nov 2015 13:17:17 -0500
Subject: [PATCH 7/8] idris-modules: documentation

---
 .../idris-modules/build-builtin-package.nix   | 11 ++++++++--
 .../idris-modules/build-idris-package.nix     |  8 ++++++--
 pkgs/development/idris-modules/default.nix    |  7 ++++++-
 .../idris-modules/with-packages.nix           |  6 ++++--
 pkgs/development/idris-modules/wl-pprint.nix  | 20 +++++++++++++++++--
 pkgs/top-level/all-packages.nix               |  4 +++-
 6 files changed, 46 insertions(+), 10 deletions(-)

diff --git a/pkgs/development/idris-modules/build-builtin-package.nix b/pkgs/development/idris-modules/build-builtin-package.nix
index 7445e95e27c..95641a8f9fa 100644
--- a/pkgs/development/idris-modules/build-builtin-package.nix
+++ b/pkgs/development/idris-modules/build-builtin-package.nix
@@ -1,4 +1,7 @@
-{ idris, build-idris-package }: name: deps: build-idris-package (args: {
+# Build one of the packages that come with idris
+# name: The name of the package
+# deps: The dependencies of the package
+{ idris, build-idris-package, lib }: name: deps: build-idris-package {
   inherit name;
 
   propagatedBuildInputs = deps;
@@ -9,4 +12,8 @@
     mv $sourceRoot/libs/${name} $IDRIS_LIBRARY_PATH
     sourceRoot=$IDRIS_LIBRARY_PATH/${name}
   '';
-})
+
+  meta = idris.meta // {
+    description = "${name} builtin Idris library";
+  };
+}
diff --git a/pkgs/development/idris-modules/build-idris-package.nix b/pkgs/development/idris-modules/build-idris-package.nix
index d3686b2a293..a00f5e74b84 100644
--- a/pkgs/development/idris-modules/build-idris-package.nix
+++ b/pkgs/development/idris-modules/build-idris-package.nix
@@ -1,4 +1,8 @@
-{ stdenv, idris, gmp }: argf: let args = {
+# Build an idris package
+#
+# args: Additional arguments to pass to mkDerivation. Generally should include at least
+#       name and src.
+{ stdenv, idris, gmp }: args: stdenv.mkDerivation ({
   preHook = ''
     mkdir idris-libs
     export IDRIS_LIBRARY_PATH=$PWD/idris-libs
@@ -33,4 +37,4 @@
   '';
 
   buildInputs = [ gmp ];
-}; in stdenv.mkDerivation (args // (argf args))
+} // args)
diff --git a/pkgs/development/idris-modules/default.nix b/pkgs/development/idris-modules/default.nix
index da879fa6cf4..95ab68c5f42 100644
--- a/pkgs/development/idris-modules/default.nix
+++ b/pkgs/development/idris-modules/default.nix
@@ -28,9 +28,14 @@
     files = builtins.filter (n: n != "default") (pkgs.lib.mapAttrsToList (name: type: let
       m = builtins.match "(.*)\.nix" name;
     in if m == null then "default" else builtins.head m) (builtins.readDir ./.));
-  in (builtins.listToAttrs (map (name: { inherit name; value = callPackage (./. + "/${name}.nix") {}; }) files)) // {
+  in (builtins.listToAttrs (map (name: {
+    inherit name;
+
+    value = callPackage (./. + "/${name}.nix") {};
+  }) files)) // {
     inherit idris callPackage;
 
+    # A list of all of the libraries that come with idris
     builtins = pkgs.lib.mapAttrsToList (name: value: value) builtins_;
   } // builtins_;
 in fix' (extends overrides idrisPackages)
diff --git a/pkgs/development/idris-modules/with-packages.nix b/pkgs/development/idris-modules/with-packages.nix
index f8abe09fe87..edcd20c1097 100644
--- a/pkgs/development/idris-modules/with-packages.nix
+++ b/pkgs/development/idris-modules/with-packages.nix
@@ -1,7 +1,9 @@
-{ stdenv, idris }: buildInputs: stdenv.mkDerivation {
+# Build a version of idris with a set of packages visible
+# packages: The packages visible to idris
+{ stdenv, idris }: packages: stdenv.mkDerivation {
   inherit (idris) name;
 
-  inherit buildInputs;
+  buildInputs = packages;
 
   preHook = ''
     mkdir -p $out/lib/${idris.name}
diff --git a/pkgs/development/idris-modules/wl-pprint.nix b/pkgs/development/idris-modules/wl-pprint.nix
index dfde08fceab..2bf5ef79253 100644
--- a/pkgs/development/idris-modules/wl-pprint.nix
+++ b/pkgs/development/idris-modules/wl-pprint.nix
@@ -1,4 +1,10 @@
-{ build-idris-package, fetchgit, prelude, base }: build-idris-package (args : {
+{ build-idris-package
+, fetchgit
+, prelude
+, base
+, lib
+, idris
+}: build-idris-package {
   name = "wl-pprint";
 
   src = fetchgit {
@@ -8,4 +14,14 @@
   };
 
   propagatedBuildInputs = [ prelude base ];
-})
+
+  meta = {
+    description = "Wadler-Leijen pretty-printing library";
+
+    homepage = https://github.com/shayan-najd/wl-pprint;
+
+    license = lib.licenses.bsd2;
+
+    inherit (idris.meta) platforms;
+  };
+}
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index f482a74881c..1f647c712f2 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -4121,7 +4121,9 @@ let
 
   icedtea_web = icedtea8_web;
 
-  idrisPackages = callPackage ../development/idris-modules { inherit (haskellPackages) idris; };
+  idrisPackages = callPackage ../development/idris-modules {
+    inherit (haskellPackages) idris;
+  };
 
   ikarus = callPackage ../development/compilers/ikarus { };
 

From 9562549ff25033a8ef1ff3906079ec874bb5c67b Mon Sep 17 00:00:00 2001
From: Shea Levy <shea@shealevy.com>
Date: Fri, 27 Nov 2015 13:34:38 -0500
Subject: [PATCH 8/8] idris-modules: Add docs

---
 pkgs/development/idris-modules/README.md | 39 ++++++++++++++++++++++++
 pkgs/development/idris-modules/TODO.md   |  3 ++
 2 files changed, 42 insertions(+)
 create mode 100644 pkgs/development/idris-modules/README.md
 create mode 100644 pkgs/development/idris-modules/TODO.md

diff --git a/pkgs/development/idris-modules/README.md b/pkgs/development/idris-modules/README.md
new file mode 100644
index 00000000000..005ed360285
--- /dev/null
+++ b/pkgs/development/idris-modules/README.md
@@ -0,0 +1,39 @@
+Idris packages
+==============
+
+This directory contains build rules for idris packages. In addition,
+it contains several functions to build and compose those packages.
+Everything is exposed to the user via the `idrisPackages` attribute.
+
+callPackage
+------------
+
+This is like the normal nixpkgs callPackage function, specialized to
+idris packages.
+
+builtins
+---------
+
+This is a list of all of the libraries that come packaged with Idris
+itself.
+
+build-idris-package
+--------------------
+
+A function to build an idris package. Its sole argument is a set like
+you might pass to `stdenv.mkDerivation`, except `build-idris-package`
+sets several attributes for you. See `build-idris-package.nix` for
+details.
+
+build-builtin-package
+----------------------
+
+A version of `build-idris-package` specialized to builtin libraries.
+Mostly for internal use.
+
+with-packages
+-------------
+
+Bundle idris together with a list of packages. Because idris currently
+only supports a single directory in its library path, you must include
+all desired libraries here, including `prelude` and `base`.
\ No newline at end of file
diff --git a/pkgs/development/idris-modules/TODO.md b/pkgs/development/idris-modules/TODO.md
new file mode 100644
index 00000000000..4dcaa61829a
--- /dev/null
+++ b/pkgs/development/idris-modules/TODO.md
@@ -0,0 +1,3 @@
+* Build the RTS separately from Idris
+* idris2nix
+* Only require gmp, rts when compiling executables
\ No newline at end of file