From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:4830:134:3::10]:40138) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gaj6L-0003jh-Nb for guix-patches@gnu.org; Sat, 22 Dec 2018 10:22:06 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gaj6K-0000Yv-6S for guix-patches@gnu.org; Sat, 22 Dec 2018 10:22:05 -0500 Received: from debbugs.gnu.org ([208.118.235.43]:55875) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1gaj6I-0000Vb-Gu for guix-patches@gnu.org; Sat, 22 Dec 2018 10:22:04 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1gaj6I-00088e-Az for guix-patches@gnu.org; Sat, 22 Dec 2018 10:22:02 -0500 Subject: [bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{, 2}-z3 bindings. Resent-Message-ID: From: Amin Bandali References: <20181216040528.29880-1-bandali@gnu.org> <87bm5lv6tj.fsf@gnu.org> <20181217072921.GG3468@macbook41> <87efag6x3w.fsf@aminb.org> <87k1k2olth.fsf@gnu.org> <874lb6aa0g.fsf@fastmail.com> <87h8f6curk.fsf@aminb.org> Date: Sat, 22 Dec 2018 10:20:55 -0500 In-Reply-To: <87h8f6curk.fsf@aminb.org> (Amin Bandali's message of "Fri, 21 Dec 2018 18:41:51 -0500") Message-ID: <87d0ptfuzs.fsf@aminb.org> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="=-=-=" List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+kyle=kyleam.com@gnu.org Sender: "Guix-patches" To: Marius Bakke Cc: 33764@debbugs.gnu.org --=-=-= Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Apologies, I just realized that I forgot to remove my use of the @ notation in my v2 patch submitted earlier. I=E2=80=99ve attached an update= d one that doesn=E2=80=99t. --=-=-= Content-Type: text/x-patch; charset=utf-8 Content-Disposition: attachment; filename=0001-gnu-z3-Update-to-4.8.3-and-provide-python3-bindings.patch Content-Transfer-Encoding: quoted-printable >From ad9433c11ebba672db3ca75689ebee92ea9da7de Mon Sep 17 00:00:00 2001 From: Amin Bandali Date: Sat, 22 Dec 2018 10:16:57 -0500 Subject: [PATCH v3] gnu: z3: Update to 4.8.3 and provide python3 bindings * gnu/packages/maths.scm (z3): Update to 4.8.3. [build-system]: Switch from cmake to make, and use the current scripts/mk_make.py build script instead of the now-deprecated contrib/cmake/bootstrap.py. --- gnu/packages/maths.scm | 32 ++++++++++++++++++++------------ 1 file changed, 20 insertions(+), 12 deletions(-) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index 9fb02b738..1b6127e9f 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -29,6 +29,7 @@ ;;; Copyright =C2=A9 2018 Marius Bakke ;;; Copyright =C2=A9 2018 Eric Brown ;;; Copyright =C2=A9 2018 Julien Lepiller +;;; Copyright =C2=A9 2018 Amin Bandali ;;; ;;; This file is part of GNU Guix. ;;; @@ -116,6 +117,7 @@ #:use-module (gnu packages tex) #:use-module (gnu packages tls) #:use-module (gnu packages version-control) + #:use-module (gnu packages which) #:use-module (gnu packages wxwidgets) #:use-module (gnu packages xml) #:use-module (srfi srfi-1)) @@ -3965,7 +3967,7 @@ as equations, scalars, vectors, and matrices.") (define-public z3 (package (name "z3") - (version "4.8.1") + (version "4.8.3") (home-page "https://github.com/Z3Prover/z3") (source (origin (method git-fetch) @@ -3974,16 +3976,10 @@ as equations, scalars, vectors, and matrices.") (file-name (git-file-name name version)) (sha256 (base32 - "1vr57bwx40sd5riijyrhy70i2wnv9xrdihf6y5zdz56yq88rl48f")))) - (build-system cmake-build-system) + "0p5gdmhd32x6zwmx7j5cgwh4jyfxa9yapym95nlmyfaqzak92qar")))) + (build-system gnu-build-system) (arguments - `(#:configure-flags - (list "-DBUILD_PYTHON_BINDINGS=3Dtrue" - "-DINSTALL_PYTHON_BINDINGS=3Dtrue" - (string-append "-DCMAKE_INSTALL_PYTHON_PKG_DIR=3D" - %output - "/lib/python2.7/site-packages")) - #:phases + `(#:phases (modify-phases %standard-phases (add-after 'unpack 'fix-compatability ;; Versions after 4.8.3 have immintrin.h IFDEFed for Windows on= ly. @@ -3994,7 +3990,18 @@ as equations, scalars, vectors, and matrices.") (add-before 'configure 'bootstrap (lambda _ (zero? - (system* "python" "contrib/cmake/bootstrap.py" "create")))) + (system* "python" "scripts/mk_make.py")))) + ;; work around gnu-build-system's setting --enable-fast-install + ;; (z3's `configure' is a wrapper around the above python file, + ;; which fails when passed --enable-fast-install) + (replace 'configure + (lambda* (#:key inputs outputs #:allow-other-keys) + (invoke "./configure" + (string-append "--prefix=3D" (assoc-ref outputs "out"= ))))) + (add-after 'configure 'change-directory + (lambda _ + (chdir "build") + #t)) (add-before 'check 'make-test-z3 (lambda _ ;; Build the test suite executable. @@ -4005,7 +4012,8 @@ as equations, scalars, vectors, and matrices.") ;; Run all the tests that don't require arguments. (zero? (system* "./test-z3" "/a"))))))) (native-inputs - `(("python" ,python-2))) + `(("which" ,which) + ("python" ,python-wrapper))) (synopsis "Theorem prover") (description "Z3 is a theorem prover and @dfn{satisfiability modulo theories} (SMT) solver. It provides a C/C++ API, as well as Python bindin= gs.") --=20 2.20.1 --=-=-=--