tjh.dev
Clone of https://github.com/NixOS/nixpkgs.git (to stress-test knotserver)
1{ lib, stdenv, callPackage, fetchFromGitHub, runCommandLocal, makeWrapper, substituteAll
2, sbcl, bash, which, perl, hostname
3, openssl, glucose, minisat, abc-verifier, z3, python3
4, certifyBooks ? true
5} @ args:
6
7let
8 # Disable immobile space so we don't run out of memory on large books, and
9 # supply 2GB of dynamic space to avoid exhausting the heap while building the
10 # ACL2 system itself; see
11 # https://www.cs.utexas.edu/users/moore/acl2/current/HTML/installation/requirements.html#Obtaining-SBCL
12 sbcl' = args.sbcl.overrideAttrs { disableImmobileSpace = true; };
13 sbcl = runCommandLocal args.sbcl.name { nativeBuildInputs = [ makeWrapper ]; } ''
14 makeWrapper ${sbcl'}/bin/sbcl $out/bin/sbcl \
15 --add-flags "--dynamic-space-size 2000"
16 '';
17
18in stdenv.mkDerivation rec {
19 pname = "acl2";
20 version = "8.5";
21
22 src = fetchFromGitHub {
23 owner = "acl2-devel";
24 repo = "acl2-devel";
25 rev = version;
26 sha256 = "12cv5ms1j3vfrq066km020nwxb6x2dzh12g8nz6xxyxysn44wzzi";
27 };
28
29 # You can swap this out with any other IPASIR implementation at
30 # build time by using overrideAttrs (make sure the derivation you
31 # use has a "libname" attribute so we can plug it into the patch
32 # below). Or, you can override it at runtime by setting the
33 # $IPASIR_SHARED_LIBRARY environment variable.
34 libipasir = callPackage ./libipasirglucose4 { };
35
36 patches = [(substituteAll {
37 src = ./0001-Fix-some-paths-for-Nix-build.patch;
38 libipasir = "${libipasir}/lib/${libipasir.libname}";
39 libssl = "${lib.getLib openssl}/lib/libssl${stdenv.hostPlatform.extensions.sharedLibrary}";
40 libcrypto = "${lib.getLib openssl}/lib/libcrypto${stdenv.hostPlatform.extensions.sharedLibrary}";
41 })];
42
43 nativeBuildInputs = lib.optional certifyBooks makeWrapper;
44
45 buildInputs = [
46 # ACL2 itself only needs a Common Lisp compiler/interpreter:
47 sbcl
48 ] ++ lib.optionals certifyBooks [
49 # To build community books, we need Perl and a couple of utilities:
50 which perl hostname
51 # Some of the books require one or more of these external tools:
52 glucose minisat abc-verifier libipasir
53 z3 (python3.withPackages (ps: [ ps.z3-solver ]))
54 ];
55
56 # NOTE: Parallel building can be memory-intensive depending on the number of
57 # concurrent jobs. For example, this build has been seen to use >120GB of
58 # RAM on an 85 core machine.
59 enableParallelBuilding = true;
60
61 preConfigure = ''
62 # When certifying books, ACL2 doesn't like $HOME not existing.
63 export HOME=$(pwd)/fake-home
64 '' + lib.optionalString certifyBooks ''
65 # Some books also care about $USER being nonempty.
66 export USER=nobody
67 '';
68
69 postConfigure = ''
70 # ACL2 and its books need to be built in place in the out directory because
71 # the proof artifacts are not relocatable. Since ACL2 mostly expects
72 # everything to exist in the original source tree layout, we put it in
73 # $out/share/${pname} and create symlinks in $out/bin as necessary.
74 mkdir -p $out/share/${pname}
75 cp -pR . $out/share/${pname}
76 cd $out/share/${pname}
77 '';
78
79 preBuild = "mkdir -p $HOME";
80 makeFlags = [ "LISP=${sbcl}/bin/sbcl" "ACL2_MAKE_LOG=NONE" ];
81
82 doCheck = true;
83 checkTarget = "mini-proveall";
84
85 installPhase = ''
86 mkdir -p $out/bin
87 ln -s $out/share/${pname}/saved_acl2 $out/bin/${pname}
88 '' + lib.optionalString certifyBooks ''
89 ln -s $out/share/${pname}/books/build/cert.pl $out/bin/${pname}-cert
90 ln -s $out/share/${pname}/books/build/clean.pl $out/bin/${pname}-clean
91 '';
92
93 preDistPhases = [ (if certifyBooks then "certifyBooksPhase" else "removeBooksPhase") ];
94
95 certifyBooksPhase = ''
96 # Certify the community books
97 pushd $out/share/${pname}/books
98 makeFlags="ACL2=$out/share/${pname}/saved_acl2"
99 buildFlags="all"
100 buildPhase
101
102 # Clean up some stuff to save space
103 find -name '*@useless-runes.lsp' -execdir rm {} + # saves ~1GB of space
104 find -name '*.cert.out' -execdir gzip {} + # saves ~400MB of space
105
106 popd
107 '';
108
109 removeBooksPhase = ''
110 # Delete the community books
111 rm -rf $out/share/${pname}/books
112 '';
113
114 meta = with lib; {
115 description = "Interpreter and a prover for a Lisp dialect";
116 mainProgram = "acl2";
117 longDescription = ''
118 ACL2 is a logic and programming language in which you can model computer
119 systems, together with a tool to help you prove properties of those
120 models. "ACL2" denotes "A Computational Logic for Applicative Common
121 Lisp".
122
123 ACL2 is part of the Boyer-Moore family of provers, for which its authors
124 have received the 2005 ACM Software System Award.
125
126 This package installs the main ACL2 executable ${pname}, as well as the
127 build tools cert.pl and clean.pl, renamed to ${pname}-cert and
128 ${pname}-clean.
129
130 '' + (if certifyBooks then ''
131 The community books are also included and certified with the `make
132 everything` target.
133 '' else ''
134 The community books are not included in this package.
135 '');
136 homepage = "https://www.cs.utexas.edu/users/moore/acl2/";
137 downloadPage = "https://github.com/acl2-devel/acl2-devel/releases";
138 license = with licenses; [
139 # ACL2 itself is bsd3
140 bsd3
141 ] ++ optionals certifyBooks [
142 # The community books are mostly bsd3 or mit but with a few
143 # other things thrown in.
144 mit gpl2 llgpl21 cc0 publicDomain unfreeRedistributable
145 ];
146 maintainers = with maintainers; [ kini raskin ];
147 platforms = platforms.all;
148 };
149}