From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:4830:134:3::10]:35391) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1da2RJ-0001Re-Se for guix-patches@gnu.org; Tue, 25 Jul 2017 12:12:07 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1da2RG-0002Tq-7b for guix-patches@gnu.org; Tue, 25 Jul 2017 12:12:05 -0400 Received: from debbugs.gnu.org ([208.118.235.43]:53478) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1da2RG-0002Tl-57 for guix-patches@gnu.org; Tue, 25 Jul 2017 12:12:02 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1da2RF-0001u0-TY for guix-patches@gnu.org; Tue, 25 Jul 2017 12:12:01 -0400 Subject: [bug#27461] [PATCH v2 1/2] gnu: Add z3. Resent-Message-ID: From: Theodoros Foradis Date: Tue, 25 Jul 2017 19:11:12 +0300 Message-Id: <20170725161113.26165-1-theodoros.for@openmailbox.org> In-Reply-To: <8760enxy1o.fsf@gnu.org> References: <8760enxy1o.fsf@gnu.org> MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 Cc: julien@lepiller.eu * 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 -;;; Copyright © 2016 Theodoros Foradis +;;; Copyright © 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 5e4cd8586..536fb9bed 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -18,6 +18,7 @@ ;;; Copyright © 2017 Paul Garlick ;;; Copyright © 2017 ng0 ;;; Copyright © 2017 Ben Woodcroft +;;; Copyright © 2017 Theodoros Foradis ;;; ;;; This file is part of GNU Guix. ;;; @@ -3141,3 +3142,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.2