diff --git a/pkgs/development/interpreters/acl2/default.nix b/pkgs/development/interpreters/acl2/default.nix
new file mode 100644
index 000000000000..959cd50aae6e
--- /dev/null
+++ b/pkgs/development/interpreters/acl2/default.nix
@@ -0,0 +1,41 @@
+a :  
+let 
+  fetchurl = a.fetchurl;
+
+  version = a.lib.attrByPath ["version"] "v3-5" a; 
+  buildInputs = with a; [
+    sbcl
+  ];
+in
+rec {
+  src = fetchurl {
+    url = "http://www.cs.utexas.edu/users/moore/acl2/${version}/distrib/acl2.tar.gz";
+    sha256 = "0zmh1njpp7n7azcyjlygr0h0k51d18s1jkj0dr1jn2bh7mpysajk";
+    name = "acl2-${version}.tar.gz";
+  };
+
+  inherit buildInputs;
+  configureFlags = [];
+
+  /* doConfigure should be removed if not needed */
+  phaseNames = ["doDeploy" "doBuild"];
+  
+  makeFlags = ["LISP='${a.sbcl}/bin/sbcl'"];
+
+  installSuffix = "acl2";
+  doDeploy = (a.simplyShare installSuffix);
+  doBuild = a.fullDepEntry (''
+    cd $out/share/${installSuffix}
+    make LISP=${a.sbcl}/bin/sbcl
+    make LISP=${a.sbcl}/bin/sbcl regression
+    ensureDir "$out/bin"
+    cp saved_acl2 "$out/bin/acl2"
+  '') ["doDeploy" "addInputs" "defEnsureDir"];
+      
+  name = "acl2-" + version;
+  meta = {
+    description = "An interpreter and a prover for a Lisp dialect";
+    maintainers = [
+    ];
+  };
+}
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 6440084767ad..e2368f04fb86 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -2074,6 +2074,9 @@ let
 
   ### DEVELOPMENT / INTERPRETERS
 
+  acl2 = builderDefsPackage ../development/interpreters/acl2 {
+    inherit sbcl;
+  };
 
   clisp = import ../development/interpreters/clisp {
     inherit fetchurl stdenv libsigsegv gettext