Merge pull request #183139 from kini/acl2-update

From d0136f350b82ae845d56029db43d153c91d5e494 Mon Sep 17 00:00:00 2001

From aed1c4b0be7576d20eed81070da2c6f92573df18 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] Fix some paths for Nix build

---

 books/build/features.sh                                     | 1 +

 .../ipasir/load-ipasir-sharedlib-raw.lsp      |  6 +--

 books/projects/smtlink/config.lisp            |  2 +-

 books/projects/smtlink/examples/examples.lisp |  4 +-

 books/projects/smtlink/smtlink-config         |  2 +-

 .../cl+ssl-20200610-git/src/reload.lisp       | 53 +------------------

 6 files changed, 8 insertions(+), 60 deletions(-)

 books/centaur/ipasir/load-ipasir-sharedlib-raw.lsp          | 6 +-----

 .../bundle/software/cl+ssl-20220707-git/src/reload.lisp     | 3 +++

 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/books/build/features.sh b/books/build/features.sh

index d45a7aa61..27256b7cd 100755

index feb5b2b59c..4b654e08bc 100755

--- a/books/build/features.sh

+++ b/books/build/features.sh

@@ -122,6 +122,7 @@ EOF

@@ -125,6 +125,7 @@ EOF

 fi

 echo "Determining whether an ipasir shared library is installed" 1>&2

     cat >> Makefile-features <<EOF

 export OS_HAS_IPASIR ?= 1

diff --git a/books/centaur/ipasir/load-ipasir-sharedlib-raw.lsp b/books/centaur/ipasir/load-ipasir-sharedlib-raw.lsp

index 762e4ad4c..c9802cb58 100644

index 762e4ad4c0..c9802cb582 100644

--- a/books/centaur/ipasir/load-ipasir-sharedlib-raw.lsp

+++ b/books/centaur/ipasir/load-ipasir-sharedlib-raw.lsp

@@ -30,11 +30,7 @@

     (error () (er hard? 'load-ipasir-shardlib-raw

                   "Couldn't load ipasir shared library from ~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 90534892f..4ab98b2f0 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-20200610-git/src/reload.lisp b/books/quicklisp/bundle/software/cl+ssl-20200610-git/src/reload.lisp

index e5db28645..65eb818a1 100644

--- a/books/quicklisp/bundle/software/cl+ssl-20200610-git/src/reload.lisp

+++ b/books/quicklisp/bundle/software/cl+ssl-20200610-git/src/reload.lisp

@@ -37,59 +37,10 @@

diff --git a/books/quicklisp/bundle/software/cl+ssl-20220707-git/src/reload.lisp b/books/quicklisp/bundle/software/cl+ssl-20220707-git/src/reload.lisp

index d409b4440f..5c65c5b4da 100644

--- a/books/quicklisp/bundle/software/cl+ssl-20220707-git/src/reload.lisp

+++ b/books/quicklisp/bundle/software/cl+ssl-20220707-git/src/reload.lisp

@@ -87,6 +87,9 @@ sudo rm /usr/local/lib/libcrypto.dylib /usr/local/lib/libssl.dylib

 ;;

 ;; These are 32-bit only.

+(cl+ssl/config:define-libssl-path "@libssl@")

+(cl+ssl/config:define-libcrypto-path "@libcrypto@")

+

 (unless cl+ssl/config::*libcrypto-override*

   (cffi:define-foreign-library libcrypto

-  (:windows (:or #+(and windows x86-64) "libcrypto-1_1-x64.dll"

-                 #+(and windows x86) "libcrypto-1_1.dll"

-                 "libeay32.dll"))

-  (: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"))

-  (:cygwin (:or "cygcrypto-1.1.dll" "cygcrypto-1.0.0.dll")))

+  (t "@libcrypto@"))

 (cffi:define-foreign-library libssl

-  (:windows (:or #+(and windows x86-64) "libssl-1_1-x64.dll"

-                 #+(and windows x86) "libssl-1_1.dll"

-                 "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.1"

-                                  "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.1f"

-                                  "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 (:or "cygssl-1.1.dll" "cygssl-1.0.0.dll"))

-  (t (:default "libssl3")))

+  (t "@libssl@"))

 (unless (member :cl+ssl-foreign-libs-already-loaded

                 *features*)

     (:windows (:or #+(and windows x86-64) "libcrypto-1_1-x64.dll"

-- 

2.31.1

in stdenv.mkDerivation rec {

  pname = "acl2";

  version = "8.4";

  version = "8.5";

  src = fetchFromGitHub {

    owner = "acl2-devel";

    repo = "acl2-devel";

    rev = version;

    sha256 = "16rr9zqmd3y1sd6zxff2f9gdd84l99pr7mdp1sjwmh427h661c68";

    sha256 = "12cv5ms1j3vfrq066km020nwxb6x2dzh12g8nz6xxyxysn44wzzi";

  };

  # You can swap this out with any other IPASIR implementation at