0eaa97ffad
GitOrigin-RevId: c59ea8b8a0e7f927e7291c14ea6cd1bd3a16ff38
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
|
|
|