From patchwork Sun Dec 16 04:05:30 2018 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Patchwork-Submitter: Amin Bandali X-Patchwork-Id: 474 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id B7ADC16895; Sun, 16 Dec 2018 06:34:17 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-6.9 required=5.0 tests=BAYES_00,RCVD_IN_DNSWL_HI, URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.0 Received: from lists.gnu.org (lists.gnu.org [IPv6:2001:4830:134:3::11]) by mira.cbaines.net (Postfix) with ESMTP id 283C316867 for ; Sun, 16 Dec 2018 06:34:17 +0000 (GMT) Received: from localhost ([::1]:41402 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gYQ0G-0003oi-Lo for patchwork@mira.cbaines.net; Sun, 16 Dec 2018 01:34:16 -0500 Received: from eggs.gnu.org ([2001:4830:134:3::10]:43395) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gYOAs-0006IY-Ij for guix-patches@gnu.org; Sat, 15 Dec 2018 23:37:07 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gYOAo-00045A-C7 for guix-patches@gnu.org; Sat, 15 Dec 2018 23:37:06 -0500 Received: from debbugs.gnu.org ([208.118.235.43]:45573) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1gYOAo-00044y-7C for guix-patches@gnu.org; Sat, 15 Dec 2018 23:37:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1gYOAn-00041J-TU for guix-patches@gnu.org; Sat, 15 Dec 2018 23:37:01 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{, 2}-z3 bindings. Resent-From: Amin Bandali Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Sun, 16 Dec 2018 04:37:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 33764 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 33764@debbugs.gnu.org X-Debbugs-Original-To: guix-patches@gnu.org Received: via spool by submit@debbugs.gnu.org id=B.154493497915397 (code B ref -1); Sun, 16 Dec 2018 04:37:01 +0000 Received: (at submit) by debbugs.gnu.org; 16 Dec 2018 04:36:19 +0000 Received: from localhost ([127.0.0.1]:49831 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gYOA7-00040H-04 for submit@debbugs.gnu.org; Sat, 15 Dec 2018 23:36:19 -0500 Received: from eggs.gnu.org ([208.118.235.92]:56323) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gYNhf-0003H2-BH for submit@debbugs.gnu.org; Sat, 15 Dec 2018 23:06:55 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gYNhX-0002ZM-Vq for submit@debbugs.gnu.org; Sat, 15 Dec 2018 23:06:49 -0500 Received: from lists.gnu.org ([2001:4830:134:3::11]:40624) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1gYNhW-0002Y5-3p for submit@debbugs.gnu.org; Sat, 15 Dec 2018 23:06:47 -0500 Received: from eggs.gnu.org ([2001:4830:134:3::10]:37690) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gYNhR-0001VE-WA for guix-patches@gnu.org; Sat, 15 Dec 2018 23:06:45 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gYNhO-0002Sz-5m for guix-patches@gnu.org; Sat, 15 Dec 2018 23:06:40 -0500 Received: from fencepost.gnu.org ([2001:4830:134:3::e]:60138) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gYNhH-0002HY-Le; Sat, 15 Dec 2018 23:06:31 -0500 Received: from wn-res-nat-129-97-125-0.dynamic.uwaterloo.ca ([129.97.125.0]:9828 helo=localhost.localdomain) by fencepost.gnu.org with esmtpsa (TLS1.2:DHE_RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1gYNhH-0004Ug-GA; Sat, 15 Dec 2018 23:06:31 -0500 From: Amin Bandali Date: Sat, 15 Dec 2018 23:05:30 -0500 Message-Id: <20181216040528.29880-1-bandali@gnu.org> X-Mailer: git-send-email 2.20.0 MIME-Version: 1.0 X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6.x X-Mailman-Approved-At: Sat, 15 Dec 2018 23:36:17 -0500 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 208.118.235.43 X-Mailman-Approved-At: Sun, 16 Dec 2018 01:34:12 -0500 X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Cc: Amin Bandali Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches * 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/python.scm (python-z3, python2-z3): New public variables. --- gnu/packages/maths.scm | 31 +++++++++++++++++++------------ gnu/packages/python.scm | 10 ++++++++++ 2 files changed, 29 insertions(+), 12 deletions(-) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index ad6aacf9c..7996c3211 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -29,6 +29,7 @@ ;;; Copyright © 2018 Marius Bakke ;;; Copyright © 2018 Eric Brown ;;; Copyright © 2018 Julien Lepiller +;;; Copyright © 2018 Amin Bandali ;;; ;;; This file is part of GNU Guix. ;;; @@ -3965,7 +3966,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) @@ -3973,21 +3974,26 @@ as equations, scalars, vectors, and matrices.") (commit (string-append "z3-" version)))) (sha256 (base32 - "1vr57bwx40sd5riijyrhy70i2wnv9xrdihf6y5zdz56yq88rl48f")))) - (build-system cmake-build-system) + "0p5gdmhd32x6zwmx7j5cgwh4jyfxa9yapym95nlmyfaqzak92qar")))) + (build-system gnu-build-system) (arguments - `(#:configure-flags - (list "-DBUILD_PYTHON_BINDINGS=true" - "-DINSTALL_PYTHON_BINDINGS=true" - (string-append "-DCMAKE_INSTALL_PYTHON_PKG_DIR=" - %output - "/lib/python2.7/site-packages")) - #:phases + `(#:phases (modify-phases %standard-phases (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=" (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. @@ -3998,7 +4004,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" ,(@ (gnu packages base) 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 bindings.") diff --git a/gnu/packages/python.scm b/gnu/packages/python.scm index fd13339cc..5db3c438e 100644 --- a/gnu/packages/python.scm +++ b/gnu/packages/python.scm @@ -56,6 +56,7 @@ ;;; Copyright © 2018 Clément Lassieur ;;; Copyright © 2018 Maxim Cournoyer ;;; Copyright © 2018 Luther Thompson +;;; Copyright © 2018 Amin Bandali ;;; ;;; This file is part of GNU Guix. ;;; @@ -14989,3 +14990,12 @@ RFC 8265 and RFC 8266.") (description "Simple decorator to set attributes of target function or class in a @acronym{DRY, Don't Repeat Yourself} way.") (license license:expat))) + +(define-public python-z3 z3) + +(define-public python2-z3 + (package (inherit python-z3) + (name "python2-z3") + (native-inputs + `(("which" ,which) + ("python" ,python-2)))))