diff options
Diffstat (limited to 'nixpkgs/pkgs/development/interpreters/acl2/default.nix')
| -rw-r--r-- | nixpkgs/pkgs/development/interpreters/acl2/default.nix | 159 |
1 files changed, 109 insertions, 50 deletions
diff --git a/nixpkgs/pkgs/development/interpreters/acl2/default.nix b/nixpkgs/pkgs/development/interpreters/acl2/default.nix index 39b243a0ce6..e3c62aae983 100644 --- a/nixpkgs/pkgs/development/interpreters/acl2/default.nix +++ b/nixpkgs/pkgs/development/interpreters/acl2/default.nix @@ -1,15 +1,19 @@ -{ stdenv, fetchFromGitHub, - # perl, which, nettools, - sbcl }: - -let hashes = { - "8.0" = "1x1giy2c1y6krg3kf8pf9wrmvk981shv0pxcwi483yjqm90xng4r"; - "8.3" = "0c0wimaf16nrr3d6cxq6p7nr7rxffvpmn66hkpwc1m6zpcipf0y5"; -}; -revs = { - "8.0" = "8.0"; - "8.3" = "8.3"; -}; +{ 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 + # http://www.cs.utexas.edu/users/moore/acl2/current/HTML/installation/requirements.html#Obtaining-SBCL + 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 "$@"''; + in stdenv.mkDerivation rec { pname = "acl2"; version = "8.3"; @@ -17,62 +21,117 @@ in stdenv.mkDerivation rec { src = fetchFromGitHub { owner = "acl2-devel"; repo = "acl2-devel"; - rev = revs.${version}; - sha256 = hashes.${version}; + rev = "${version}"; + sha256 = "0c0wimaf16nrr3d6cxq6p7nr7rxffvpmn66hkpwc1m6zpcipf0y5"; }; - buildInputs = [ sbcl - # which perl nettools + 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 ]; + 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. enableParallelBuilding = true; - phases = "unpackPhase installPhase"; + 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 + ''; - installSuffix = "acl2"; + 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"; installPhase = '' - mkdir -p $out/share/${installSuffix} mkdir -p $out/bin - cp -R . $out/share/${installSuffix} - cd $out/share/${installSuffix} + 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 + ''; - # make ACL2 image - make LISP=${sbcl}/bin/sbcl + preDistPhases = [ (if certifyBooks then "certifyBooksPhase" else "removeBooksPhase") ]; - # The community books don't build properly under Nix yet. - rm -rf books - #make ACL2=$out/share/saved_acl2 USE_QUICKLISP=1 regression-everything + certifyBooksPhase = '' + # Certify the community books + pushd $out/share/${pname}/books + makeFlags="ACL2=$out/share/${pname}/saved_acl2" + buildFlags="everything" + buildPhase + popd + ''; - cp saved_acl2 $out/bin/acl2 + removeBooksPhase = '' + # Delete the community books + rm -rf $out/share/${pname}/books ''; - meta = { + meta = with stdenv.lib; { description = "An interpreter and a prover for a Lisp dialect"; 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. - ''; + 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. + ''); 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.all; - broken = stdenv.isAarch64 && stdenv.isLinux; + 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; }; } |