From: Amin Bandali <bandali@gnu.org>
To: 33764@debbugs.gnu.org
Cc: Amin Bandali <bandali@gnu.org>
Subject: [bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{, 2}-z3 bindings.
Date: Sat, 15 Dec 2018 23:05:30 -0500 [thread overview]
Message-ID: <20181216040528.29880-1-bandali@gnu.org> (raw)
* 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@fastmail.com>
;;; Copyright © 2018 Eric Brown <brown@fastmail.com>
;;; Copyright © 2018 Julien Lepiller <julien@lepiller.eu>
+;;; Copyright © 2018 Amin Bandali <bandali@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@lassieur.org>
;;; Copyright © 2018 Maxim Cournoyer <maxim.cournoyer@gmail.com>
;;; Copyright © 2018 Luther Thompson <lutheroto@gmail.com>
+;;; Copyright © 2018 Amin Bandali <bandali@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
next reply other threads:[~2018-12-16 4:37 UTC|newest]
Thread overview: 9+ messages / expand[flat|nested] mbox.gz Atom feed top
2018-12-16 4:05 Amin Bandali [this message]
2018-12-16 15:18 ` [bug#33764] [PATCH] gnu: z3: Update to 4.8.3 and add python{, 2}-z3 bindings Ludovic Courtès
2018-12-17 7:29 ` Efraim Flashner
2018-12-17 14:34 ` Amin Bandali
2018-12-21 17:02 ` Ludovic Courtès
2018-12-21 20:40 ` Marius Bakke
2018-12-21 23:41 ` Amin Bandali
2018-12-22 15:20 ` Amin Bandali
2018-12-23 17:33 ` bug#33764: " Ludovic Courtès
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=20181216040528.29880-1-bandali@gnu.org \
--to=bandali@gnu.org \
--cc=33764@debbugs.gnu.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
Code repositories for project(s) associated with this external index
https://git.savannah.gnu.org/cgit/guix.git
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.