From 43d23211dd7d22b5264ed06d446f89d632125da8 Mon Sep 17 00:00:00 2001 From: Keshav Kini 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 -(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