diff --git a/pkgs/development/compilers/agda/agda.nix b/pkgs/development/compilers/agda/2.3.2.2.nix
similarity index 100%
rename from pkgs/development/compilers/agda/agda.nix
rename to pkgs/development/compilers/agda/2.3.2.2.nix
diff --git a/pkgs/development/compilers/agda/2.4.0.1.nix b/pkgs/development/compilers/agda/2.4.0.1.nix
new file mode 100644
index 00000000000..e472eb1c276
--- /dev/null
+++ b/pkgs/development/compilers/agda/2.4.0.1.nix
@@ -0,0 +1,30 @@
+{ cabal, alex, binary, boxes, dataHash, deepseq, emacs, equivalence
+, filepath, geniplate, happy, hashable, hashtables, haskeline
+, haskellSrcExts, mtl, parallel, QuickCheck, STMonadTrans, strict
+, text, time, transformers, unorderedContainers, xhtml, zlib
+}:
+
+cabal.mkDerivation (self: {
+  pname = "Agda";
+  version = "2.4.0.1";
+  sha256 = "11my5k606zvra3w3m1wllc4dy5mfv4lr32fqd579vqcks6wpirjq";
+  isLibrary = true;
+  isExecutable = true;
+  buildDepends = [
+    binary boxes dataHash deepseq equivalence filepath geniplate
+    hashable hashtables haskeline haskellSrcExts mtl parallel
+    QuickCheck STMonadTrans strict text time transformers
+    unorderedContainers xhtml zlib
+  ];
+  buildTools = [ alex emacs happy ];
+  postInstall = ''
+    $out/bin/agda -c --no-main $(find $out/share -name Primitive.agda)
+    $out/bin/agda-mode compile
+  '';
+  meta = {
+    homepage = "http://wiki.portal.chalmers.se/agda/";
+    description = "A dependently typed functional programming language and proof assistant";
+    license = "unknown";
+    platforms = self.ghc.meta.platforms;
+  };
+})
diff --git a/pkgs/development/compilers/agda/stdlib.nix b/pkgs/development/compilers/agda/stdlib-0.7.nix
similarity index 100%
rename from pkgs/development/compilers/agda/stdlib.nix
rename to pkgs/development/compilers/agda/stdlib-0.7.nix
diff --git a/pkgs/development/compilers/agda/stdlib-2.4.0.nix b/pkgs/development/compilers/agda/stdlib-2.4.0.nix
new file mode 100644
index 00000000000..faa55d379b1
--- /dev/null
+++ b/pkgs/development/compilers/agda/stdlib-2.4.0.nix
@@ -0,0 +1,32 @@
+{ cabal, fetchurl, filemanip, Agda }:
+
+cabal.mkDerivation (self: {
+  pname = "Agda-lib-ffi";
+  version = "2.4.0";
+
+  src = fetchurl {
+    url = "https://github.com/agda/agda-stdlib/archive/v2.4.0.tar.gz";
+    sha256 = "1rz0jrkm1b8d8aj9hbj3yl2k219c57r0cizfx98qqf1b9mwixzbf";
+  };
+
+  buildDepends = [ filemanip Agda ];
+  jailbreak = true;             # otherwise, it complains about base
+
+  preConfigure = "cd ffi";
+
+  postInstall = ''
+      mkdir -p $out/share
+      cd ..
+      runhaskell GenerateEverything
+      ${Agda}/bin/agda -i . -i src Everything.agda
+      cp -pR src $out/share/agda
+  '';
+
+  meta = {
+    homepage = "http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary";
+    description = "A standard library for use with the Agda compiler.";
+    license = "unknown";
+    platforms = self.ghc.meta.platforms;
+    maintainers = [ self.stdenv.lib.maintainers.jwiegley ];
+  };
+})
\ No newline at end of file
diff --git a/pkgs/top-level/haskell-packages.nix b/pkgs/top-level/haskell-packages.nix
index 09745e5c8df..f2334b9e6a8 100644
--- a/pkgs/top-level/haskell-packages.nix
+++ b/pkgs/top-level/haskell-packages.nix
@@ -2600,8 +2600,17 @@ self : let callPackage = x : y : modifyPrio (newScope self x y); in
 
   # Compilers.
 
-  Agda = callPackage ../development/compilers/agda/agda.nix { QuickCheck = self.QuickCheck_2_6; };
-  AgdaStdlib = callPackage ../development/compilers/agda/stdlib.nix {};
+  Agda_2_3_2_2 = callPackage ../development/compilers/agda/2.3.2.2.nix {};
+  Agda_2_4_0_1 = callPackage ../development/compilers/agda/2.4.0.1.nix {};
+  Agda = self.Agda_2_3_2_2;
+
+  AgdaStdlib_0_7 = callPackage ../development/compilers/agda/stdlib-0.7.nix {
+    Agda = self.Agda_2_3_2_2;
+  };
+  AgdaStdlib_2_4_0 = callPackage ../development/compilers/agda/stdlib-2.4.0.nix {
+    Agda = self.Agda_2_4_0_1;
+  };
+  AgdaStdlib = self.AgdaStdlib_0_7;
 
   uhc = callPackage ../development/compilers/uhc {};