acl2, acl2-minimal: build standard library, init
Before this commit, we only built the main ACL2 executable. Most users
will also want the standard library (the "Community Books"), so after
this commit, we build the entire `make everything` suite, which includes
essentially everything provided in the ACL2 repository.
There's also a new top-level package called `acl2-minimal` which has
just the core ACL2 executable, for those who really only want that.
Future work: modularize the build so that we can support multiple
different subsets of the standard library. A lot of the stuff in this
complete build is probably superfluous to almost all users. Also,
because some of the books have unclear or idiosyncratic licenses, the
full build will not be cached on cache.nixos.org, and installing it will
mean spending a few hours building it. So it would be good to have a
pared down build which excluded non-free books and things that people
rarely or never use.
2020-02-24 05:12:37 +00:00
|
|
|
{ stdenv, callPackage, fetchFromGitHub, writeShellScriptBin, substituteAll
|
|
|
|
|
, sbcl, bash, which, perl, nettools
|
|
|
|
|
, openssl, glucose, minisat, abc-verifier, z3, python2
|
|
|
|
|
, certifyBooks ? true
|
|
|
|
|
} @ args:
|
|
|
|
|
|
|
|
|
|
let
|
|
|
|
|
# Disable immobile space so we don't run out of memory on large books; see
|
2020-10-02 08:58:50 +01:00
|
|
|
# https://www.cs.utexas.edu/users/moore/acl2/current/HTML/installation/requirements.html#Obtaining-SBCL
|
acl2, acl2-minimal: build standard library, init
Before this commit, we only built the main ACL2 executable. Most users
will also want the standard library (the "Community Books"), so after
this commit, we build the entire `make everything` suite, which includes
essentially everything provided in the ACL2 repository.
There's also a new top-level package called `acl2-minimal` which has
just the core ACL2 executable, for those who really only want that.
Future work: modularize the build so that we can support multiple
different subsets of the standard library. A lot of the stuff in this
complete build is probably superfluous to almost all users. Also,
because some of the books have unclear or idiosyncratic licenses, the
full build will not be cached on cache.nixos.org, and installing it will
mean spending a few hours building it. So it would be good to have a
pared down build which excluded non-free books and things that people
rarely or never use.
2020-02-24 05:12:37 +00:00
|
|
|
sbcl = args.sbcl.override { disableImmobileSpace = true; };
|
|
|
|
|
|
|
|
|
|
# Wrap to add `-model` argument because some of the books in 8.3 need this.
|
|
|
|
|
# Fixed upstream (https://github.com/acl2/acl2/commit/0359538a), so this can
|
|
|
|
|
# be removed in ACL2 8.4.
|
|
|
|
|
glucose = writeShellScriptBin "glucose" ''exec ${args.glucose}/bin/glucose -model "$@"'';
|
|
|
|
|
|
2017-11-04 17:45:34 +00:00
|
|
|
in stdenv.mkDerivation rec {
|
2019-08-15 13:41:18 +01:00
|
|
|
pname = "acl2";
|
2020-04-23 00:47:27 +01:00
|
|
|
version = "8.3";
|
2009-08-13 15:32:52 +01:00
|
|
|
|
2017-11-04 17:45:34 +00:00
|
|
|
src = fetchFromGitHub {
|
|
|
|
|
owner = "acl2-devel";
|
|
|
|
|
repo = "acl2-devel";
|
2020-11-01 22:39:49 +00:00
|
|
|
rev = version;
|
acl2, acl2-minimal: build standard library, init
Before this commit, we only built the main ACL2 executable. Most users
will also want the standard library (the "Community Books"), so after
this commit, we build the entire `make everything` suite, which includes
essentially everything provided in the ACL2 repository.
There's also a new top-level package called `acl2-minimal` which has
just the core ACL2 executable, for those who really only want that.
Future work: modularize the build so that we can support multiple
different subsets of the standard library. A lot of the stuff in this
complete build is probably superfluous to almost all users. Also,
because some of the books have unclear or idiosyncratic licenses, the
full build will not be cached on cache.nixos.org, and installing it will
mean spending a few hours building it. So it would be good to have a
pared down build which excluded non-free books and things that people
rarely or never use.
2020-02-24 05:12:37 +00:00
|
|
|
sha256 = "0c0wimaf16nrr3d6cxq6p7nr7rxffvpmn66hkpwc1m6zpcipf0y5";
|
2009-08-13 15:32:52 +01:00
|
|
|
};
|
|
|
|
|
|
acl2, acl2-minimal: build standard library, init
Before this commit, we only built the main ACL2 executable. Most users
will also want the standard library (the "Community Books"), so after
this commit, we build the entire `make everything` suite, which includes
essentially everything provided in the ACL2 repository.
There's also a new top-level package called `acl2-minimal` which has
just the core ACL2 executable, for those who really only want that.
Future work: modularize the build so that we can support multiple
different subsets of the standard library. A lot of the stuff in this
complete build is probably superfluous to almost all users. Also,
because some of the books have unclear or idiosyncratic licenses, the
full build will not be cached on cache.nixos.org, and installing it will
mean spending a few hours building it. So it would be good to have a
pared down build which excluded non-free books and things that people
rarely or never use.
2020-02-24 05:12:37 +00:00
|
|
|
libipasirglucose4 = callPackage ./libipasirglucose4 { };
|
|
|
|
|
|
|
|
|
|
patches = [
|
|
|
|
|
(substituteAll {
|
|
|
|
|
src = ./0001-Fix-some-paths-for-Nix-build.patch;
|
|
|
|
|
inherit bash libipasirglucose4;
|
|
|
|
|
openssl = openssl.out;
|
|
|
|
|
})
|
|
|
|
|
./0002-Restrict-RDTSC-to-x86.patch
|
2017-11-04 17:45:34 +00:00
|
|
|
];
|
|
|
|
|
|
acl2, acl2-minimal: build standard library, init
Before this commit, we only built the main ACL2 executable. Most users
will also want the standard library (the "Community Books"), so after
this commit, we build the entire `make everything` suite, which includes
essentially everything provided in the ACL2 repository.
There's also a new top-level package called `acl2-minimal` which has
just the core ACL2 executable, for those who really only want that.
Future work: modularize the build so that we can support multiple
different subsets of the standard library. A lot of the stuff in this
complete build is probably superfluous to almost all users. Also,
because some of the books have unclear or idiosyncratic licenses, the
full build will not be cached on cache.nixos.org, and installing it will
mean spending a few hours building it. So it would be good to have a
pared down build which excluded non-free books and things that people
rarely or never use.
2020-02-24 05:12:37 +00:00
|
|
|
buildInputs = [
|
|
|
|
|
# ACL2 itself only needs a Common Lisp compiler/interpreter:
|
|
|
|
|
sbcl
|
|
|
|
|
] ++ stdenv.lib.optionals certifyBooks [
|
|
|
|
|
# To build community books, we need Perl and a couple of utilities:
|
|
|
|
|
which perl nettools
|
|
|
|
|
# Some of the books require one or more of these external tools:
|
|
|
|
|
openssl.out glucose minisat abc-verifier libipasirglucose4
|
|
|
|
|
z3 (python2.withPackages (ps: [ ps.z3 ]))
|
|
|
|
|
];
|
|
|
|
|
|
|
|
|
|
# NOTE: Parallel building can be memory-intensive depending on the number of
|
|
|
|
|
# concurrent jobs. For example, this build has been seen to use >120GB of
|
|
|
|
|
# RAM on an 85 core machine.
|
2017-11-04 17:45:34 +00:00
|
|
|
enableParallelBuilding = true;
|
2009-08-13 15:32:52 +01:00
|
|
|
|
acl2, acl2-minimal: build standard library, init
Before this commit, we only built the main ACL2 executable. Most users
will also want the standard library (the "Community Books"), so after
this commit, we build the entire `make everything` suite, which includes
essentially everything provided in the ACL2 repository.
There's also a new top-level package called `acl2-minimal` which has
just the core ACL2 executable, for those who really only want that.
Future work: modularize the build so that we can support multiple
different subsets of the standard library. A lot of the stuff in this
complete build is probably superfluous to almost all users. Also,
because some of the books have unclear or idiosyncratic licenses, the
full build will not be cached on cache.nixos.org, and installing it will
mean spending a few hours building it. So it would be good to have a
pared down build which excluded non-free books and things that people
rarely or never use.
2020-02-24 05:12:37 +00:00
|
|
|
preConfigure = ''
|
|
|
|
|
# When certifying books, ACL2 doesn't like $HOME not existing.
|
|
|
|
|
export HOME=$(pwd)/fake-home
|
|
|
|
|
'' + stdenv.lib.optionalString certifyBooks ''
|
|
|
|
|
# Some books also care about $USER being nonempty.
|
|
|
|
|
export USER=nobody
|
|
|
|
|
'';
|
2009-08-13 15:32:52 +01:00
|
|
|
|
acl2, acl2-minimal: build standard library, init
Before this commit, we only built the main ACL2 executable. Most users
will also want the standard library (the "Community Books"), so after
this commit, we build the entire `make everything` suite, which includes
essentially everything provided in the ACL2 repository.
There's also a new top-level package called `acl2-minimal` which has
just the core ACL2 executable, for those who really only want that.
Future work: modularize the build so that we can support multiple
different subsets of the standard library. A lot of the stuff in this
complete build is probably superfluous to almost all users. Also,
because some of the books have unclear or idiosyncratic licenses, the
full build will not be cached on cache.nixos.org, and installing it will
mean spending a few hours building it. So it would be good to have a
pared down build which excluded non-free books and things that people
rarely or never use.
2020-02-24 05:12:37 +00:00
|
|
|
postConfigure = ''
|
|
|
|
|
# ACL2 and its books need to be built in place in the out directory because
|
|
|
|
|
# the proof artifacts are not relocatable. Since ACL2 mostly expects
|
|
|
|
|
# everything to exist in the original source tree layout, we put it in
|
|
|
|
|
# $out/share/${pname} and create symlinks in $out/bin as necessary.
|
|
|
|
|
mkdir -p $out/share/${pname}
|
|
|
|
|
cp -pR . $out/share/${pname}
|
|
|
|
|
cd $out/share/${pname}
|
|
|
|
|
'';
|
|
|
|
|
|
|
|
|
|
preBuild = "mkdir -p $HOME";
|
|
|
|
|
makeFlags="LISP=${sbcl}/bin/sbcl";
|
|
|
|
|
|
|
|
|
|
doCheck = true;
|
|
|
|
|
checkTarget = "mini-proveall";
|
2016-01-24 12:49:33 +00:00
|
|
|
|
|
|
|
|
installPhase = ''
|
2017-11-04 17:45:34 +00:00
|
|
|
mkdir -p $out/bin
|
acl2, acl2-minimal: build standard library, init
Before this commit, we only built the main ACL2 executable. Most users
will also want the standard library (the "Community Books"), so after
this commit, we build the entire `make everything` suite, which includes
essentially everything provided in the ACL2 repository.
There's also a new top-level package called `acl2-minimal` which has
just the core ACL2 executable, for those who really only want that.
Future work: modularize the build so that we can support multiple
different subsets of the standard library. A lot of the stuff in this
complete build is probably superfluous to almost all users. Also,
because some of the books have unclear or idiosyncratic licenses, the
full build will not be cached on cache.nixos.org, and installing it will
mean spending a few hours building it. So it would be good to have a
pared down build which excluded non-free books and things that people
rarely or never use.
2020-02-24 05:12:37 +00:00
|
|
|
ln -s $out/share/${pname}/saved_acl2 $out/bin/${pname}
|
|
|
|
|
'' + stdenv.lib.optionalString certifyBooks ''
|
|
|
|
|
ln -s $out/share/${pname}/books/build/cert.pl $out/bin/${pname}-cert
|
|
|
|
|
ln -s $out/share/${pname}/books/build/clean.pl $out/bin/${pname}-clean
|
|
|
|
|
'';
|
2017-11-04 17:45:34 +00:00
|
|
|
|
acl2, acl2-minimal: build standard library, init
Before this commit, we only built the main ACL2 executable. Most users
will also want the standard library (the "Community Books"), so after
this commit, we build the entire `make everything` suite, which includes
essentially everything provided in the ACL2 repository.
There's also a new top-level package called `acl2-minimal` which has
just the core ACL2 executable, for those who really only want that.
Future work: modularize the build so that we can support multiple
different subsets of the standard library. A lot of the stuff in this
complete build is probably superfluous to almost all users. Also,
because some of the books have unclear or idiosyncratic licenses, the
full build will not be cached on cache.nixos.org, and installing it will
mean spending a few hours building it. So it would be good to have a
pared down build which excluded non-free books and things that people
rarely or never use.
2020-02-24 05:12:37 +00:00
|
|
|
preDistPhases = [ (if certifyBooks then "certifyBooksPhase" else "removeBooksPhase") ];
|
2017-11-04 17:45:34 +00:00
|
|
|
|
acl2, acl2-minimal: build standard library, init
Before this commit, we only built the main ACL2 executable. Most users
will also want the standard library (the "Community Books"), so after
this commit, we build the entire `make everything` suite, which includes
essentially everything provided in the ACL2 repository.
There's also a new top-level package called `acl2-minimal` which has
just the core ACL2 executable, for those who really only want that.
Future work: modularize the build so that we can support multiple
different subsets of the standard library. A lot of the stuff in this
complete build is probably superfluous to almost all users. Also,
because some of the books have unclear or idiosyncratic licenses, the
full build will not be cached on cache.nixos.org, and installing it will
mean spending a few hours building it. So it would be good to have a
pared down build which excluded non-free books and things that people
rarely or never use.
2020-02-24 05:12:37 +00:00
|
|
|
certifyBooksPhase = ''
|
|
|
|
|
# Certify the community books
|
|
|
|
|
pushd $out/share/${pname}/books
|
|
|
|
|
makeFlags="ACL2=$out/share/${pname}/saved_acl2"
|
|
|
|
|
buildFlags="everything"
|
|
|
|
|
buildPhase
|
|
|
|
|
popd
|
|
|
|
|
'';
|
2017-11-04 17:45:34 +00:00
|
|
|
|
acl2, acl2-minimal: build standard library, init
Before this commit, we only built the main ACL2 executable. Most users
will also want the standard library (the "Community Books"), so after
this commit, we build the entire `make everything` suite, which includes
essentially everything provided in the ACL2 repository.
There's also a new top-level package called `acl2-minimal` which has
just the core ACL2 executable, for those who really only want that.
Future work: modularize the build so that we can support multiple
different subsets of the standard library. A lot of the stuff in this
complete build is probably superfluous to almost all users. Also,
because some of the books have unclear or idiosyncratic licenses, the
full build will not be cached on cache.nixos.org, and installing it will
mean spending a few hours building it. So it would be good to have a
pared down build which excluded non-free books and things that people
rarely or never use.
2020-02-24 05:12:37 +00:00
|
|
|
removeBooksPhase = ''
|
|
|
|
|
# Delete the community books
|
|
|
|
|
rm -rf $out/share/${pname}/books
|
2016-01-24 12:49:33 +00:00
|
|
|
'';
|
|
|
|
|
|
acl2, acl2-minimal: build standard library, init
Before this commit, we only built the main ACL2 executable. Most users
will also want the standard library (the "Community Books"), so after
this commit, we build the entire `make everything` suite, which includes
essentially everything provided in the ACL2 repository.
There's also a new top-level package called `acl2-minimal` which has
just the core ACL2 executable, for those who really only want that.
Future work: modularize the build so that we can support multiple
different subsets of the standard library. A lot of the stuff in this
complete build is probably superfluous to almost all users. Also,
because some of the books have unclear or idiosyncratic licenses, the
full build will not be cached on cache.nixos.org, and installing it will
mean spending a few hours building it. So it would be good to have a
pared down build which excluded non-free books and things that people
rarely or never use.
2020-02-24 05:12:37 +00:00
|
|
|
meta = with stdenv.lib; {
|
2009-08-13 15:32:52 +01:00
|
|
|
description = "An interpreter and a prover for a Lisp dialect";
|
2017-11-04 17:45:34 +00:00
|
|
|
longDescription = ''
|
acl2, acl2-minimal: build standard library, init
Before this commit, we only built the main ACL2 executable. Most users
will also want the standard library (the "Community Books"), so after
this commit, we build the entire `make everything` suite, which includes
essentially everything provided in the ACL2 repository.
There's also a new top-level package called `acl2-minimal` which has
just the core ACL2 executable, for those who really only want that.
Future work: modularize the build so that we can support multiple
different subsets of the standard library. A lot of the stuff in this
complete build is probably superfluous to almost all users. Also,
because some of the books have unclear or idiosyncratic licenses, the
full build will not be cached on cache.nixos.org, and installing it will
mean spending a few hours building it. So it would be good to have a
pared down build which excluded non-free books and things that people
rarely or never use.
2020-02-24 05:12:37 +00:00
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
This package installs the main ACL2 executable ${pname}, as well as the
|
|
|
|
|
build tools cert.pl and clean.pl, renamed to ${pname}-cert and
|
|
|
|
|
${pname}-clean.
|
|
|
|
|
|
|
|
|
|
'' + (if certifyBooks then ''
|
|
|
|
|
The community books are also included and certified with the `make
|
|
|
|
|
everything` target.
|
|
|
|
|
'' else ''
|
|
|
|
|
The community books are not included in this package.
|
|
|
|
|
'');
|
2020-10-02 08:58:50 +01:00
|
|
|
homepage = "https://www.cs.utexas.edu/users/moore/acl2/";
|
2020-04-01 02:11:51 +01:00
|
|
|
downloadPage = "https://github.com/acl2-devel/acl2-devel/releases";
|
acl2, acl2-minimal: build standard library, init
Before this commit, we only built the main ACL2 executable. Most users
will also want the standard library (the "Community Books"), so after
this commit, we build the entire `make everything` suite, which includes
essentially everything provided in the ACL2 repository.
There's also a new top-level package called `acl2-minimal` which has
just the core ACL2 executable, for those who really only want that.
Future work: modularize the build so that we can support multiple
different subsets of the standard library. A lot of the stuff in this
complete build is probably superfluous to almost all users. Also,
because some of the books have unclear or idiosyncratic licenses, the
full build will not be cached on cache.nixos.org, and installing it will
mean spending a few hours building it. So it would be good to have a
pared down build which excluded non-free books and things that people
rarely or never use.
2020-02-24 05:12:37 +00:00
|
|
|
license = with licenses; [
|
|
|
|
|
# ACL2 itself is bsd3
|
|
|
|
|
bsd3
|
|
|
|
|
] ++ optionals certifyBooks [
|
|
|
|
|
# The community books are mostly bsd3 or mit but with a few
|
|
|
|
|
# other things thrown in.
|
|
|
|
|
mit gpl2 llgpl21 cc0 publicDomain unfreeRedistributable
|
|
|
|
|
];
|
|
|
|
|
maintainers = with maintainers; [ kini raskin ];
|
|
|
|
|
platforms = platforms.all;
|
2009-08-13 15:32:52 +01:00
|
|
|
};
|
|
|
|
|
}
|
