Merge branch 'idris-packages'

8 files changed, 219 insertions, 0 deletions

diff --git a/pkgs/development/idris-modules/README.md b/pkgs/development/idris-modules/README.md
new file mode 100644
index 0000000000000..005ed3602851c
--- /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 0000000000000..4dcaa61829a81
--- /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
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 0000000000000..95641a8f9fa1c
--- /dev/null
+++ b/pkgs/development/idris-modules/build-builtin-package.nix
@@ -0,0 +1,19 @@
+# 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;
+
+  inherit (idris) src;
+
+  postUnpack = ''
+    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
new file mode 100644
index 0000000000000..a00f5e74b845b
--- /dev/null
+++ b/pkgs/development/idris-modules/build-idris-package.nix
@@ -0,0 +1,40 @@
+# 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
+
+    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
+  '';
+
+  buildInputs = [ gmp ];
+} // args)
diff --git a/pkgs/development/idris-modules/default.nix b/pkgs/development/idris-modules/default.nix
new file mode 100644
index 0000000000000..95ab68c5f42b4
--- /dev/null
+++ b/pkgs/development/idris-modules/default.nix
@@ -0,0 +1,41 @@
+{ 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;
+
+    builtins_ = pkgs.lib.mapAttrs self.build-builtin-package {
+      prelude = [];
+
+      base = [ self.prelude ];
+
+      contrib = [ self.prelude self.base ];
+
+      effects = [ self.prelude self.base ];
+
+      pruviloj = [ self.prelude self.base ];
+    };
+
+    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)) // {
+    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
new file mode 100644
index 0000000000000..edcd20c10978e
--- /dev/null
+++ b/pkgs/development/idris-modules/with-packages.nix
@@ -0,0 +1,46 @@
+# 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;
+
+  buildInputs = packages;
+
+  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
+    #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/bin
+    mv idris $out/bin
+  '';
+
+  stripAllList = [ "bin" ];
+}
diff --git a/pkgs/development/idris-modules/wl-pprint.nix b/pkgs/development/idris-modules/wl-pprint.nix
new file mode 100644
index 0000000000000..2bf5ef79253c2
--- /dev/null
+++ b/pkgs/development/idris-modules/wl-pprint.nix
@@ -0,0 +1,27 @@
+{ build-idris-package
+, fetchgit
+, prelude
+, base
+, lib
+, idris
+}: build-idris-package {
+  name = "wl-pprint";
+
+  src = fetchgit {
+    url = "git://github.com/shayan-najd/wl-pprint.git";
+    rev = "120f654b0b9838b57e10b163d3562d959439fb07";
+    sha256 = "b5d02a9191973dd8915279e84a9b4df430eb252f429327f45eb8a047d8bb954d";
+  };
+
+  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 760f3309be34c..1f647c712f2bb 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -4121,6 +4121,10 @@ let
 
   icedtea_web = icedtea8_web;
 
+  idrisPackages = callPackage ../development/idris-modules {
+    inherit (haskellPackages) idris;
+  };
+
   ikarus = callPackage ../development/compilers/ikarus { };
 
   intercal = callPackage ../development/compilers/intercal { };