diff options
Diffstat (limited to 'nixpkgs/pkgs/development/interpreters/acl2')
5 files changed, 410 insertions, 50 deletions
diff --git a/nixpkgs/pkgs/development/interpreters/acl2/0001-Fix-some-paths-for-Nix-build.patch b/nixpkgs/pkgs/development/interpreters/acl2/0001-Fix-some-paths-for-Nix-build.patch new file mode 100644 index 00000000000..2b7f8b6a53b --- /dev/null +++ b/nixpkgs/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/nixpkgs/pkgs/development/interpreters/acl2/0002-Restrict-RDTSC-to-x86.patch b/nixpkgs/pkgs/development/interpreters/acl2/0002-Restrict-RDTSC-to-x86.patch new file mode 100644 index 00000000000..74af5adef64 --- /dev/null +++ b/nixpkgs/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/nixpkgs/pkgs/development/interpreters/acl2/default.nix b/nixpkgs/pkgs/development/interpreters/acl2/default.nix index 39b243a0ce6..e3c62aae983 100644 --- a/nixpkgs/pkgs/development/interpreters/acl2/default.nix +++ b/nixpkgs/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/nixpkgs/pkgs/development/interpreters/acl2/libipasirglucose4/0001-Support-shared-library-build.patch b/nixpkgs/pkgs/development/interpreters/acl2/libipasirglucose4/0001-Support-shared-library-build.patch new file mode 100644 index 00000000000..c78fa1ab925 --- /dev/null +++ b/nixpkgs/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/nixpkgs/pkgs/development/interpreters/acl2/libipasirglucose4/default.nix b/nixpkgs/pkgs/development/interpreters/acl2/libipasirglucose4/default.nix new file mode 100644 index 00000000000..5186cd69584 --- /dev/null +++ b/nixpkgs/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 ]; + }; +} |