acl2, acl2-minimal: build standard library, init

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.

5 files changed, 410 insertions, 50 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
new file mode 100644
index 0000000000000..2b7f8b6a53b1e
--- /dev/null
+++ b/pkgs/development/interpreters/acl2/0001-Fix-some-paths-for-Nix-build.patch
@@ -0,0 +1,190 @@
+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
+
diff --git a/pkgs/development/interpreters/acl2/0002-Restrict-RDTSC-to-x86.patch b/pkgs/development/interpreters/acl2/0002-Restrict-RDTSC-to-x86.patch
new file mode 100644
index 0000000000000..74af5adef6493
--- /dev/null
+++ b/pkgs/development/interpreters/acl2/0002-Restrict-RDTSC-to-x86.patch
@@ -0,0 +1,29 @@
+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 39b243a0ce6a9..e3c62aae98337 100644
--- a/pkgs/development/interpreters/acl2/default.nix
+++ b/pkgs/development/interpreters/acl2/default.nix
@@ -1,15 +1,19 @@
-{ stdenv, fetchFromGitHub,
-  # perl, which, nettools,
-  sbcl }:
-
-let hashes = {
-  "8.0" = "1x1giy2c1y6krg3kf8pf9wrmvk981shv0pxcwi483yjqm90xng4r";
-  "8.3" = "0c0wimaf16nrr3d6cxq6p7nr7rxffvpmn66hkpwc1m6zpcipf0y5";
-};
-revs = {
-  "8.0" = "8.0";
-  "8.3" = "8.3";
-};
+{ stdenv, callPackage, fetchFromGitHub, writeShellScriptBin, substituteAll
+, sbcl, bash, which, perl, nettools
+, openssl, glucose, minisat, abc-verifier, z3, python2
+, certifyBooks ? true
+} @ args:
+
+let
+  # Disable immobile space so we don't run out of memory on large books; see
+  # http://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 "$@"'';
+
 in stdenv.mkDerivation rec {
   pname = "acl2";
   version = "8.3";
@@ -17,62 +21,117 @@ in stdenv.mkDerivation rec {
   src = fetchFromGitHub {
     owner = "acl2-devel";
     repo = "acl2-devel";
-    rev = revs.${version};
-    sha256 = hashes.${version};
+    rev = "${version}";
+    sha256 = "0c0wimaf16nrr3d6cxq6p7nr7rxffvpmn66hkpwc1m6zpcipf0y5";
   };
 
-  buildInputs = [ sbcl
-    # which perl nettools
+  libipasirglucose4 = 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
   ];
 
+  buildInputs = [
+    # ACL2 itself only needs a Common Lisp compiler/interpreter:
+    sbcl
+  ] ++ stdenv.lib.optionals certifyBooks [
+    # To build community books, we need Perl and a couple of utilities:
+    which perl nettools
+    # 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 ]))
+  ];
+
+  # NOTE: Parallel building can be memory-intensive depending on the number of
+  # concurrent jobs.  For example, this build has been seen to use >120GB of
+  # RAM on an 85 core machine.
   enableParallelBuilding = true;
 
-  phases = "unpackPhase installPhase";
+  preConfigure = ''
+    # When certifying books, ACL2 doesn't like $HOME not existing.
+    export HOME=$(pwd)/fake-home
+  '' + stdenv.lib.optionalString certifyBooks ''
+    # Some books also care about $USER being nonempty.
+    export USER=nobody
+  '';
 
-  installSuffix = "acl2";
+  postConfigure = ''
+    # ACL2 and its books need to be built in place in the out directory because
+    # the proof artifacts are not relocatable. Since ACL2 mostly expects
+    # everything to exist in the original source tree layout, we put it in
+    # $out/share/${pname} and create symlinks in $out/bin as necessary.
+    mkdir -p $out/share/${pname}
+    cp -pR . $out/share/${pname}
+    cd $out/share/${pname}
+  '';
+
+  preBuild = "mkdir -p $HOME";
+  makeFlags="LISP=${sbcl}/bin/sbcl";
+
+  doCheck = true;
+  checkTarget = "mini-proveall";
 
   installPhase = ''
-    mkdir -p $out/share/${installSuffix}
     mkdir -p $out/bin
-    cp -R . $out/share/${installSuffix}
-    cd $out/share/${installSuffix}
+    ln -s $out/share/${pname}/saved_acl2           $out/bin/${pname}
+  '' + stdenv.lib.optionalString certifyBooks ''
+    ln -s $out/share/${pname}/books/build/cert.pl  $out/bin/${pname}-cert
+    ln -s $out/share/${pname}/books/build/clean.pl $out/bin/${pname}-clean
+  '';
 
-    # make ACL2 image
-    make LISP=${sbcl}/bin/sbcl
+  preDistPhases = [ (if certifyBooks then "certifyBooksPhase" else "removeBooksPhase") ];
 
-    # The community books don't build properly under Nix yet.
-    rm -rf books
-    #make ACL2=$out/share/saved_acl2 USE_QUICKLISP=1 regression-everything
+  certifyBooksPhase = ''
+    # Certify the community books
+    pushd $out/share/${pname}/books
+    makeFlags="ACL2=$out/share/${pname}/saved_acl2"
+    buildFlags="everything"
+    buildPhase
+    popd
+  '';
 
-    cp saved_acl2 $out/bin/acl2
+  removeBooksPhase = ''
+    # Delete the community books
+    rm -rf $out/share/${pname}/books
   '';
 
-  meta = {
+  meta = with stdenv.lib; {
     description = "An interpreter and a prover for a Lisp dialect";
     longDescription = ''
-      ACL2 is a logic and programming language in which you can model
-      computer systems, together with a tool to help you prove
-      properties of those models. "ACL2" denotes "A Computational
-      Logic for Applicative Common Lisp".
-
-      ACL2 is part of the Boyer-Moore family of provers, for which its
-      authors have received the 2005 ACM Software System Award.
-
-      NOTE: In nixpkgs, the community books that usually ship with
-      ACL2 have been removed because it is not currently possible to
-      build them with Nix.
-    '';
+      ACL2 is a logic and programming language in which you can model computer
+      systems, together with a tool to help you prove properties of those
+      models. "ACL2" denotes "A Computational Logic for Applicative Common
+      Lisp".
+
+      ACL2 is part of the Boyer-Moore family of provers, for which its authors
+      have received the 2005 ACM Software System Award.
+
+      This package installs the main ACL2 executable ${pname}, as well as the
+      build tools cert.pl and clean.pl, renamed to ${pname}-cert and
+      ${pname}-clean.
+
+    '' + (if certifyBooks then ''
+      The community books are also included and certified with the `make
+      everything` target.
+    '' else ''
+      The community books are not included in this package.
+    '');
     homepage = "http://www.cs.utexas.edu/users/moore/acl2/";
     downloadPage = "https://github.com/acl2-devel/acl2-devel/releases";
-    # There are a bunch of licenses in the community books, but since
-    # they currently get deleted during the build, we don't mention
-    # their licenses here.  ACL2 proper is released under a BSD
-    # 3-clause license.
-    #license = with stdenv.lib.licenses;
-    #[ free bsd3 mit gpl2 llgpl21 cc0 publicDomain ];
-    license = stdenv.lib.licenses.bsd3;
-    maintainers = with stdenv.lib.maintainers; [ kini raskin ];
-    platforms = stdenv.lib.platforms.all;
-    broken = stdenv.isAarch64 && stdenv.isLinux;
+    license = with licenses; [
+      # ACL2 itself is bsd3
+      bsd3
+    ] ++ optionals certifyBooks [
+      # The community books are mostly bsd3 or mit but with a few
+      # other things thrown in.
+      mit gpl2 llgpl21 cc0 publicDomain unfreeRedistributable
+    ];
+    maintainers = with maintainers; [ kini raskin ];
+    platforms = platforms.all;
   };
 }
diff --git a/pkgs/development/interpreters/acl2/libipasirglucose4/0001-Support-shared-library-build.patch b/pkgs/development/interpreters/acl2/libipasirglucose4/0001-Support-shared-library-build.patch
new file mode 100644
index 0000000000000..c78fa1ab925a3
--- /dev/null
+++ b/pkgs/development/interpreters/acl2/libipasirglucose4/0001-Support-shared-library-build.patch
@@ -0,0 +1,46 @@
+From 0f48e046f44624f4d4d8255ac5bd26397a38f16c Mon Sep 17 00:00:00 2001
+From: Keshav Kini <keshav.kini@gmail.com>
+Date: Sun, 23 Feb 2020 14:09:30 -0800
+Subject: [PATCH] Support shared library build
+
+Patch taken from [the ACL2 Books documentation][1].
+
+- Add " -fPIC" to the CXXFLAGS to build position-independent code,
+  required for shared libraries.
+
+- Add the line "export CXXFLAGS" below the setting of CXXFLAGS, so that
+  those flags apply to the recursive make of the core solver library.
+
+- Fix a typo: replace the occurrence of "CXXLAGS" with "CXXFLAGS".
+
+[1]: http://www.cs.utexas.edu/users/moore/acl2/v8-2/combined-manual/index.html?topic=IPASIR____BUILDING-AN-IPASIR-SOLVER-LIBRARY
+---
+ makefile | 5 +++--
+ 1 file changed, 3 insertions(+), 2 deletions(-)
+
+diff --git a/makefile b/makefile
+index 07121de..4e85c4b 100755
+--- a/makefile
++++ b/makefile
+@@ -29,7 +29,8 @@ TARGET=libipasir$(SIG).a
+ 
+ CXX=g++  
+ 
+-CXXFLAGS= -g -std=c++11 -Wall -DNDEBUG -O3
++CXXFLAGS= -g -std=c++11 -Wall -DNDEBUG -O3 -fPIC
++export CXXFLAGS
+ 
+ #-----------------------------------------------------------------------#
+ #- REQUIRED TOP RULES --------------------------------------------------#
+@@ -67,7 +68,7 @@ libipasir$(SIG).a: .FORCE
+ #-----------------------------------------------------------------------#
+ 
+ ipasir$(NAME)glue.o: ipasir$(NAME)glue.cc ipasir.h makefile
+-	$(CXX) -g  -std=c++11 $(CXXLAGS) \
++	$(CXX) -g  -std=c++11 $(CXXFLAGS) \
+ 	  -DVERSION=\"$(VERSION)\" \
+ 	  -I$(DIR) -I$(DIR)/core -c ipasir$(NAME)glue.cc
+ 
+-- 
+2.23.1
+
diff --git a/pkgs/development/interpreters/acl2/libipasirglucose4/default.nix b/pkgs/development/interpreters/acl2/libipasirglucose4/default.nix
new file mode 100644
index 0000000000000..5186cd69584e1
--- /dev/null
+++ b/pkgs/development/interpreters/acl2/libipasirglucose4/default.nix
@@ -0,0 +1,36 @@
+{ stdenv, fetchurl, zlib, unzip }:
+
+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";
+
+  src = fetchurl {
+    url = "https://baldur.iti.kit.edu/sat-competition-2017/solvers/incremental/glucose-ipasir.zip";
+    sha256 = "0xchgady9vwdh8frmc8swz6va53igp2wj1y9sshd0g7549n87wdj";
+  };
+  nativeBuildInputs = [ unzip ];
+
+  buildInputs = [ zlib ];
+
+  sourceRoot = "sat/glucose4";
+  patches = [ ./0001-Support-shared-library-build.patch ];
+
+  postBuild = ''
+    g++ -shared -Wl,-soname,libipasirglucose4.so -o libipasirglucose4.so \
+        ipasirglucoseglue.o libipasirglucose4.a
+  '';
+
+  installPhase = ''
+    install -D libipasirglucose4.so $out/lib/libipasirglucose4.so
+  '';
+
+  meta = with stdenv.lib; {
+    description = "Shared library providing IPASIR interface to the Glucose SAT solver";
+    license = licenses.mit;
+    platforms = platforms.unix;
+    maintainers = with maintainers; [ kini ];
+  };
+}