Merge pull request #85903 from kini/acl2-update
acl2: build standard library as well
This commit is contained in:
commit
ee02ea68d4
|
@ -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
|
||||||
|
|
|
@ -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
|
||||||
|
|
|
@ -1,15 +1,19 @@
|
||||||
{ stdenv, fetchFromGitHub,
|
{ stdenv, callPackage, fetchFromGitHub, writeShellScriptBin, substituteAll
|
||||||
# perl, which, nettools,
|
, sbcl, bash, which, perl, nettools
|
||||||
sbcl }:
|
, 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 "$@"'';
|
||||||
|
|
||||||
let hashes = {
|
|
||||||
"8.0" = "1x1giy2c1y6krg3kf8pf9wrmvk981shv0pxcwi483yjqm90xng4r";
|
|
||||||
"8.3" = "0c0wimaf16nrr3d6cxq6p7nr7rxffvpmn66hkpwc1m6zpcipf0y5";
|
|
||||||
};
|
|
||||||
revs = {
|
|
||||||
"8.0" = "8.0";
|
|
||||||
"8.3" = "8.3";
|
|
||||||
};
|
|
||||||
in stdenv.mkDerivation rec {
|
in stdenv.mkDerivation rec {
|
||||||
pname = "acl2";
|
pname = "acl2";
|
||||||
version = "8.3";
|
version = "8.3";
|
||||||
|
@ -17,62 +21,117 @@ in stdenv.mkDerivation rec {
|
||||||
src = fetchFromGitHub {
|
src = fetchFromGitHub {
|
||||||
owner = "acl2-devel";
|
owner = "acl2-devel";
|
||||||
repo = "acl2-devel";
|
repo = "acl2-devel";
|
||||||
rev = revs.${version};
|
rev = "${version}";
|
||||||
sha256 = hashes.${version};
|
sha256 = "0c0wimaf16nrr3d6cxq6p7nr7rxffvpmn66hkpwc1m6zpcipf0y5";
|
||||||
};
|
};
|
||||||
|
|
||||||
buildInputs = [ sbcl
|
libipasirglucose4 = callPackage ./libipasirglucose4 { };
|
||||||
# which perl nettools
|
|
||||||
|
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;
|
enableParallelBuilding = true;
|
||||||
|
|
||||||
phases = "unpackPhase installPhase";
|
preConfigure = ''
|
||||||
|
# When certifying books, ACL2 doesn't like $HOME not existing.
|
||||||
installSuffix = "acl2";
|
export HOME=$(pwd)/fake-home
|
||||||
|
'' + stdenv.lib.optionalString certifyBooks ''
|
||||||
installPhase = ''
|
# Some books also care about $USER being nonempty.
|
||||||
mkdir -p $out/share/${installSuffix}
|
export USER=nobody
|
||||||
mkdir -p $out/bin
|
|
||||||
cp -R . $out/share/${installSuffix}
|
|
||||||
cd $out/share/${installSuffix}
|
|
||||||
|
|
||||||
# make ACL2 image
|
|
||||||
make LISP=${sbcl}/bin/sbcl
|
|
||||||
|
|
||||||
# The community books don't build properly under Nix yet.
|
|
||||||
rm -rf books
|
|
||||||
#make ACL2=$out/share/saved_acl2 USE_QUICKLISP=1 regression-everything
|
|
||||||
|
|
||||||
cp saved_acl2 $out/bin/acl2
|
|
||||||
'';
|
'';
|
||||||
|
|
||||||
meta = {
|
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/bin
|
||||||
|
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
|
||||||
|
'';
|
||||||
|
|
||||||
|
preDistPhases = [ (if certifyBooks then "certifyBooksPhase" else "removeBooksPhase") ];
|
||||||
|
|
||||||
|
certifyBooksPhase = ''
|
||||||
|
# Certify the community books
|
||||||
|
pushd $out/share/${pname}/books
|
||||||
|
makeFlags="ACL2=$out/share/${pname}/saved_acl2"
|
||||||
|
buildFlags="everything"
|
||||||
|
buildPhase
|
||||||
|
popd
|
||||||
|
'';
|
||||||
|
|
||||||
|
removeBooksPhase = ''
|
||||||
|
# Delete the community books
|
||||||
|
rm -rf $out/share/${pname}/books
|
||||||
|
'';
|
||||||
|
|
||||||
|
meta = with stdenv.lib; {
|
||||||
description = "An interpreter and a prover for a Lisp dialect";
|
description = "An interpreter and a prover for a Lisp dialect";
|
||||||
longDescription = ''
|
longDescription = ''
|
||||||
ACL2 is a logic and programming language in which you can model
|
ACL2 is a logic and programming language in which you can model computer
|
||||||
computer systems, together with a tool to help you prove
|
systems, together with a tool to help you prove properties of those
|
||||||
properties of those models. "ACL2" denotes "A Computational
|
models. "ACL2" denotes "A Computational Logic for Applicative Common
|
||||||
Logic for Applicative Common Lisp".
|
Lisp".
|
||||||
|
|
||||||
ACL2 is part of the Boyer-Moore family of provers, for which its
|
ACL2 is part of the Boyer-Moore family of provers, for which its authors
|
||||||
authors have received the 2005 ACM Software System Award.
|
have received the 2005 ACM Software System Award.
|
||||||
|
|
||||||
NOTE: In nixpkgs, the community books that usually ship with
|
This package installs the main ACL2 executable ${pname}, as well as the
|
||||||
ACL2 have been removed because it is not currently possible to
|
build tools cert.pl and clean.pl, renamed to ${pname}-cert and
|
||||||
build them with Nix.
|
${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/";
|
homepage = "http://www.cs.utexas.edu/users/moore/acl2/";
|
||||||
downloadPage = "https://github.com/acl2-devel/acl2-devel/releases";
|
downloadPage = "https://github.com/acl2-devel/acl2-devel/releases";
|
||||||
# There are a bunch of licenses in the community books, but since
|
license = with licenses; [
|
||||||
# they currently get deleted during the build, we don't mention
|
# ACL2 itself is bsd3
|
||||||
# their licenses here. ACL2 proper is released under a BSD
|
bsd3
|
||||||
# 3-clause license.
|
] ++ optionals certifyBooks [
|
||||||
#license = with stdenv.lib.licenses;
|
# The community books are mostly bsd3 or mit but with a few
|
||||||
#[ free bsd3 mit gpl2 llgpl21 cc0 publicDomain ];
|
# other things thrown in.
|
||||||
license = stdenv.lib.licenses.bsd3;
|
mit gpl2 llgpl21 cc0 publicDomain unfreeRedistributable
|
||||||
maintainers = with stdenv.lib.maintainers; [ kini raskin ];
|
];
|
||||||
platforms = stdenv.lib.platforms.all;
|
maintainers = with maintainers; [ kini raskin ];
|
||||||
broken = stdenv.isAarch64 && stdenv.isLinux;
|
platforms = platforms.all;
|
||||||
};
|
};
|
||||||
}
|
}
|
||||||
|
|
|
@ -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
|
||||||
|
|
|
@ -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 ];
|
||||||
|
};
|
||||||
|
}
|
|
@ -9625,6 +9625,7 @@ in
|
||||||
### DEVELOPMENT / INTERPRETERS
|
### DEVELOPMENT / INTERPRETERS
|
||||||
|
|
||||||
acl2 = callPackage ../development/interpreters/acl2 { };
|
acl2 = callPackage ../development/interpreters/acl2 { };
|
||||||
|
acl2-minimal = callPackage ../development/interpreters/acl2 { certifyBooks = false; };
|
||||||
|
|
||||||
angelscript = callPackage ../development/interpreters/angelscript {};
|
angelscript = callPackage ../development/interpreters/angelscript {};
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue