From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:4830:134:3::10]:48964) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dOQsP-00078w-LD for guix-patches@gnu.org; Fri, 23 Jun 2017 11:52:06 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dOQsM-0001yA-GW for guix-patches@gnu.org; Fri, 23 Jun 2017 11:52:05 -0400 Received: from debbugs.gnu.org ([208.118.235.43]:60215) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1dOQsM-0001y3-CL for guix-patches@gnu.org; Fri, 23 Jun 2017 11:52:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1dOQsM-0004Oz-3O for guix-patches@gnu.org; Fri, 23 Jun 2017 11:52:02 -0400 Subject: [bug#27461] [PATCH] gnu: Add z3. Resent-Message-ID: Received: from eggs.gnu.org ([2001:4830:134:3::10]:48572) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1dOQr6-00071x-8x for guix-patches@gnu.org; Fri, 23 Jun 2017 11:50:45 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1dOQr2-0001XN-M9 for guix-patches@gnu.org; Fri, 23 Jun 2017 11:50:44 -0400 Received: from lb1.openmailbox.org ([5.79.108.160]:33494 helo=mail.openmailbox.org) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1dOQr2-0001WL-84 for guix-patches@gnu.org; Fri, 23 Jun 2017 11:50:40 -0400 From: Theodoros Foradis Date: Fri, 23 Jun 2017 18:50:22 +0300 Message-Id: <20170623155022.16252-1-theodoros.for@openmailbox.org> MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable 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: 27461@debbugs.gnu.org * 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 =C2=A9 2016 Danny Milosavljevic -;;; Copyright =C2=A9 2016 Theodoros Foradis +;;; Copyright =C2=A9 2016, 2017 Theodoros Foradis ;;; ;;; 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 =C2=A9 2017 Paul Garlick ;;; Copyright =C2=A9 2017 ng0 ;;; Copyright =C2=A9 2017 Ben Woodcroft +;;; Copyright =C2=A9 2017 Theodoros Foradis ;;; ;;; 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+))) =20 +(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=3D" + (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) )) --=20 2.13.1