acl2: 8.3 -> 8.4

4 files changed, 86 insertions, 146 deletions

diff --git a/pkgs/development/interpreters/acl2/0001-Fix-some-paths-for-Nix-build.patch b/pkgs/development/interpreters/acl2/0001-Fix-some-paths-for-Nix-build.patch
index 2b7f8b6a53b1..ac107414a92d 100644
--- a/pkgs/development/interpreters/acl2/0001-Fix-some-paths-for-Nix-build.patch
+++ b/pkgs/development/interpreters/acl2/0001-Fix-some-paths-for-Nix-build.patch
@@ -1,54 +1,46 @@
-From 43d23211dd7d22b5264ed06d446f89d632125da8 Mon Sep 17 00:00:00 2001
+From d0136f350b82ae845d56029db43d153c91d5e494 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
+Subject: [PATCH] Fix some paths for Nix build
 
 ---
  books/build/features.sh                       |  1 +
- .../ipasir/load-ipasir-sharedlib-raw.lsp      | 16 +++----
+ .../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-20181018-git/src/reload.lisp       | 48 ++-----------------
- .../shellpool-20150505-git/src/main.lisp      | 20 +-------
- 7 files changed, 15 insertions(+), 78 deletions(-)
+ .../cl+ssl-20200610-git/src/reload.lisp       | 53 +------------------
+ 6 files changed, 8 insertions(+), 60 deletions(-)
 
 diff --git a/books/build/features.sh b/books/build/features.sh
-index c8493d51a..def853f53 100755
+index d45a7aa61..27256b7cd 100755
 --- a/books/build/features.sh
 +++ b/books/build/features.sh
-@@ -84,6 +84,7 @@ fi
- 
+@@ -122,6 +122,7 @@ EOF
+ 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 ]];
++IPASIR_SHARED_LIBRARY=${IPASIR_SHARED_LIBRARY:-@libipasir@}
+ if check_ipasir; then
+     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 c6b0b3185..5ac5c675a 100644
+index 762e4ad4c..c9802cb58 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>
+@@ -30,11 +30,7 @@
  
--(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))))
+ (er-let* ((libname (acl2::getenv$ "IPASIR_SHARED_LIBRARY" acl2::*the-live-state*)))
+   (handler-case
+-      (cffi::load-foreign-library
+-       (or libname
+-           (cw "WARNING: $IPASIR_SHARED_LIBRARY not specified, ~
+-                defaulting to \"libipasirglucose4.so\"")
+-           "libipasirglucose4.so"))
++      (cffi::load-foreign-library (or libname "@libipasir@"))
+     (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
@@ -63,7 +55,7 @@ index c74073174..8d92355f7 100644
  
  ;; -----------------------------------------------------------------
 diff --git a/books/projects/smtlink/examples/examples.lisp b/books/projects/smtlink/examples/examples.lisp
-index bc66e0165..24f0d639c 100644
+index 90534892f..4ab98b2f0 100644
 --- a/books/projects/smtlink/examples/examples.lisp
 +++ b/books/projects/smtlink/examples/examples.lisp
 @@ -75,7 +75,7 @@ Subgoal 2
@@ -91,25 +83,32 @@ index 0d2703545..0f58904ea 100644
 @@ -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)
+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 @@
+ ;; These are 32-bit only.
  
  (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")))
+-                "/usr/lib/libcrypto.dylib"))
+-  (:cygwin (:or "cygcrypto-1.1.dll" "cygcrypto-1.0.0.dll")))
 +  (t "@openssl@/lib/libcrypto.so"))
  
  (cffi:define-foreign-library libssl
--  (:windows (:or "libssl32.dll" "ssleay32.dll"))
+-  (: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)
@@ -128,11 +127,13 @@ index 3f6aa35d0..ac4012363 100644
 -  ;; 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"
+-  ((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"
@@ -142,49 +143,12 @@ index 3f6aa35d0..ac4012363 100644
 -                                  "libssl.so.10"
 -                                  "libssl.so.4"
 -                                  "libssl.so"))
--  (:cygwin "cygssl-1.0.0.dll")
+-  (:cygwin (:or "cygssl-1.1.dll" "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
+2.31.1
 
diff --git a/pkgs/development/interpreters/acl2/0002-Restrict-RDTSC-to-x86.patch b/pkgs/development/interpreters/acl2/0002-Restrict-RDTSC-to-x86.patch
deleted file mode 100644
index 74af5adef649..000000000000
--- a/pkgs/development/interpreters/acl2/0002-Restrict-RDTSC-to-x86.patch
+++ /dev/null
@@ -1,29 +0,0 @@
-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
-
diff --git a/pkgs/development/interpreters/acl2/default.nix b/pkgs/development/interpreters/acl2/default.nix
index c089916158bd..2d104e9fb4c4 100644
--- a/pkgs/development/interpreters/acl2/default.nix
+++ b/pkgs/development/interpreters/acl2/default.nix
@@ -1,50 +1,53 @@
-{ lib, stdenv, callPackage, fetchFromGitHub, writeShellScriptBin, substituteAll
+{ lib, stdenv, callPackage, fetchFromGitHub, runCommandLocal, makeWrapper, substituteAll
 , sbcl, bash, which, perl, nettools
-, openssl, glucose, minisat, abc-verifier, z3, python2
+, openssl, glucose, minisat, abc-verifier, z3, python
 , certifyBooks ? true
 } @ args:
 
 let
-  # Disable immobile space so we don't run out of memory on large books; see
+  # Disable immobile space so we don't run out of memory on large books, and
+  # supply 2GB of dynamic space to avoid exhausting the heap while building the
+  # ACL2 system itself; see
   # https://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 "$@"'';
+  sbcl' = args.sbcl.override { disableImmobileSpace = true; };
+  sbcl = runCommandLocal args.sbcl.name { buildInputs = [ makeWrapper ]; } ''
+    makeWrapper ${sbcl'}/bin/sbcl $out/bin/sbcl \
+      --add-flags "--dynamic-space-size 2000"
+  '';
 
 in stdenv.mkDerivation rec {
   pname = "acl2";
-  version = "8.3";
+  version = "8.4";
 
   src = fetchFromGitHub {
     owner = "acl2-devel";
     repo = "acl2-devel";
     rev = version;
-    sha256 = "0c0wimaf16nrr3d6cxq6p7nr7rxffvpmn66hkpwc1m6zpcipf0y5";
+    sha256 = "16rr9zqmd3y1sd6zxff2f9gdd84l99pr7mdp1sjwmh427h661c68";
   };
 
-  libipasirglucose4 = callPackage ./libipasirglucose4 { };
+  # You can swap this out with any other IPASIR implementation at
+  # build time by using overrideAttrs (make sure the derivation you
+  # use has a "libname" attribute so we can plug it into the patch
+  # below).  Or, you can override it at runtime by setting the
+  # $IPASIR_SHARED_LIBRARY environment variable.
+  libipasir = 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
-  ];
+  patches = [(substituteAll {
+    src = ./0001-Fix-some-paths-for-Nix-build.patch;
+    libipasir = "${libipasir}/lib/${libipasir.libname}";
+    openssl = openssl.out;
+  })];
 
   buildInputs = [
     # ACL2 itself only needs a Common Lisp compiler/interpreter:
     sbcl
   ] ++ lib.optionals certifyBooks [
     # To build community books, we need Perl and a couple of utilities:
-    which perl nettools
+    which perl nettools makeWrapper
     # 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 ]))
+    openssl.out glucose minisat abc-verifier libipasir
+    z3 (python.withPackages (ps: [ ps.z3 ]))
   ];
 
   # NOTE: Parallel building can be memory-intensive depending on the number of
@@ -71,7 +74,7 @@ in stdenv.mkDerivation rec {
   '';
 
   preBuild = "mkdir -p $HOME";
-  makeFlags="LISP=${sbcl}/bin/sbcl";
+  makeFlags = "LISP=${sbcl}/bin/sbcl ACL2_MAKE_LOG=NONE";
 
   doCheck = true;
   checkTarget = "mini-proveall";
@@ -90,8 +93,13 @@ in stdenv.mkDerivation rec {
     # Certify the community books
     pushd $out/share/${pname}/books
     makeFlags="ACL2=$out/share/${pname}/saved_acl2"
-    buildFlags="everything"
+    buildFlags="all"
     buildPhase
+
+    # Clean up some stuff to save space
+    find -name '*@useless-runes.lsp' -execdir rm {} +  # saves ~1GB of space
+    find -name '*.cert.out' -execdir gz {} +           # saves ~400MB of space
+
     popd
   '';
 
diff --git a/pkgs/development/interpreters/acl2/libipasirglucose4/default.nix b/pkgs/development/interpreters/acl2/libipasirglucose4/default.nix
index 5c10c176c14a..dc8308267f40 100644
--- a/pkgs/development/interpreters/acl2/libipasirglucose4/default.nix
+++ b/pkgs/development/interpreters/acl2/libipasirglucose4/default.nix
@@ -1,17 +1,14 @@
 { lib, stdenv, fetchurl, zlib, unzip }:
 
-let
-
-  cxx = "${stdenv.cc.targetPrefix}c++";
-  libName = "libipasirglucose4" + stdenv.targetPlatform.extensions.sharedLibrary;
-
-in stdenv.mkDerivation rec {
+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";
 
+  libname = pname + stdenv.targetPlatform.extensions.sharedLibrary;
+
   src = fetchurl {
     url = "https://baldur.iti.kit.edu/sat-competition-2017/solvers/incremental/glucose-ipasir.zip";
     sha256 = "0xchgady9vwdh8frmc8swz6va53igp2wj1y9sshd0g7549n87wdj";
@@ -23,16 +20,16 @@ in stdenv.mkDerivation rec {
   sourceRoot = "sat/glucose4";
   patches = [ ./0001-Support-shared-library-build.patch ];
 
-  makeFlags = [ "CXX=${cxx}" ];
+  makeFlags = [ "CXX=${stdenv.cc.targetPrefix}c++" ];
 
   postBuild = ''
-    ${cxx} -shared -o ${libName} \
-        ${if stdenv.cc.isClang then "" else "-Wl,-soname,${libName}"} \
+    $CXX -shared -o ${libname} \
+        ${if stdenv.cc.isClang then "" else "-Wl,-soname,${libname}"} \
         ipasirglucoseglue.o libipasirglucose4.a
   '';
 
   installPhase = ''
-    install -D ${libName} $out/lib/${libName}
+    install -D ${libname} $out/lib/${libname}
   '';
 
   meta = with lib; {