--- Begin Message ---
|
Subject: |
[PATCH] gnu: Add z3. |
|
Date: |
Fri, 23 Jun 2017 18:50:22 +0300 |
* gnu/packages/maths.scm (z3): New variable.
* gnu/packages/fpga.scm (yosys): Add z3 to propagated-inputs.
---
gnu/packages/fpga.scm | 5 ++++-
gnu/packages/maths.scm | 34 ++++++++++++++++++++++++++++++++++
2 files changed, 38 insertions(+), 1 deletion(-)
diff --git a/gnu/packages/fpga.scm b/gnu/packages/fpga.scm
index 420d0aff2..220877577 100644
--- a/gnu/packages/fpga.scm
+++ b/gnu/packages/fpga.scm
@@ -1,6 +1,6 @@
;;; GNU Guix --- Functional package management for GNU
;;; Copyright © 2016 Danny Milosavljevic <address@hidden>
-;;; Copyright © 2016 Theodoros Foradis <address@hidden>
+;;; Copyright © 2016, 2017 Theodoros Foradis <address@hidden>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -36,6 +36,7 @@
#:use-module (gnu packages graphviz)
#:use-module (gnu packages libffi)
#:use-module (gnu packages linux)
+ #:use-module (gnu packages maths)
#:use-module (gnu packages perl)
#:use-module (gnu packages ghostscript)
#:use-module (gnu packages gperf)
@@ -198,6 +199,8 @@ For synthesis, the compiler generates netlists in the
desired format.")
("psmisc" ,psmisc)
("xdot" ,xdot)
("abc" ,abc)))
+ (propagated-inputs
+ `(("z3" ,z3))) ; should be in path for yosys-smtbmc
(home-page "http://www.clifford.at/yosys/";)
(synopsis "FPGA Verilog RTL synthesizer")
(description "Yosys synthesizes Verilog-2005.")
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 1115cef59..3ee0beeef 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -18,6 +18,7 @@
;;; Copyright © 2017 Paul Garlick <address@hidden>
;;; Copyright © 2017 ng0 <address@hidden>
;;; Copyright © 2017 Ben Woodcroft <address@hidden>
+;;; Copyright © 2017 Theodoros Foradis <address@hidden>
;;;
;;; This file is part of GNU Guix.
;;;
@@ -3129,3 +3130,36 @@ as equations, scalars, vectors, and matrices.")
(home-page "https://www.gnu.org/software/jacal/";)
(license license:gpl3+)))
+(define-public z3
+ (package
+ (name "z3")
+ (version "4.5.0")
+ (source (origin
+ (method url-fetch)
+ (uri (string-append
+ "https://github.com/Z3Prover/z3/archive/z3-";
+ version ".tar.gz"))
+ (sha256
+ (base32
+ "032a5lvji2liwmc25jv52bdrhimqflvqbpg77ccaq1jykhiivbmf"))))
+ (build-system gnu-build-system)
+ (arguments
+ `(#:test-target "test"
+ #:phases
+ (modify-phases %standard-phases
+ (replace 'configure
+ (lambda* (#:key inputs outputs #:allow-other-keys)
+ (zero?
+ (system* "python" "scripts/mk_make.py"
+ (string-append "--prefix="
+ (assoc-ref outputs "out"))))))
+ (add-after 'configure 'change-dir
+ (lambda _
+ (chdir "build")
+ #t)))))
+ (native-inputs
+ `(("python" ,python-2)))
+ (synopsis "Theorem prover")
+ (description "@code{z3} is a theorem prover.")
+ (home-page "https://github.com/Z3Prover/z3";)
+ (license license:expat) ))
--
2.13.1
--- End Message ---
--- Begin Message ---
|
Subject: |
Re: [PATCH] gnu: Add python bindings to z3. |
|
Date: |
Mon, 21 Aug 2017 17:14:00 +0200 |
|
User-agent: |
Gnus/5.13 (Gnus v5.13) Emacs/25.2 (gnu/linux) |
Hi Theodoros,
And sorry for the long delay!
Theodoros Foradis <address@hidden> skribis:
> * gnu/packages/maths.scm (z3): Add python bindings.
> [build-system]: Change to cmake-build-system.
> [arguments]<phases>: Remove "changedir" phase.
> Add "bootstrap" phase.
> [arguments]<configure-flags>: Add them.
> [arguments]<tests>: Disable tests.
I’ve applied this patch with a few modifications, in particular
arranging to run the tests (disabling them altogether was not OK since
we knew there is a test suite):
https://git.savannah.gnu.org/cgit/guix.git/commit/?id=cf684d87d7446ffe33ca4c73bf51dc24fa5a7129
Thanks,
Ludo’.
--- End Message ---