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