GNU bug report logs - #33764
[PATCH] gnu: z3: Update to 4.8.3 and add python{,2}-z3 bindings.

Previous Next

Full log

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Amin Bandali <bandali <at> gnu.org>
To: guix-patches <at> gnu.org
Cc: Amin Bandali <bandali <at> gnu.org>
Subject: [PATCH] gnu: z3: Update to 4.8.3 and add python{,2}-z3 bindings.
Date: Sat, 15 Dec 2018 23:05:30 -0500

* 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 <mbakke <at> fastmail.com>
 ;;; Copyright © 2018 Eric Brown <brown <at> fastmail.com>
 ;;; Copyright © 2018 Julien Lepiller <julien <at> lepiller.eu>
+;;; Copyright © 2018 Amin Bandali <bandali <at> gnu.org>
 ;;;
 ;;; 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 <clement <at> lassieur.org>
 ;;; Copyright © 2018 Maxim Cournoyer <maxim.cournoyer <at> gmail.com>
 ;;; Copyright © 2018 Luther Thompson <lutheroto <at> gmail.com>
+;;; Copyright © 2018 Amin Bandali <bandali <at> gnu.org>
 ;;;
 ;;; 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)))))
-- 
2.20.0

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.