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.
This commit is contained in:
Keshav Kini 2020-02-23 21:12:37 -08:00
parent 181179c53b
commit 9a32d3d136
6 changed files with 415 additions and 54 deletions

View file

@ -0,0 +1,190 @@
From 43d23211dd7d22b5264ed06d446f89d632125da8 Mon Sep 17 00:00:00 2001
From: Keshav Kini <keshav.kini@gmail.com>
Date: Sat, 30 May 2020 21:27:47 -0700
Subject: [PATCH 1/2] Fix some paths for Nix build
---
books/build/features.sh | 1 +
.../ipasir/load-ipasir-sharedlib-raw.lsp | 16 +++----
books/projects/smtlink/config.lisp | 2 +-
books/projects/smtlink/examples/examples.lisp | 4 +-
books/projects/smtlink/smtlink-config | 2 +-
.../cl+ssl-20181018-git/src/reload.lisp | 48 ++-----------------
.../shellpool-20150505-git/src/main.lisp | 20 +-------
7 files changed, 15 insertions(+), 78 deletions(-)
diff --git a/books/build/features.sh b/books/build/features.sh
index c8493d51a..def853f53 100755
--- a/books/build/features.sh
+++ b/books/build/features.sh
@@ -84,6 +84,7 @@ fi
echo "Determining whether an ipasir shared library is installed" 1>&2
+IPASIR_SHARED_LIBRARY=${IPASIR_SHARED_LIBRARY:-@libipasirglucose4@/lib/libipasirglucose4.so}
if [[ $IPASIR_SHARED_LIBRARY != '' ]];
then
if [[ -e $IPASIR_SHARED_LIBRARY ]];
diff --git a/books/centaur/ipasir/load-ipasir-sharedlib-raw.lsp b/books/centaur/ipasir/load-ipasir-sharedlib-raw.lsp
index c6b0b3185..5ac5c675a 100644
--- a/books/centaur/ipasir/load-ipasir-sharedlib-raw.lsp
+++ b/books/centaur/ipasir/load-ipasir-sharedlib-raw.lsp
@@ -28,13 +28,9 @@
;
; Original authors: Sol Swords <sswords@centtech.com>
-(er-let* ((libname (acl2::getenv$ "IPASIR_SHARED_LIBRARY" acl2::*the-live-state*)))
- (if libname
- (handler-case
- (cffi::load-foreign-library libname)
- (error () (er hard? 'load-ipasir-shardlib-raw
- "Couldn't load the specified ipasir shared library, ~s0."
- libname)))
- (er hard? 'load-ipasir-shardlib-raw
- "Couldn't load an ipasir library because the ~
- IPASIR_SHARED_LIBRARY environment variable was unset.")))
+(let ((libname "@libipasirglucose4@/lib/libipasirglucose4.so"))
+ (handler-case
+ (cffi::load-foreign-library libname)
+ (error () (er hard? 'load-ipasir-shardlib-raw
+ "Couldn't load the specified ipasir shared library, ~s0."
+ libname))))
diff --git a/books/projects/smtlink/config.lisp b/books/projects/smtlink/config.lisp
index c74073174..8d92355f7 100644
--- a/books/projects/smtlink/config.lisp
+++ b/books/projects/smtlink/config.lisp
@@ -51,7 +51,7 @@ where the system books are."))
(make-smtlink-config :interface-dir interface-dir
:smt-module "ACL2_to_Z3"
:smt-class "ACL22SMT"
- :smt-cmd "/usr/bin/env python"
+ :smt-cmd "python"
:pythonpath "")))
;; -----------------------------------------------------------------
diff --git a/books/projects/smtlink/examples/examples.lisp b/books/projects/smtlink/examples/examples.lisp
index bc66e0165..24f0d639c 100644
--- a/books/projects/smtlink/examples/examples.lisp
+++ b/books/projects/smtlink/examples/examples.lisp
@@ -75,7 +75,7 @@ Subgoal 2
Subgoal 2.2
Subgoal 2.2'
Using default SMT-trusted-cp...
-; SMT solver: `/usr/bin/env python /tmp/py_file/smtlink.w59zR`: 0.52 sec, 7,904 bytes
+; SMT solver: `python /tmp/py_file/smtlink.w59zR`: 0.52 sec, 7,904 bytes
Proved!
Subgoal 2.2''
Subgoal 2.1
@@ -139,7 +139,7 @@ read back into ACL2. Below are the outputs from this clause processor called
@({
Using default SMT-trusted-cp...
-; SMT solver: `/usr/bin/env python /tmp/py_file/smtlink.w59zR`: 0.52 sec, 7,904 bytes
+; SMT solver: `python /tmp/py_file/smtlink.w59zR`: 0.52 sec, 7,904 bytes
Proved!
})
diff --git a/books/projects/smtlink/smtlink-config b/books/projects/smtlink/smtlink-config
index 0d2703545..0f58904ea 100644
--- a/books/projects/smtlink/smtlink-config
+++ b/books/projects/smtlink/smtlink-config
@@ -1 +1 @@
-smt-cmd=/usr/bin/env python
+smt-cmd=python
diff --git a/books/quicklisp/bundle/software/cl+ssl-20181018-git/src/reload.lisp b/books/quicklisp/bundle/software/cl+ssl-20181018-git/src/reload.lisp
index 3f6aa35d0..ac4012363 100644
--- a/books/quicklisp/bundle/software/cl+ssl-20181018-git/src/reload.lisp
+++ b/books/quicklisp/bundle/software/cl+ssl-20181018-git/src/reload.lisp
@@ -20,54 +20,12 @@
(in-package :cl+ssl)
(cffi:define-foreign-library libcrypto
- (:openbsd "libcrypto.so")
- (:darwin (:or "/opt/local/lib/libcrypto.dylib" ;; MacPorts
- "/sw/lib/libcrypto.dylib" ;; Fink
- "/usr/local/opt/openssl/lib/libcrypto.dylib" ;; Homebrew
- "/usr/local/lib/libcrypto.dylib" ;; personalized install
- "libcrypto.dylib" ;; default system libcrypto, which may have insufficient crypto
- "/usr/lib/libcrypto.dylib")))
+ (t "@openssl@/lib/libcrypto.so"))
(cffi:define-foreign-library libssl
- (:windows (:or "libssl32.dll" "ssleay32.dll"))
- ;; The default OS-X libssl seems have had insufficient crypto algos
- ;; (missing TLSv1_[1,2]_XXX methods,
- ;; see https://github.com/cl-plus-ssl/cl-plus-ssl/issues/56)
- ;; so first try to load possible custom installations of libssl
- (:darwin (:or "/opt/local/lib/libssl.dylib" ;; MacPorts
- "/sw/lib/libssl.dylib" ;; Fink
- "/usr/local/opt/openssl/lib/libssl.dylib" ;; Homebrew
- "/usr/local/lib/libssl.dylib" ;; personalized install
- "libssl.dylib" ;; default system libssl, which may have insufficient crypto
- "/usr/lib/libssl.dylib"))
- (:solaris (:or "/lib/64/libssl.so"
- "libssl.so.0.9.8" "libssl.so" "libssl.so.4"))
- ;; Unlike some other systems, OpenBSD linker,
- ;; when passed library name without versions at the end,
- ;; will locate the library with highest macro.minor version,
- ;; so we can just use just "libssl.so".
- ;; More info at https://github.com/cl-plus-ssl/cl-plus-ssl/pull/2.
- (:openbsd "libssl.so")
- ((and :unix (not :cygwin)) (:or "libssl.so.1.0.2m"
- "libssl.so.1.0.2k"
- "libssl.so.1.0.2"
- "libssl.so.1.0.1l"
- "libssl.so.1.0.1j"
- "libssl.so.1.0.1e"
- "libssl.so.1.0.1"
- "libssl.so.1.0.0q"
- "libssl.so.1.0.0"
- "libssl.so.0.9.8ze"
- "libssl.so.0.9.8"
- "libssl.so.10"
- "libssl.so.4"
- "libssl.so"))
- (:cygwin "cygssl-1.0.0.dll")
- (t (:default "libssl3")))
-
-(cffi:define-foreign-library libeay32
- (:windows "libeay32.dll"))
+ (t "@openssl@/lib/libssl.so"))
+(cffi:define-foreign-library libeay32)
(unless (member :cl+ssl-foreign-libs-already-loaded
*features*)
diff --git a/books/quicklisp/bundle/software/shellpool-20150505-git/src/main.lisp b/books/quicklisp/bundle/software/shellpool-20150505-git/src/main.lisp
index cda8dc94c..11035ea09 100644
--- a/books/quicklisp/bundle/software/shellpool-20150505-git/src/main.lisp
+++ b/books/quicklisp/bundle/software/shellpool-20150505-git/src/main.lisp
@@ -106,26 +106,8 @@
; Glue
-#-sbcl
(defun find-bash ()
- #+windows "bash.exe"
- #-windows "bash")
-
-#+sbcl
-;; SBCL (on Linux, at least) won't successfully run "bash" all by itself. So,
-;; on SBCL, try to find a likely bash. BOZO this probably isn't great. It
-;; would be better to search the user's PATH for which bash to use.
-(let ((found-bash))
- (defun find-bash ()
- (or found-bash
- (let ((paths-to-try '("/bin/bash"
- "/usr/bin/bash"
- "/usr/local/bin/bash")))
- (loop for path in paths-to-try do
- (when (cl-fad::file-exists-p path)
- (setq found-bash path)
- (return-from find-bash path)))
- (error "Bash not found among ~s" paths-to-try)))))
+ "@bash@/bin/bash")
#+(or allegro lispworks)
(defstruct bashprocess
--
2.25.4

View file

@ -0,0 +1,29 @@
From b0ccf68f277d0bd5e6fc9d41742f31ddda99a955 Mon Sep 17 00:00:00 2001
From: Keshav Kini <keshav.kini@gmail.com>
Date: Mon, 1 Jun 2020 21:42:24 -0700
Subject: [PATCH 2/2] Restrict RDTSC to x86
Backported from [1]. According to Curtis Dunham, this should fix the ACL2 base
system build on ARM.
[1]: https://github.com/acl2/acl2/commit/292fa2ccc6217e6307d7bb8373eb90f5d258ea5e
---
memoize-raw.lisp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/memoize-raw.lisp b/memoize-raw.lisp
index 205e78653..478198dee 100644
--- a/memoize-raw.lisp
+++ b/memoize-raw.lisp
@@ -189,7 +189,7 @@
;; RDTSC nonsense, but we still can report mysterious results since we have no
;; clue about which core we are running on in CCL (or, presumably, SBCL).
-#+(or ccl sbcl)
+#+(and (or ccl sbcl) x86-64)
(eval-when
(:execute :compile-toplevel :load-toplevel)
(when #+ccl (fboundp 'ccl::rdtsc)
--
2.25.4

View file

@ -1,15 +1,19 @@
{ stdenv, fetchFromGitHub,
# perl, which, nettools,
sbcl }:
{ 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 "$@"'';
let hashes = {
"8.0" = "1x1giy2c1y6krg3kf8pf9wrmvk981shv0pxcwi483yjqm90xng4r";
"8.3" = "0c0wimaf16nrr3d6cxq6p7nr7rxffvpmn66hkpwc1m6zpcipf0y5";
};
revs = {
"8.0" = "8.0";
"8.3" = "8.3";
};
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";
installSuffix = "acl2";
installPhase = ''
mkdir -p $out/share/${installSuffix}
mkdir -p $out/bin
cp -R . $out/share/${installSuffix}
cd $out/share/${installSuffix}
# make ACL2 image
make LISP=${sbcl}/bin/sbcl
# The community books don't build properly under Nix yet.
rm -rf books
#make ACL2=$out/share/saved_acl2 USE_QUICKLISP=1 regression-everything
cp saved_acl2 $out/bin/acl2
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
'';
meta = {
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/bin
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
'';
preDistPhases = [ (if certifyBooks then "certifyBooksPhase" else "removeBooksPhase") ];
certifyBooksPhase = ''
# Certify the community books
pushd $out/share/${pname}/books
makeFlags="ACL2=$out/share/${pname}/saved_acl2"
buildFlags="everything"
buildPhase
popd
'';
removeBooksPhase = ''
# Delete the community books
rm -rf $out/share/${pname}/books
'';
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 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.
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.
'';
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;
};
}

View file

@ -0,0 +1,46 @@
From 0f48e046f44624f4d4d8255ac5bd26397a38f16c Mon Sep 17 00:00:00 2001
From: Keshav Kini <keshav.kini@gmail.com>
Date: Sun, 23 Feb 2020 14:09:30 -0800
Subject: [PATCH] Support shared library build
Patch taken from [the ACL2 Books documentation][1].
- Add " -fPIC" to the CXXFLAGS to build position-independent code,
required for shared libraries.
- Add the line "export CXXFLAGS" below the setting of CXXFLAGS, so that
those flags apply to the recursive make of the core solver library.
- Fix a typo: replace the occurrence of "CXXLAGS" with "CXXFLAGS".
[1]: http://www.cs.utexas.edu/users/moore/acl2/v8-2/combined-manual/index.html?topic=IPASIR____BUILDING-AN-IPASIR-SOLVER-LIBRARY
---
makefile | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/makefile b/makefile
index 07121de..4e85c4b 100755
--- a/makefile
+++ b/makefile
@@ -29,7 +29,8 @@ TARGET=libipasir$(SIG).a
CXX=g++
-CXXFLAGS= -g -std=c++11 -Wall -DNDEBUG -O3
+CXXFLAGS= -g -std=c++11 -Wall -DNDEBUG -O3 -fPIC
+export CXXFLAGS
#-----------------------------------------------------------------------#
#- REQUIRED TOP RULES --------------------------------------------------#
@@ -67,7 +68,7 @@ libipasir$(SIG).a: .FORCE
#-----------------------------------------------------------------------#
ipasir$(NAME)glue.o: ipasir$(NAME)glue.cc ipasir.h makefile
- $(CXX) -g -std=c++11 $(CXXLAGS) \
+ $(CXX) -g -std=c++11 $(CXXFLAGS) \
-DVERSION=\"$(VERSION)\" \
-I$(DIR) -I$(DIR)/core -c ipasir$(NAME)glue.cc
--
2.23.1

View file

@ -0,0 +1,36 @@
{ stdenv, fetchurl, zlib, unzip }:
stdenv.mkDerivation rec {
pname = "libipasirglucose4";
# This library has no version number AFAICT (beyond generally being based on
# Glucose 4.x), but it was submitted to the 2017 SAT competition so let's use
# that as the version number, I guess.
version = "2017";
src = fetchurl {
url = "https://baldur.iti.kit.edu/sat-competition-2017/solvers/incremental/glucose-ipasir.zip";
sha256 = "0xchgady9vwdh8frmc8swz6va53igp2wj1y9sshd0g7549n87wdj";
};
nativeBuildInputs = [ unzip ];
buildInputs = [ zlib ];
sourceRoot = "sat/glucose4";
patches = [ ./0001-Support-shared-library-build.patch ];
postBuild = ''
g++ -shared -Wl,-soname,libipasirglucose4.so -o libipasirglucose4.so \
ipasirglucoseglue.o libipasirglucose4.a
'';
installPhase = ''
install -D libipasirglucose4.so $out/lib/libipasirglucose4.so
'';
meta = with stdenv.lib; {
description = "Shared library providing IPASIR interface to the Glucose SAT solver";
license = licenses.mit;
platforms = platforms.unix;
maintainers = with maintainers; [ kini ];
};
}

View file

@ -9620,6 +9620,7 @@ in
### DEVELOPMENT / INTERPRETERS
acl2 = callPackage ../development/interpreters/acl2 { };
acl2-minimal = callPackage ../development/interpreters/acl2 { certifyBooks = false; };
angelscript = callPackage ../development/interpreters/angelscript {};