9a32d3d136
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.
190 lines
8.2 KiB
Diff
190 lines
8.2 KiB
Diff
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
|
|
|