Adding ACL2.

ACL2 = A Computational Logic for Applicative Common Lisp. It is 
a Lisp sublanguage and a correctness prover for it.

svn path=/nixpkgs/trunk/; revision=16708
This commit is contained in:
Michael Raskin 2009-08-13 14:32:52 +00:00
parent 8703ea4070
commit 7ffff9d558
2 changed files with 44 additions and 0 deletions

View File

@ -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 = [
];
};
}

View File

@ -2074,6 +2074,9 @@ let
### DEVELOPMENT / INTERPRETERS
acl2 = builderDefsPackage ../development/interpreters/acl2 {
inherit sbcl;
};
clisp = import ../development/interpreters/clisp {
inherit fetchurl stdenv libsigsegv gettext