diff --git a/lib/maintainers.nix b/lib/maintainers.nix
index 451cb4867a5..e2d3c73301b 100644
--- a/lib/maintainers.nix
+++ b/lib/maintainers.nix
@@ -328,6 +328,7 @@
   KibaFox = "Kiba Fox <kiba.fox@foxypossibilities.com>";
   kierdavis = "Kier Davis <kierdavis@gmail.com>";
   kiloreux = "Kiloreux Emperex <kiloreux@gmail.com>";
+  kini = "Keshav Kini <keshav.kini@gmail.com>";
   kkallio = "Karn Kallio <tierpluspluslists@gmail.com>";
   knedlsepp = "Josef Kemetmüller <josef.kemetmueller@gmail.com>";
   konimex = "Muhammad Herdiansyah <herdiansyah@netc.eu>";
diff --git a/pkgs/development/interpreters/acl2/default.nix b/pkgs/development/interpreters/acl2/default.nix
index f1e2315d794..16734c184eb 100644
--- a/pkgs/development/interpreters/acl2/default.nix
+++ b/pkgs/development/interpreters/acl2/default.nix
@@ -1,16 +1,26 @@
-{ stdenv, fetchurl, sbcl }:
+{ stdenv, fetchFromGitHub,
+  # perl, which, nettools,
+  sbcl }:
 
-stdenv.mkDerivation rec {
+let hashes = {
+  "7.4" = "04jb789nks9llwysxz1zw9pq1dh0j39b5fcmivcc4bq9v9cga2l1";
+};
+in stdenv.mkDerivation rec {
   name = "acl2-${version}";
-  version = "v6-5";
+  version = "7.4";
 
-  src = fetchurl {
-    url = "http://www.cs.utexas.edu/users/moore/acl2/${version}/distrib/acl2.tar.gz";
-    sha256 = "19kfclgpdyms016s06pjf3icj3mx9jlcj8vfgpbx2ac4ls0ir36g";
-    name = "acl2-${version}.tar.gz";
+  src = fetchFromGitHub {
+    owner = "acl2-devel";
+    repo = "acl2-devel";
+    rev = "${version}";
+    sha256 = hashes."${version}";
   };
 
-  buildInputs = [ sbcl ];
+  buildInputs = [ sbcl
+    # which perl nettools
+  ];
+
+  enableParallelBuilding = true;
 
   phases = "unpackPhase installPhase";
 
@@ -18,18 +28,45 @@ stdenv.mkDerivation rec {
 
   installPhase = ''
     mkdir -p $out/share/${installSuffix}
+    mkdir -p $out/bin
     cp -R . $out/share/${installSuffix}
     cd $out/share/${installSuffix}
-    make 'LISP=${sbcl}/bin/sbcl --dynamic-space-size 2000'
-    make 'LISP=${sbcl}/bin/sbcl --dynamic-space-size 2000' regression
-    make LISP=${sbcl}/bin/sbcl TAGS
-    mkdir -p $out/bin
+
+    # make ACL2 image
+    make LISP=${sbcl}/bin/sbcl
+
+    # The community books don't build properly under Nix yet.
+    rm -rf books
+    #make ACL2=$out/share/saved_acl2 USE_QUICKLISP=1 regression-everything
+
     cp saved_acl2 $out/bin/acl2
   '';
 
   meta = {
     description = "An interpreter and a prover for a Lisp dialect";
-    maintainers = with stdenv.lib.maintainers; [ raskin ];
+    longDescription = ''
+      ACL2 is a logic and programming language in which you can model
+      computer systems, together with a tool to help you prove
+      properties of those models. "ACL2" denotes "A Computational
+      Logic for Applicative Common Lisp".
+
+      ACL2 is part of the Boyer-Moore family of provers, for which its
+      authors have received the 2005 ACM Software System Award.
+
+      NOTE: In nixpkgs, the community books that usually ship with
+      ACL2 have been removed because it is not currently possible to
+      build them with Nix.
+    '';
+    homepage = http://www.cs.utexas.edu/users/moore/acl2/;
+    downloadPage = https://github.com/acl2-devel/acl2-devel/releases;
+    # There are a bunch of licenses in the community books, but since
+    # they currently get deleted during the build, we don't mention
+    # their licenses here.  ACL2 proper is released under a BSD
+    # 3-clause license.
+    #license = with stdenv.lib.licenses;
+    #[ free bsd3 mit gpl2 llgpl21 cc0 publicDomain ];
+    license = stdenv.lib.licenses.bsd3;
+    maintainers = with stdenv.lib.maintainers; [ kini raskin ];
     platforms = stdenv.lib.platforms.linux;
   };
 }
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 92974dd3d5d..bb573341d73 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -6362,9 +6362,7 @@ with pkgs;
 
   ### DEVELOPMENT / INTERPRETERS
 
-  acl2 = callPackage ../development/interpreters/acl2 {
-    sbcl = sbcl_1_2_0;
-  };
+  acl2 = callPackage ../development/interpreters/acl2 { };
 
   angelscript = callPackage ../development/interpreters/angelscript {};