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